@@ -538,6 +538,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
538
538
// / \param struct_expr [out]: struct that we may initialize
539
539
// / \param code: block to add pre-requisite declarations (e.g. to allocate a
540
540
// / data array)
541
+ // / \param min_nondet_string_length: minimum length of strings to initialize
541
542
// / \param max_nondet_string_length: maximum length of strings to initialize
542
543
// / \param loc: location in the source
543
544
// / \param function_id: function ID to associate with auxiliary variables
@@ -573,6 +574,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
573
574
bool initialize_nondet_string_fields (
574
575
struct_exprt &struct_expr,
575
576
code_blockt &code,
577
+ const std::size_t &min_nondet_string_length,
576
578
const std::size_t &max_nondet_string_length,
577
579
const source_locationt &loc,
578
580
const irep_idt &function_id,
@@ -627,11 +629,10 @@ bool initialize_nondet_string_fields(
627
629
code.add (code_declt (length_expr));
628
630
code.add (code_assignt (length_expr, nondet_length));
629
631
630
- // assume (length_expr >= 0);
631
- code.add (
632
- code_assumet (
633
- binary_relation_exprt (
634
- length_expr, ID_ge, from_integer (0 , java_int_type ()))));
632
+ // assume (length_expr >= min_nondet_string_length);
633
+ const exprt min_length =
634
+ from_integer (min_nondet_string_length, java_int_type ());
635
+ code.add (code_assumet (binary_relation_exprt (length_expr, ID_ge, min_length)));
635
636
636
637
// assume (length_expr <= max_input_length)
637
638
if (max_nondet_string_length <= max_value (length_expr.type ()))
@@ -1044,15 +1045,15 @@ void java_object_factoryt::gen_nondet_struct_init(
1044
1045
// If the initialised type is a special-cased String type (one with length
1045
1046
// and data fields introduced by string-library preprocessing), initialise
1046
1047
// those fields with nondet values:
1047
- skip_special_string_fields =
1048
- initialize_nondet_string_fields (
1049
- to_struct_expr (initial_object) ,
1050
- assignments ,
1051
- object_factory_parameters.max_nondet_string_length ,
1052
- loc,
1053
- object_factory_parameters.function_id ,
1054
- symbol_table,
1055
- object_factory_parameters.string_printable );
1048
+ skip_special_string_fields = initialize_nondet_string_fields (
1049
+ to_struct_expr (initial_object),
1050
+ assignments ,
1051
+ object_factory_parameters. min_nondet_string_length ,
1052
+ object_factory_parameters.max_nondet_string_length ,
1053
+ loc,
1054
+ object_factory_parameters.function_id ,
1055
+ symbol_table,
1056
+ object_factory_parameters.string_printable );
1056
1057
1057
1058
assignments.copy_to_operands (
1058
1059
code_assignt (expr, initial_object));
0 commit comments