diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 01:16:59 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-08-24 01:16:59 +0530 |
| commit | 64b57a073afe03ab57d99c96ef6994b77f786d0e (patch) | |
| tree | c30b495975bcd0c0299b864945408525b92332f0 /Test | |
| parent | 426914e83193a9434a360d0d0ca4752fdf752e64 (diff) | |
Support for irreducible graphs (with extractLoops)
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/extractloops/Answer | 115 | ||||
| -rw-r--r-- | Test/extractloops/runtest.bat | 6 | ||||
| -rw-r--r-- | Test/extractloops/t3.bpl | 42 |
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;
+}
+
+
|