From 2417ba8293140541c1b626189adc27a26238891c Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Sat, 4 Sep 2010 20:19:51 +0000
Subject: Added tests for extractloops

---
 Test/extractloops/Answer      | 58 +++++++++++++++++++++++++++++++++++++++++++
 Test/extractloops/runtest.bat | 13 ++++++++++
 Test/extractloops/t1.bpl      | 42 +++++++++++++++++++++++++++++++
 Test/extractloops/t2.bpl      | 56 +++++++++++++++++++++++++++++++++++++++++
 4 files changed, 169 insertions(+)
 create mode 100644 Test/extractloops/Answer
 create mode 100644 Test/extractloops/runtest.bat
 create mode 100644 Test/extractloops/t1.bpl
 create mode 100644 Test/extractloops/t2.bpl

(limited to 'Test/extractloops')

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
new file mode 100644
index 00000000..b3efbe02
--- /dev/null
+++ b/Test/extractloops/Answer
@@ -0,0 +1,58 @@
+----- 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
+
+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
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
new file mode 100644
index 00000000..dbc524c0
--- /dev/null
+++ b/Test/extractloops/runtest.bat
@@ -0,0 +1,13 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
+echo ----- Running regression test t1.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t1.bpl
+echo -----
+echo ----- Running regression test t2.bpl
+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t2.bpl
+echo -----
+
diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl
new file mode 100644
index 00000000..58b89e6b
--- /dev/null
+++ b/Test/extractloops/t1.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_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;
+}
+
+
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl
new file mode 100644
index 00000000..d0011929
--- /dev/null
+++ b/Test/extractloops/t2.bpl
@@ -0,0 +1,56 @@
+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_LoopHead:
+    call foo();
+    goto anon3_LoopDone, anon3_LoopBody;
+
+  anon3_LoopBody:
+    assume g < x;
+    g := g + 1;
+    x := x - 1;
+    y := 0;
+    goto lab1_LoopHead;
+
+  lab1_LoopHead:
+    goto lab1_LoopBody, lab1_LoopDone;
+
+  lab1_LoopBody:
+    assume y < 2;
+    y := y + 1;
+    goto lab1_LoopHead;
+    
+  lab1_LoopDone:
+    assume y >= 2;
+    goto anon3_LoopHead;
+
+  anon3_LoopDone:
+    assume g >= x;
+    goto anon2;
+
+  anon2:
+    assert false;
+    assert x == 1;
+    return;
+}
+
+
-- 
cgit v1.2.3