Merge pull request #6763 from tautschnig/bugfixes/fs-havoc_object

Full slice: support havoc_object

Author: tautschnig

regression/cbmc/havoc_object1/full-slice.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 6 of 8 failed.*$
+--

src/analyses/goto_rw.cpp

@@ -830,6 +830,14 @@ static void goto_rw_other(
     rw_set.get_array_objects(
       function, target, rw_range_sett::get_modet::READ, code.op1());
   }
+  else if(statement == ID_havoc_object)
+  {
+    PRECONDITION(code.operands().size() == 1);
+    // re-use get_array_objects as this havoc_object affects whatever is the
+    // object being the pointer that code.op0() is
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::LHS_W, code.op0());
+  }
 }
 
 static void goto_rw(

src/pointer-analysis/value_set.cpp

@@ -1676,6 +1676,9 @@ void value_sett::apply_code_rec(
   {
     // Ignore by default; could prune the value set.
   }
+  else if(statement == ID_havoc_object)
+  {
+  }
   else
   {
     // std::cerr << code.pretty() << '\n';

src/pointer-analysis/value_set_fi.cpp

@@ -1399,6 +1399,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
   {
     // doesn't do anything
   }
+  else if(statement == ID_havoc_object)
+  {
+  }
   else
     throw
       code.pretty()+"\n"+