Merge pull request #5455 from tautschnig/fix-5450

Fix loop-to-assume transformation in goto-symex

Author: tautschnig

regression/cbmc/while2/main.c

@@ -0,0 +1,20 @@
+#include "assert.h"
+
+int main()
+{
+  int count = 0;
+  do
+  {
+    count = count + 1;
+  } while(count < 5);
+
+  do
+  {
+  } while(count < 5);
+
+  while(count < 5)
+    ;
+
+  assert(count == 5);
+  assert(count == 17);
+}

regression/cbmc/while2/requires-transform.c

@@ -0,0 +1,15 @@
+#include "assert.h"
+
+int main()
+{
+  int count;
+
+  do
+  {
+  } while(count < 5);
+
+  while(count < 5)
+    ;
+
+  assert(count >= 5);
+}

regression/cbmc/while2/requires-transform.desc

@@ -0,0 +1,11 @@
+CORE
+requires-transform.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test will only terminate, if the transformation of loops to assumes by
+goto-symex is applied.

regression/cbmc/while2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line 18 assertion count == 5: SUCCESS$
+^\[main.assertion.2\] line 19 assertion count == 17: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-symex/symex_goto.cpp

@@ -252,9 +252,12 @@ void goto_symext::symex_goto(statet &state)
     // is it label: goto label; or while(cond); - popular in SV-COMP
     if(
       symex_config.self_loops_to_assumptions &&
+      // label: goto label; or do {} while(cond);
       (goto_target == state.source.pc ||
+       // while(cond);
        (instruction.incoming_edges.size() == 1 &&
-        *instruction.incoming_edges.begin() == goto_target)))
+        *instruction.incoming_edges.begin() == goto_target &&
+        goto_target->is_goto() && new_guard.is_true())))
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto