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

In keeping with CBMC's behaviour, generate unwinding assumptions even
when unwinding assertions are generated for (failing) assertions are not
considered fatal in GOTO programs. Unwinding assumptions should only be
skipped when partial loops are requested.

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