@@ -369,12 +369,12 @@ exprt::operandst
369
369
symbol_tablet &symbol_table,
370
370
code_blockt &init_code)
371
371
{
372
- assert (operands.size ()==2 );
372
+ PRECONDITION (operands.size ()==2 );
373
373
exprt::operandst ops;
374
- exprt op0=operands[0 ];
375
- exprt op1=operands[1 ];
374
+ const exprt &op0=operands[0 ];
375
+ const exprt &op1=operands[1 ];
376
+ PRECONDITION (implements_java_char_sequence (op0.type ()));
376
377
377
- assert (implements_java_char_sequence (op0.type ()));
378
378
dereference_exprt deref0=
379
379
checked_dereference (op0, to_pointer_type (op0.type ()).subtype ());
380
380
process_single_operand (ops, deref0, loc, symbol_table, init_code);
@@ -396,21 +396,16 @@ exprt::operandst
396
396
typet java_string_library_preprocesst::get_data_type (
397
397
const typet &type, const symbol_tablet &symbol_table)
398
398
{
399
+ PRECONDITION (type.id ()==ID_struct || type.id ()==ID_symbol);
399
400
if (type.id ()==ID_symbol)
400
401
{
401
402
symbolt sym=symbol_table.lookup (to_symbol_type (type).get_identifier ());
402
- assert (sym.type .id ()!=ID_symbol);
403
+ CHECK_RETURN (sym.type .id ()!=ID_symbol);
403
404
return get_data_type (sym.type , symbol_table);
404
405
}
405
- else
406
- {
407
- assert (type.id ()==ID_struct);
408
- const struct_typet &struct_type=to_struct_type (type);
409
- for (auto component : struct_type.components ())
410
- if (component.get_name ()==" data" )
411
- return component.type ();
412
- assert (false && " type does not contain data component" );
413
- }
406
+ // else type id is ID_struct
407
+ const struct_typet &struct_type=to_struct_type (type);
408
+ return struct_type.component_type (" data" );
414
409
}
415
410
416
411
// / Finds the type of the length component
@@ -420,21 +415,16 @@ typet java_string_library_preprocesst::get_data_type(
420
415
typet java_string_library_preprocesst::get_length_type (
421
416
const typet &type, const symbol_tablet &symbol_table)
422
417
{
418
+ PRECONDITION (type.id ()==ID_struct || type.id ()==ID_symbol);
423
419
if (type.id ()==ID_symbol)
424
420
{
425
421
symbolt sym=symbol_table.lookup (to_symbol_type (type).get_identifier ());
426
- assert (sym.type .id ()!=ID_symbol);
422
+ CHECK_RETURN (sym.type .id ()!=ID_symbol);
427
423
return get_length_type (sym.type , symbol_table);
428
424
}
429
- else
430
- {
431
- assert (type.id ()==ID_struct);
432
- const struct_typet &struct_type=to_struct_type (type);
433
- for (auto component : struct_type.components ())
434
- if (component.get_name ()==" length" )
435
- return component.type ();
436
- assert (false && " type does not contain length component" );
437
- }
425
+ // else type id is ID_struct
426
+ const struct_typet &struct_type=to_struct_type (type);
427
+ return struct_type.component_type (" length" );
438
428
}
439
429
440
430
// / access length member
@@ -730,7 +720,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
730
720
const exprt &rhs_length,
731
721
symbol_tablet &symbol_table)
732
722
{
733
- assert (implements_java_char_sequence (lhs.type ()));
723
+ PRECONDITION (implements_java_char_sequence (lhs.type ()));
734
724
dereference_exprt deref=checked_dereference (lhs, lhs.type ().subtype ());
735
725
736
726
code_blockt code;
@@ -788,7 +778,7 @@ codet java_string_library_preprocesst::
788
778
const source_locationt &loc,
789
779
symbol_tablet &symbol_table)
790
780
{
791
- assert (implements_java_char_sequence (lhs.type ()));
781
+ PRECONDITION (implements_java_char_sequence (lhs.type ()));
792
782
dereference_exprt deref=checked_dereference (lhs, lhs.type ().subtype ());
793
783
794
784
code_blockt code;
@@ -814,7 +804,7 @@ codet java_string_library_preprocesst::
814
804
codet java_string_library_preprocesst::code_assign_java_string_to_string_expr (
815
805
const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table)
816
806
{
817
- assert (implements_java_char_sequence (rhs.type ()));
807
+ PRECONDITION (implements_java_char_sequence (rhs.type ()));
818
808
819
809
typet deref_type;
820
810
if (rhs.type ().subtype ().id ()==ID_symbol)
@@ -903,7 +893,7 @@ codet java_string_library_preprocesst::make_float_to_string_code(
903
893
{
904
894
// Getting the argument
905
895
code_typet::parameterst params=type.parameters ();
906
- assert (params.size ()==1 && " wrong number of parameters in Float.toString " );
896
+ PRECONDITION (params.size ()==1 );
907
897
exprt arg=symbol_exprt (params[0 ].get_identifier (), params[0 ].type ());
908
898
909
899
// Holder for output code
@@ -1012,7 +1002,10 @@ codet java_string_library_preprocesst::make_float_to_string_code(
1012
1002
string_expr_list.push_back (neg_simple_notation);
1013
1003
1014
1004
// Combining all cases
1015
- assert (string_expr_list.size ()==condition_list.size ());
1005
+ INVARIANT (
1006
+ string_expr_list.size ()==condition_list.size (),
1007
+ " number of created strings should correspond to number of conditions" );
1008
+
1016
1009
// We do not check the condition of the first element in the list as it
1017
1010
// will be reached only if all other conditions are not satisfied.
1018
1011
codet tmp_code=code_assign_string_expr_to_java_string (
@@ -1059,7 +1052,7 @@ codet java_string_library_preprocesst::make_init_function_from_call(
1059
1052
code_typet::parameterst params=type.parameters ();
1060
1053
1061
1054
// The first parameter is the object to be initialized
1062
- assert (!params.empty ());
1055
+ PRECONDITION (!params.empty ());
1063
1056
exprt arg_this=symbol_exprt (params[0 ].get_identifier (), params[0 ].type ());
1064
1057
if (ignore_first_arg)
1065
1058
params.erase (params.begin ());
@@ -1100,11 +1093,11 @@ codet java_string_library_preprocesst::
1100
1093
symbol_tablet &symbol_table)
1101
1094
{
1102
1095
// This is similar to assign functions except we return a pointer to `this`
1096
+ code_typet::parameterst params=type.parameters ();
1097
+ PRECONDITION (!params.empty ());
1103
1098
code_blockt code;
1104
1099
code.add (make_assign_function_from_call (
1105
1100
function_name, type, loc, symbol_table));
1106
- code_typet::parameterst params=type.parameters ();
1107
- assert (!params.empty ());
1108
1101
exprt arg_this=symbol_exprt (params[0 ].get_identifier (), params[0 ].type ());
1109
1102
code.add (code_returnt (arg_this));
1110
1103
return code;
@@ -1151,10 +1144,10 @@ codet java_string_library_preprocesst::make_string_to_char_array_code(
1151
1144
symbol_tablet &symbol_table)
1152
1145
{
1153
1146
code_blockt code;
1154
- assert (!type.parameters ().empty ());
1147
+ PRECONDITION (!type.parameters ().empty ());
1155
1148
const code_typet::parametert &p=type.parameters ()[0 ];
1156
1149
symbol_exprt string_argument (p.get_identifier (), p.type ());
1157
- assert (implements_java_char_sequence (string_argument.type ()));
1150
+ PRECONDITION (implements_java_char_sequence (string_argument.type ()));
1158
1151
1159
1152
// lhs = new java::array[char]
1160
1153
exprt lhs=allocate_fresh_array (
0 commit comments