diff options
| author |  wuestholz <unknown> | 2013-06-02 18:16:30 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-02 18:16:30 -0700 |
| commit | 734ee394898d9e37c784f32e0d105678f82d981a (patch) | |
| tree | 16a650a0da1d5e03f7675bfc930669e708f31342 /Test | |
| parent | 5aaf3b555f7ffd81468d95f1d543f5f1212f6643 (diff) | |
Added a feature for verifying several program snapshots (incl. result caching and prioritization).
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/alltests.txt | 1 | ||||
| -rw-r--r-- | Test/snapshots/Answer | 27 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots0.v0.bpl | 42 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots0.v1.bpl | 42 | ||||
| -rw-r--r-- | Test/snapshots/Snapshots0.v2.bpl | 31 | ||||
| -rw-r--r-- | Test/snapshots/runtest.bat | 7 |
6 files changed, 150 insertions, 0 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt index ebe396e9..c0eec7ad 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -28,3 +28,4 @@ stratifiedinline Use Stratified inlining benchmarks extractloops Use Extract loops benchmarks
havoc0 Use HAVOC-generated bpl files
AbsHoudini Postponed Test for abstract houdini
+snapshots Use Tests for program snapshot verification
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer new file mode 100644 index 00000000..aac9cd03 --- /dev/null +++ b/Test/snapshots/Answer @@ -0,0 +1,27 @@ +c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): anon0
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): anon0
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): anon0
+
+Boogie program verifier finished with 0 verified, 4 errors
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
+c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors
+c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
+
+Boogie program verifier finished with 2 verified, 1 error
diff --git a/Test/snapshots/Snapshots0.v0.bpl b/Test/snapshots/Snapshots0.v0.bpl new file mode 100644 index 00000000..c75e9520 --- /dev/null +++ b/Test/snapshots/Snapshots0.v0.bpl @@ -0,0 +1,42 @@ +// id = "P1:0"
+// priority = 3
+// checksum = "123"
+//
+// Action: verify
+procedure {:priority 3} {:checksum "123"} P1()
+{
+ assert false;
+}
+
+
+// id = "P2:0"
+// priority = 3
+// checksum = null
+//
+// Action: verify
+procedure {:priority 3} P2()
+{
+ assert false;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = null
+//
+// Action: verify
+procedure P3()
+{
+ assert false;
+}
+
+
+// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: verify
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+ assert false;
+}
diff --git a/Test/snapshots/Snapshots0.v1.bpl b/Test/snapshots/Snapshots0.v1.bpl new file mode 100644 index 00000000..efd30c8f --- /dev/null +++ b/Test/snapshots/Snapshots0.v1.bpl @@ -0,0 +1,42 @@ +// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: skip
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+ assert false;
+}
+
+
+// id = "P1:0"
+// priority = 5
+// checksum = "234"
+//
+// Action: verify (unknown checksum)
+procedure {:priority 5} {:checksum "234"} P1()
+{
+ assert true;
+}
+
+
+// id = "P2:0"
+// priority = 3
+// checksum = null
+//
+// Action: verify (no checksum)
+procedure {:priority 3} P2()
+{
+ assert false;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: verify (unknown checksum)
+procedure {:checksum "234"} P3()
+{
+ assert true;
+}
diff --git a/Test/snapshots/Snapshots0.v2.bpl b/Test/snapshots/Snapshots0.v2.bpl new file mode 100644 index 00000000..156977f7 --- /dev/null +++ b/Test/snapshots/Snapshots0.v2.bpl @@ -0,0 +1,31 @@ +// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: skip
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+ assert false;
+}
+
+
+// id = "P1:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:priority 1} {:checksum "234"} P1()
+{
+ assert true;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:checksum "234"} P3()
+{
+ assert true;
+}
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat new file mode 100644 index 00000000..05421b85 --- /dev/null +++ b/Test/snapshots/runtest.bat @@ -0,0 +1,7 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BGEXE=%BOOGIEDIR%\Boogie.exe
+
+%BGEXE% %* /verifySnapshots Snapshots0.bpl
|