Support for irreducible graphs (with extractLoops)

3 files changed, 117 insertions, 46 deletions

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index b3efbe02..9a6c95a3 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -1,58 +1,81 @@
 ----- Running regression test t1.bpl

 t1.bpl(38,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        t1.bpl(19,3): anon0

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(27,3): anon3_LoopBody

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(27,3): anon3_LoopBody

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(33,3): anon3_LoopDone

-        t1.bpl(37,3): anon2

+    t1.bpl(19,3): anon0

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(27,3): anon3_LoopBody

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(27,3): anon3_LoopBody

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(33,3): anon3_LoopDone

+    t1.bpl(37,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test t2.bpl

 t2.bpl(51,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        t2.bpl(19,3): anon0

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(27,3): anon3_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(42,3): lab1_LoopDone

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(27,3): anon3_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(42,3): lab1_LoopDone

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(46,3): anon3_LoopDone

-        t2.bpl(50,3): anon2

+    t2.bpl(19,3): anon0

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(27,3): anon3_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(42,3): lab1_LoopDone

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(27,3): anon3_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(42,3): lab1_LoopDone

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(46,3): anon3_LoopDone

+    t2.bpl(50,3): anon2

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

+----- Running regression test t3.bpl with recursion bound 2

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

+----- Running regression test t3.bpl with recursion bound 4

+t3.bpl(38,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    t3.bpl(19,3): anon0

+    t3.bpl(27,3): anon3_LoopBody

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t3.bpl(27,3): anon3_LoopBody

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t3.bpl(33,3): anon3_LoopDone

+    t3.bpl(37,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index dbc524c0..1ee560b9 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -10,4 +10,10 @@ echo -----
 echo ----- Running regression test t2.bpl

 %BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t2.bpl

 echo -----

+echo ----- Running regression test t3.bpl with recursion bound 2

+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:2 t3.bpl

+echo -----

+echo ----- Running regression test t3.bpl with recursion bound 4

+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl

+echo -----

 

diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl
new file mode 100644
index 00000000..e5fad6d1
--- /dev/null
+++ b/Test/extractloops/t3.bpl
@@ -0,0 +1,42 @@
+var g: int;

+

+procedure A();

+  requires g == 0;

+  modifies g;

+

+procedure {:inline 1} {:verify false} foo(); 

+

+implementation foo() {

+  var t: int;

+  t := 0;

+}

+

+implementation A()

+{

+  var x: int;

+  var y: int;

+

+  anon0:

+    x := 4;

+    goto anon3_LoopHead, anon3_LoopBody;

+

+  anon3_LoopHead:

+    call foo();

+    goto anon3_LoopDone, anon3_LoopBody;

+

+  anon3_LoopBody:

+    assume g < x;

+    g := g + 1;

+    x := x - 1;

+    goto anon3_LoopHead;

+

+  anon3_LoopDone:

+    assume g >= x;

+    goto anon2;

+

+  anon2:

+    assert x == 1;

+    return;

+}

+

+