Skip to content

Commit

Permalink
Add invariant on array to pointer association
Browse files Browse the repository at this point in the history
In the string solver each char array should be associated to a pointer
which is unique for each array. This invariant ensures we don't make
mistake there.
  • Loading branch information
romainbrenguier committed Nov 23, 2017
1 parent 2a22a2e commit 2e760b3
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion src/solvers/refinement/string_constraint_generator_main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,10 @@ exprt string_constraint_generatort::associate_array_to_pointer(

/// \todo We should use a function for inserting the correspondance
/// between array and pointers.
arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
const auto it_bool =
arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
INVARIANT(
it_bool.second, "should not associate two arrays to the same pointer");
add_default_axioms(to_array_string_expr(array_expr));
return from_integer(0, f.type());
}
Expand Down

0 comments on commit 2e760b3

Please sign in to comment.