Skip to content

Commit fbb5724

Browse files
Declaring string expression symbol for each string_exprt
These are used in the string solver. So each string_exprt used in the code should have a symbol of the same type which corresponds to it.
1 parent a9de859 commit fbb5724

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

+4
Original file line numberDiff line numberDiff line change
@@ -1223,6 +1223,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
12231223
ID_cprover_string_literal_func,
12241224
{class_identifier},
12251225
symbol_table));
1226+
exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code);
1227+
code.add(code_assignt(string_expr_sym, string_expr));
12261228

12271229
// string_expr1 = substr(string_expr, 6)
12281230
// We do this to remove the "java::" prefix
@@ -1233,6 +1235,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
12331235
ID_cprover_string_substring_func,
12341236
{string_expr, from_integer(6, java_int_type())},
12351237
symbol_table));
1238+
exprt string_expr_sym1=fresh_string_expr_symbol(loc, symbol_table, code);
1239+
code.add(code_assignt(string_expr_sym1, string_expr1));
12361240

12371241
// string1 = (String*) string_expr
12381242
pointer_typet string_ptr_type(

0 commit comments

Comments
 (0)