Enabled "Extract loops benchmarks" lit tests.

12 files changed, 141 insertions, 46 deletions

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index 48ca65e9..88bd8c99 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -1,58 +1,58 @@
 ----- Running regression test t1.bpl

 (0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t1.bpl(17,3): anon0

-    t1.bpl(22,3): anon3_LoopHead

+    t1.bpl(19,3): anon0

+    t1.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(8,5): anon0

+        t1.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(26,3): anon3_LoopBody

-    t1.bpl(22,3): anon3_LoopHead

+    t1.bpl(28,3): anon3_LoopBody

+    t1.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(8,5): anon0

+        t1.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(26,3): anon3_LoopBody

-    t1.bpl(22,3): anon3_LoopHead

+    t1.bpl(28,3): anon3_LoopBody

+    t1.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t1.bpl(8,5): anon0

+        t1.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t1.bpl(32,3): anon3_LoopDone

-    t1.bpl(36,3): anon2

+    t1.bpl(34,3): anon3_LoopDone

+    t1.bpl(38,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test t2.bpl

 (0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t2.bpl(16,3): anon0

-    t2.bpl(21,3): anon3_LoopHead

+    t2.bpl(18,3): anon0

+    t2.bpl(23,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t2.bpl(7,5): anon0

+        t2.bpl(9,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(25,3): anon3_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(35,3): lab1_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(35,3): lab1_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(40,3): lab1_LoopDone

-    t2.bpl(21,3): anon3_LoopHead

+    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(7,5): anon0

+        t2.bpl(9,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(25,3): anon3_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(35,3): lab1_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(35,3): lab1_LoopBody

-    t2.bpl(32,3): lab1_LoopHead

-    t2.bpl(40,3): lab1_LoopDone

-    t2.bpl(21,3): anon3_LoopHead

+    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(7,5): anon0

+        t2.bpl(9,5): anon0

     Inlined call to procedure foo ends

-    t2.bpl(44,3): anon3_LoopDone

-    t2.bpl(48,3): anon2

+    t2.bpl(46,3): anon3_LoopDone

+    t2.bpl(50,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -63,23 +63,23 @@ Boogie program verifier finished with 1 verified, 0 errors
 ----- Running regression test t3.bpl with recursion bound 4

 (0,0): Error BP5001: This assertion might not hold.

 Execution trace:

-    t3.bpl(15,3): anon0

-    t3.bpl(20,3): anon3_LoopHead

+    t3.bpl(19,3): anon0

+    t3.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(6,5): anon0

+        t3.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(24,3): anon3_LoopBody

-    t3.bpl(20,3): anon3_LoopHead

+    t3.bpl(28,3): anon3_LoopBody

+    t3.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(6,5): anon0

+        t3.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(24,3): anon3_LoopBody

-    t3.bpl(20,3): anon3_LoopHead

+    t3.bpl(28,3): anon3_LoopBody

+    t3.bpl(24,3): anon3_LoopHead

     Inlined call to procedure foo begins

-        t3.bpl(6,5): anon0

+        t3.bpl(10,5): anon0

     Inlined call to procedure foo ends

-    t3.bpl(30,3): anon3_LoopDone

-    t3.bpl(34,3): anon2

+    t3.bpl(34,3): anon3_LoopDone

+    t3.bpl(38,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl
index 976d58d6..b224aece 100644
--- a/Test/extractloops/detLoopExtract.bpl
+++ b/Test/extractloops/detLoopExtract.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t

+// RUN: %diff %s.expect %t

 var g:int;
 var h:int; //not modified
 var k:int; //modified in a procedure call
@@ -41,4 +43,4 @@ modifies k;
 {
  k := 0;
  return; 
-}
\ No newline at end of file
+}
diff --git a/Test/extractloops/detLoopExtract.bpl.expect b/Test/extractloops/detLoopExtract.bpl.expect
new file mode 100644
index 00000000..0840bd8a
--- /dev/null
+++ b/Test/extractloops/detLoopExtract.bpl.expect
@@ -0,0 +1,3 @@
+Stratified Inlining: Reached recursion bound of 4
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl
index 8388cd57..80646ef2 100644
--- a/Test/extractloops/detLoopExtract1.bpl
+++ b/Test/extractloops/detLoopExtract1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -deterministicExtractLoops -recursionBound:4 %s > %t
+// RUN: %diff %s.expect %t
 var g:int;
 
 procedure {:entrypoint} Foo(a:int)
diff --git a/Test/extractloops/detLoopExtract1.bpl.expect b/Test/extractloops/detLoopExtract1.bpl.expect
new file mode 100644
index 00000000..0840bd8a
--- /dev/null
+++ b/Test/extractloops/detLoopExtract1.bpl.expect
@@ -0,0 +1,3 @@
+Stratified Inlining: Reached recursion bound of 4
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl
index 00df45e9..2f566a4c 100644
--- a/Test/extractloops/t1.bpl
+++ b/Test/extractloops/t1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t

+// RUN: %diff %s.expect %t

 var g: int;

 

 

diff --git a/Test/extractloops/t1.bpl.expect b/Test/extractloops/t1.bpl.expect
new file mode 100644
index 00000000..9780a21f
--- /dev/null
+++ b/Test/extractloops/t1.bpl.expect
@@ -0,0 +1,21 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+    t1.bpl(19,3): anon0
+    t1.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t1.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t1.bpl(28,3): anon3_LoopBody
+    t1.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t1.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t1.bpl(28,3): anon3_LoopBody
+    t1.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t1.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t1.bpl(34,3): anon3_LoopDone
+    t1.bpl(38,3): anon2
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl
index 93f80f20..5546eb86 100644
--- a/Test/extractloops/t2.bpl
+++ b/Test/extractloops/t2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 %s > %t

+// RUN: %diff %s.expect %t

 var g: int;

 

 

diff --git a/Test/extractloops/t2.bpl.expect b/Test/extractloops/t2.bpl.expect
new file mode 100644
index 00000000..27f59372
--- /dev/null
+++ b/Test/extractloops/t2.bpl.expect
@@ -0,0 +1,33 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+    t2.bpl(18,3): anon0
+    t2.bpl(23,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t2.bpl(9,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(9,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(9,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
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl
index d14767ab..d3afa8d5 100644
--- a/Test/extractloops/t3.bpl
+++ b/Test/extractloops/t3.bpl
@@ -1,3 +1,7 @@
+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:2 %s > %t

+// RUN: %diff %s.rb2.expect %t

+// RUN: %boogie -stratifiedInline:1 -extractLoops -removeEmptyBlocks:0 -coalesceBlocks:0 -recursionBound:4 %s > %t

+// RUN: %diff %s.rb4.expect %t

 var g: int;

 

 procedure foo()

diff --git a/Test/extractloops/t3.bpl.rb2.expect b/Test/extractloops/t3.bpl.rb2.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/extractloops/t3.bpl.rb2.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/extractloops/t3.bpl.rb4.expect b/Test/extractloops/t3.bpl.rb4.expect
new file mode 100644
index 00000000..cdcdd0f2
--- /dev/null
+++ b/Test/extractloops/t3.bpl.rb4.expect
@@ -0,0 +1,21 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+    t3.bpl(19,3): anon0
+    t3.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t3.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t3.bpl(28,3): anon3_LoopBody
+    t3.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t3.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t3.bpl(28,3): anon3_LoopBody
+    t3.bpl(24,3): anon3_LoopHead
+    Inlined call to procedure foo begins
+        t3.bpl(10,5): anon0
+    Inlined call to procedure foo ends
+    t3.bpl(34,3): anon3_LoopDone
+    t3.bpl(38,3): anon2
+
+Boogie program verifier finished with 0 verified, 1 error