Skip to content

Commit ea0c70a

Browse files
Remove redundant pointer to array association
This redundant step which is already done in process_parameters, was detected in string constraint generation as an attempt to access two array to the same pointers. Although the array are in fact the same here, the second call to add_pointer_to_array_association is unecessary.
1 parent 89c123e commit ea0c70a

File tree

1 file changed

+0
-8
lines changed

1 file changed

+0
-8
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -1696,14 +1696,6 @@ codet java_string_library_preprocesst::make_init_from_array_code(
16961696
/// \todo this assumes the array to be constant between all calls to
16971697
/// string primitives, which may not be true in general.
16981698
refined_string_exprt string_arg = to_string_expr(args[1]);
1699-
add_pointer_to_array_association(
1700-
string_arg.content(),
1701-
dereference_exprt(
1702-
string_arg.content(),
1703-
array_typet(java_char_type(), infinity_exprt(java_int_type()))),
1704-
symbol_table,
1705-
loc,
1706-
code);
17071699

17081700
// The third argument is `count`, whereas the third argument of substring
17091701
// is `end` which corresponds to `offset+count`

0 commit comments

Comments
 (0)