Merge pull request #7831 from thomasspriggs/tas/fix_havoc_guards

Fix havoc guards

Author: Enrico Steffinlongo

regression/cbmc/havoc_choice/main.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+#include <stdbool.h>
+
+bool nondet_bool();
+
+int main()
+{
+  char a = 'a';
+  char b = 'b';
+  char c = 'c';
+  char d = 'd';
+
+  char *p =
+    nondet_bool() ? (nondet_bool() ? &a : &b) : (nondet_bool() ? &c : &d);
+
+  __CPROVER_havoc_object(p);
+
+  if(p == &a)
+    assert(a == 'a');
+  else
+    assert(a == 'a');
+
+  if(p == &b)
+    assert(b == 'b');
+  else
+    assert(b == 'b');
+
+  if(p == &c)
+    assert(c == 'c');
+  else
+    assert(c == 'c');
+
+  if(p == &d)
+    assert(d == 'd');
+  else
+    assert(d == 'd');
+}

regression/cbmc/havoc_choice/test.desc

@@ -0,0 +1,19 @@
+CORE new-smt-backend
+main.c
+
+\[main\.assertion\.1\] line \d+ assertion a \=\= \'a\'\: FAILURE
+\[main\.assertion\.2\] line \d+ assertion a \=\= \'a\'\: SUCCESS
+\[main\.assertion\.3\] line \d+ assertion b \=\= \'b\'\: FAILURE
+\[main\.assertion\.4\] line \d+ assertion b \=\= \'b\'\: SUCCESS
+\[main\.assertion\.5\] line \d+ assertion c \=\= \'c\'\: FAILURE
+\[main\.assertion\.6\] line \d+ assertion c \=\= \'c\'\: SUCCESS
+\[main\.assertion\.7\] line \d+ assertion d \=\= \'d\'\: FAILURE
+\[main\.assertion\.8\] line \d+ assertion d \=\= \'d\'\: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+In the case where __CPROVER_havoc_object is applied to a pointer which points
+to one of a selection of objects, only the one object which it pointed to should
+be reassigned. This test is to cover the specific case where the value of the
+pointer is expressed using nested ternary conditional expressions.

src/goto-symex/symex_other.cpp

@@ -46,11 +46,11 @@ void goto_symext::havoc_rec(
   {
     const if_exprt &if_expr=to_if_expr(dest);
 
-    guardt guard_t=state.guard;
+    guardt guard_t = guard;
     guard_t.add(if_expr.cond());
     havoc_rec(state, guard_t, if_expr.true_case());
 
-    guardt guard_f=state.guard;
+    guardt guard_f = guard;
     guard_f.add(not_exprt(if_expr.cond()));
     havoc_rec(state, guard_f, if_expr.false_case());
   }
@@ -68,7 +68,11 @@ void goto_symext::havoc_rec(
   }
   else
   {
-    // consider printing a warning
+    INVARIANT_WITH_DIAGNOSTICS(
+      false,
+      "Attempted to symex havoc applied to unsupported expression",
+      state.source.pc->code().pretty(),
+      dest.pretty());
   }
 }