diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test16 | |
Initial set of files.
Diffstat (limited to 'Test/test16')
| -rw-r--r-- | Test/test16/Answer | 23 | ||||
| -rw-r--r-- | Test/test16/LoopUnroll.bpl | 79 | ||||
| -rw-r--r-- | Test/test16/Output | 23 | ||||
| -rw-r--r-- | Test/test16/runtest.bat | 13 |
4 files changed, 138 insertions, 0 deletions
diff --git a/Test/test16/Answer b/Test/test16/Answer new file mode 100644 index 00000000..5fac425b --- /dev/null +++ b/Test/test16/Answer @@ -0,0 +1,23 @@ +-------------------- LoopUnroll.bpl /loopUnroll:1 --------------------
+LoopUnroll.bpl(56,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LoopUnroll.bpl(52,5): anon0#1
+ LoopUnroll.bpl(53,3): anon2_LoopHead#1
+ LoopUnroll.bpl(55,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 2 verified, 1 error
+-------------------- LoopUnroll.bpl /loopUnroll:2 --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+-------------------- LoopUnroll.bpl /loopUnroll:3 --------------------
+LoopUnroll.bpl(74,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LoopUnroll.bpl(68,5): anon0#3
+ LoopUnroll.bpl(69,3): anon2_LoopHead#3
+ LoopUnroll.bpl(71,5): anon2_LoopBody#3
+ LoopUnroll.bpl(69,3): anon2_LoopHead#2
+ LoopUnroll.bpl(71,5): anon2_LoopBody#2
+ LoopUnroll.bpl(69,3): anon2_LoopHead#1
+ LoopUnroll.bpl(71,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test16/LoopUnroll.bpl b/Test/test16/LoopUnroll.bpl new file mode 100644 index 00000000..83bf2686 --- /dev/null +++ b/Test/test16/LoopUnroll.bpl @@ -0,0 +1,79 @@ +procedure P()
+{
+ var x: int;
+
+ A:
+ x := 0;
+ goto B, Goner, C;
+
+ B:
+ x := 1;
+ goto D;
+
+ C:
+ x := 2;
+ goto D;
+
+ Goner:
+ x := 5;
+ assume false;
+ x := 6;
+ goto B;
+
+ D:
+ x := 3;
+ goto LoopHead;
+
+ LoopHead:
+ assert x < 100;
+ goto LoopBody, LoopDone;
+
+ LoopBody:
+ x := x + 1;
+ goto LoopHead, LoopBodyMore;
+
+ LoopBodyMore:
+ x := x + 2;
+ goto LoopHead;
+
+ LoopDone:
+ x := 88;
+ return;
+}
+
+type MyValue;
+const SpecialValue: MyValue;
+
+procedure WrongRange(a: [int]MyValue, N: int)
+ requires 0 <= N;
+{
+ var i: int, v: MyValue;
+
+ i := 1; // bad idea
+ while (i <= N) // also a bad idea
+ {
+ assert 0 <= i; // lower bounds check
+ assert i < N; // error: upper bounds check
+ v := a[i];
+ i := i + 1;
+ }
+}
+
+procedure ManyIterations(a: [int]MyValue, N: int)
+ requires 0 <= N;
+ requires a[0] != SpecialValue && a[1] != SpecialValue;
+{
+ var i: int, v: MyValue;
+
+ i := 0;
+ while (i < N)
+ {
+ assert 0 <= i; // lower bounds check
+ assert i < N; // upper bounds check
+ v := a[i];
+ assert a[i] != SpecialValue; // error: after more than 2 loop unrollings
+ i := i + 1;
+ }
+}
+
+// ERROR: /printInstrumented seems to erase filename source-location information
diff --git a/Test/test16/Output b/Test/test16/Output new file mode 100644 index 00000000..5fac425b --- /dev/null +++ b/Test/test16/Output @@ -0,0 +1,23 @@ +-------------------- LoopUnroll.bpl /loopUnroll:1 --------------------
+LoopUnroll.bpl(56,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LoopUnroll.bpl(52,5): anon0#1
+ LoopUnroll.bpl(53,3): anon2_LoopHead#1
+ LoopUnroll.bpl(55,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 2 verified, 1 error
+-------------------- LoopUnroll.bpl /loopUnroll:2 --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+-------------------- LoopUnroll.bpl /loopUnroll:3 --------------------
+LoopUnroll.bpl(74,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ LoopUnroll.bpl(68,5): anon0#3
+ LoopUnroll.bpl(69,3): anon2_LoopHead#3
+ LoopUnroll.bpl(71,5): anon2_LoopBody#3
+ LoopUnroll.bpl(69,3): anon2_LoopHead#2
+ LoopUnroll.bpl(71,5): anon2_LoopBody#2
+ LoopUnroll.bpl(69,3): anon2_LoopHead#1
+ LoopUnroll.bpl(71,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test16/runtest.bat b/Test/test16/runtest.bat new file mode 100644 index 00000000..069ecd63 --- /dev/null +++ b/Test/test16/runtest.bat @@ -0,0 +1,13 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+echo -------------------- LoopUnroll.bpl /loopUnroll:1 --------------------
+"%BPLEXE%" %* /loopUnroll:1 /logPrefix:-lu1 LoopUnroll.bpl
+echo -------------------- LoopUnroll.bpl /loopUnroll:2 --------------------
+"%BPLEXE%" %* LoopUnroll.bpl /logPrefix:-lu2 /proc:ManyIterations /loopUnroll:2
+echo -------------------- LoopUnroll.bpl /loopUnroll:3 --------------------
+"%BPLEXE%" %* LoopUnroll.bpl /logPrefix:-lu3 /proc:ManyIterations /loopUnroll:3
+
|