Merge pull request #5870 from tautschnig/loop-counter

Loop counter resetting must not result in unlimited unwinding

Author: tautschnig

regression/cbmc/unwind_counters4/main.c

@@ -0,0 +1,24 @@
+int main()
+{
+  int x;
+  int y;
+
+  do
+  {
+    y = 10;
+    goto label;
+    x = 1; // dead code, makes sure the above goto is not removed
+  label:
+    _Bool nondet;
+    if(nondet)
+      __CPROVER_assert(y != 10, "violated via first loop");
+    else
+      __CPROVER_assert(y != 20, "violated via second loop");
+
+    if(x % 2)
+      break; // this statement must not cause the loop counter to be reset
+  } while(1);
+
+  y = 20;
+  goto label;
+}

regression/cbmc/unwind_counters4/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\** 2 of 2 failed
+--
+--
+Loop unwinding must terminate despite the existence of multiple loop entry
+points.

src/goto-symex/symex_main.cpp

@@ -97,7 +97,7 @@ void symex_transition(
     for(const auto &i_e : instruction.incoming_edges)
     {
       if(
-        i_e->is_goto() && i_e->is_backwards_goto() &&
+        i_e->is_backwards_goto() && i_e->get_target() == to &&
         (!is_backwards_goto ||
          state.source.pc->location_number > i_e->location_number))
       {