diff options
| author |  akashlal <unknown> | 2010-09-04 20:19:51 +0000 |
|---|---|---|
| committer | akashlal <unknown> | 2010-09-04 20:19:51 +0000 |
| commit | 2417ba8293140541c1b626189adc27a26238891c (patch) | |
| tree | f020d4b0a42fca705eeb6c54b62da00eeeeb9164 /Test/extractloops | |
| parent | 6541ac9ebb538c339f818e9d473e09c5207f23ae (diff) | |
Added tests for extractloops
Diffstat (limited to 'Test/extractloops')
| -rw-r--r-- | Test/extractloops/Answer | 58 | ||||
| -rw-r--r-- | Test/extractloops/runtest.bat | 13 | ||||
| -rw-r--r-- | Test/extractloops/t1.bpl | 42 | ||||
| -rw-r--r-- | Test/extractloops/t2.bpl | 56 |
4 files changed, 169 insertions, 0 deletions
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;
+}
+
+
|