Skip to content

Commit

Permalink
Remove redundant pointer to array association
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
romainbrenguier committed Nov 23, 2017
1 parent 89c123e commit ea0c70a
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1696,14 +1696,6 @@ codet java_string_library_preprocesst::make_init_from_array_code(
/// \todo this assumes the array to be constant between all calls to
/// string primitives, which may not be true in general.
refined_string_exprt string_arg = to_string_expr(args[1]);
add_pointer_to_array_association(
string_arg.content(),
dereference_exprt(
string_arg.content(),
array_typet(java_char_type(), infinity_exprt(java_int_type()))),
symbol_table,
loc,
code);

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

0 comments on commit ea0c70a

Please sign in to comment.