Check frame conditions on deallocating

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

regression/contracts/assigns_enforce_18/main.c

@@ -14,12 +14,18 @@ void foo(int *xp, int *xq, int a) __CPROVER_assigns(*xp)
   y = -1;
 }
 
-void bar(int *a, int *b) __CPROVER_assigns(a, *b)
+void bar(int *a, int *b) __CPROVER_assigns(*a, *b)
 {
   free(a);
   *b = 0;
 }
 
+void baz(int *a, int *c) __CPROVER_assigns(*a)
+{
+  free(c);
+  *a = 0;
+}
+
 int main()
 {
   int z = 0;
@@ -31,5 +37,7 @@ int main()
   int b = 1;
   bar(a, &b);
   assert(b == 0);
+  int *c = malloc(sizeof(*c));
+  baz(&y, c);
   return 0;
 }

regression/contracts/assigns_enforce_18/test.desc

@@ -3,13 +3,16 @@ main.c
 --enforce-all-contracts _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
+^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$
+^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
-^.* 1 of \d+ failed \(\d+ iteration.*\)$
+^.* 2 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --
 ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$

src/goto-instrument/contracts/contracts.cpp

@@ -743,8 +743,19 @@ void code_contractst::instrument_call_statement(
   }
   else if(called_name == "free")
   {
-    assigns_clause.remove_from_local_write_set(dereference_exprt(
-      to_typecast_expr(instruction_iterator->call_arguments().front()).op()));
+    goto_programt alias_assertion;
+    const exprt &lhs_dereference = dereference_exprt(
+      to_typecast_expr(instruction_iterator->call_arguments().front()).op());
+    alias_assertion.add(goto_programt::make_assertion(
+      assigns_clause.generate_containment_check(lhs_dereference),
+      instruction_iterator->source_location));
+    alias_assertion.instructions.back().source_location.set_comment(
+      "Check that " + from_expr(ns, lhs_dereference.id(), lhs_dereference) +
+      " is assignable");
+    assigns_clause.remove_from_local_write_set(lhs_dereference);
+    assigns_clause.remove_from_global_write_set(lhs_dereference);
+    insert_before_swap_and_advance(
+      program, instruction_iterator, alias_assertion);
     return;
   }