Skip to content

Commit 2e760b3

Browse files
Add invariant on array to pointer association
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.
1 parent 2a22a2e commit 2e760b3

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -270,7 +270,10 @@ exprt string_constraint_generatort::associate_array_to_pointer(
270270

271271
/// \todo We should use a function for inserting the correspondance
272272
/// between array and pointers.
273-
arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
273+
const auto it_bool =
274+
arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
275+
INVARIANT(
276+
it_bool.second, "should not associate two arrays to the same pointer");
274277
add_default_axioms(to_array_string_expr(array_expr));
275278
return from_integer(0, f.type());
276279
}

0 commit comments

Comments
 (0)