Merge pull request #6630 from tautschnig/bugfixes/missing-assumption

goto-instrument --unwind: unwinding assertions do not disable unwinding assumptions

Author: tautschnig

regression/goto-instrument/unwind-assert2/main.c

@@ -3,4 +3,5 @@ int main()
 {
   int i;
   for(i = 0; i < 10; i++) {}
+  __CPROVER_assert(0, "fails when fully unwinding the loop");
 }

regression/goto-instrument/unwind-assert2/test.desc

@@ -1,6 +1,8 @@
 CORE
 main.c
 --unwind 9 --unwinding-assertions
+^\[main.assertion.1\] line 6 fails when fully unwinding the loop: SUCCESS$
+^\*\* 1 of 2 failed
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -194,7 +194,7 @@ int goto_instrument_parse_optionst::doit()
 
         if(unwinding_assertions)
         {
-          unwind_strategy=goto_unwindt::unwind_strategyt::ASSERT;
+          unwind_strategy = goto_unwindt::unwind_strategyt::ASSERT_ASSUME;
         }
         else if(partial_loops)
         {

src/goto-instrument/unwind.cpp

@@ -128,6 +128,10 @@ void goto_unwindt::unwind(
   }
   else
   {
+    PRECONDITION(
+      unwind_strategy == unwind_strategyt::ASSERT_ASSUME ||
+      unwind_strategy == unwind_strategyt::ASSUME);
+
     goto_programt::const_targett t=loop_exit;
     t--;
     assert(t->is_backwards_goto());
@@ -144,22 +148,23 @@ void goto_unwindt::unwind(
         exit_cond = loop_head->get_condition();
     }
 
-    goto_programt::targett new_t;
-
-    if(unwind_strategy==unwind_strategyt::ASSERT)
+    if(unwind_strategy == unwind_strategyt::ASSERT_ASSUME)
     {
-      new_t = rest_program.add(goto_programt::make_assertion(exit_cond));
+      goto_programt::targett assertion = rest_program.add(
+        goto_programt::make_assertion(exit_cond, loop_head->source_location()));
+      unwind_log.insert(assertion, loop_head->location_number);
     }
-    else if(unwind_strategy==unwind_strategyt::ASSUME)
+
+    if(
+      unwind_strategy == unwind_strategyt::ASSUME ||
+      unwind_strategy == unwind_strategyt::ASSERT_ASSUME)
     {
-      new_t = rest_program.add(goto_programt::make_assumption(exit_cond));
+      goto_programt::targett assumption =
+        rest_program.add(goto_programt::make_assumption(
+          exit_cond, loop_head->source_location()));
+      unwind_log.insert(assumption, loop_head->location_number);
     }
-    else
-      UNREACHABLE;
 
-    new_t->source_location_nonconst() = loop_head->source_location();
-    new_t->location_number=loop_head->location_number;
-    unwind_log.insert(new_t, loop_head->location_number);
   }
 
   assert(!rest_program.empty());

src/goto-instrument/unwind.h

@@ -21,7 +21,13 @@ class unwindsett;
 class goto_unwindt
 {
 public:
-  enum class unwind_strategyt { CONTINUE, PARTIAL, ASSERT, ASSUME };
+  enum class unwind_strategyt
+  {
+    CONTINUE,
+    PARTIAL,
+    ASSERT_ASSUME,
+    ASSUME
+  };
 
   // unwind loop