Check frame conditions before __CPROVER_havoc_object

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_20/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+
+void foo(int *y) __CPROVER_assigns()
+{
+  __CPROVER_havoc_object(y);
+  x = 2;
+}
+
+int main()
+{
+  int *y = malloc(sizeof(*y));
+  *y = 0;
+  foo(y);
+  assert(x == 2);
+  return 0;
+}

regression/contracts/assigns_enforce_20/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether contract enforcement works with __CPROVER_havoc_object.

src/goto-instrument/contracts/contracts.cpp

@@ -748,7 +748,8 @@ void code_contractst::instrument_call_statement(
     called_name =
       to_symbol_expr(instruction_iterator->call_function()).get_identifier();
   }
-
+  log.warning() << "called function: " << id2string(called_name)
+                << messaget::eom;
   if(called_name == "malloc")
   {
     // malloc statments return a void pointer, which is then cast and assigned
@@ -972,6 +973,23 @@ void code_contractst::check_frame_conditions(
     {
       assigns.remove_from_local_write_set(instruction_it->get_dead().symbol());
     }
+    else if(
+      instruction_it->is_other() &&
+      instruction_it->get_other().get_statement() == ID_havoc_object)
+    {
+      goto_programt alias_assertion;
+      const exprt &havoc_argument = dereference_exprt(
+        to_typecast_expr(instruction_it->get_other().operands().front()).op());
+      alias_assertion.add(goto_programt::make_assertion(
+        assigns.generate_containment_check(havoc_argument),
+        instruction_it->source_location));
+      alias_assertion.instructions.back().source_location.set_comment(
+        "Check that " + from_expr(ns, havoc_argument.id(), havoc_argument) +
+        " is assignable");
+      assigns.remove_from_local_write_set(havoc_argument);
+      assigns.remove_from_global_write_set(havoc_argument);
+      insert_before_swap_and_advance(program, instruction_it, alias_assertion);
+    }
   }
 }