diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/snapshots/Answer | 18 | ||||
-rw-r--r-- | Test/snapshots/Snapshots1.v0.bpl | 4 | ||||
-rw-r--r-- | Test/snapshots/Snapshots1.v1.bpl | 4 | ||||
-rw-r--r-- | Test/snapshots/Snapshots1.v2.bpl | 4 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v0.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v1.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v2.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v3.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v4.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots2.v5.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots3.v0.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots3.v1.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots4.v0.bpl | 6 | ||||
-rw-r--r-- | Test/snapshots/Snapshots4.v1.bpl | 8 | ||||
-rw-r--r-- | Test/snapshots/Snapshots5.v0.bpl | 11 | ||||
-rw-r--r-- | Test/snapshots/Snapshots5.v1.bpl | 11 | ||||
-rw-r--r-- | Test/snapshots/runtest.bat | 2 |
17 files changed, 62 insertions, 22 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index dc0ee8c1..7826d2f0 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -61,3 +61,21 @@ Execution trace: Snapshots3.v1.bpl(6,1): anon0
Boogie program verifier finished with 0 verified, 1 error
+
+Boogie program verifier finished with 3 verified, 0 errors
+Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots4.v1.bpl(23,5): anon0
+Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
+Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Snapshots4.v1.bpl(33,1): anon0
+
+Boogie program verifier finished with 2 verified, 2 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Snapshots5.v1.bpl(5,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl index d6d4332e..ea2c06bb 100644 --- a/Test/snapshots/Snapshots1.v0.bpl +++ b/Test/snapshots/Snapshots1.v0.bpl @@ -1,6 +1,6 @@ procedure {:checksum "P1$proc#0"} P1();
// Action: verify
-implementation {:checksum "P1$impl#0"} P1()
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
{
call P2();
}
@@ -8,7 +8,7 @@ implementation {:checksum "P1$impl#0"} P1() procedure {:checksum "P2$proc#0"} P2();
// Action: verify
-implementation {:checksum "P2$impl#0"} P2()
+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
{
assert 1 != 1;
}
diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl index c0014a03..9fbe44af 100644 --- a/Test/snapshots/Snapshots1.v1.bpl +++ b/Test/snapshots/Snapshots1.v1.bpl @@ -1,6 +1,6 @@ procedure {:checksum "P1$proc#0"} P1();
// Action: skip
-implementation {:checksum "P1$impl#0"} P1()
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
{
call P2();
}
@@ -8,7 +8,7 @@ implementation {:checksum "P1$impl#0"} P1() procedure {:checksum "P2$proc#0"} P2();
// Action: verify
-implementation {:checksum "P2$impl#1"} P2()
+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
{
assert 2 != 2;
}
diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl index 49e8b389..c699631e 100644 --- a/Test/snapshots/Snapshots1.v2.bpl +++ b/Test/snapshots/Snapshots1.v2.bpl @@ -1,6 +1,6 @@ procedure {:checksum "P1$proc#0"} P1();
// Action: verify
-implementation {:checksum "P1$impl#0"} P1()
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
{
call P2();
}
@@ -9,7 +9,7 @@ implementation {:checksum "P1$impl#0"} P1() procedure {:checksum "P2$proc#1"} P2();
requires false;
// Action: verify
-implementation {:checksum "P2$impl#1"} P2()
+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
{
assert 2 != 2;
}
diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl index 63f1995d..91f05a0d 100644 --- a/Test/snapshots/Snapshots2.v0.bpl +++ b/Test/snapshots/Snapshots2.v0.bpl @@ -1,6 +1,6 @@ procedure {:checksum "P0$proc#0"} P0();
// Action: verify
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl index a00bdecb..1dec4954 100644 --- a/Test/snapshots/Snapshots2.v1.bpl +++ b/Test/snapshots/Snapshots2.v1.bpl @@ -1,6 +1,6 @@ procedure {:checksum "P0$proc#0"} P0();
// Action: skip
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl index 02c5e6df..567191d3 100644 --- a/Test/snapshots/Snapshots2.v2.bpl +++ b/Test/snapshots/Snapshots2.v2.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#2"} P0();
requires F0();
// Action: verify (procedure changed)
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl index 5bf59435..7f6c4a82 100644 --- a/Test/snapshots/Snapshots2.v3.bpl +++ b/Test/snapshots/Snapshots2.v3.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#2"} P0();
requires F0();
// Action: verify (function changed)
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl index 3d11ee27..abbf5e86 100644 --- a/Test/snapshots/Snapshots2.v4.bpl +++ b/Test/snapshots/Snapshots2.v4.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#2"} P0();
requires F0();
// Action: skip
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl index 5ff7bb4d..55d08527 100644 --- a/Test/snapshots/Snapshots2.v5.bpl +++ b/Test/snapshots/Snapshots2.v5.bpl @@ -2,7 +2,7 @@ procedure {:checksum "P0$proc#5"} P0(); requires F0();
ensures F0();
// Action: verify (procedure changed)
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}
diff --git a/Test/snapshots/Snapshots3.v0.bpl b/Test/snapshots/Snapshots3.v0.bpl index 65dd49ff..7ab7aa5c 100644 --- a/Test/snapshots/Snapshots3.v0.bpl +++ b/Test/snapshots/Snapshots3.v0.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#0"} P0();
ensures G();
// Action: verify
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
}
diff --git a/Test/snapshots/Snapshots3.v1.bpl b/Test/snapshots/Snapshots3.v1.bpl index 329382ac..5eb57e78 100644 --- a/Test/snapshots/Snapshots3.v1.bpl +++ b/Test/snapshots/Snapshots3.v1.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#0"} P0();
ensures G();
// Action: verify
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
}
diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl index 430aee99..59a42289 100644 --- a/Test/snapshots/Snapshots4.v0.bpl +++ b/Test/snapshots/Snapshots4.v0.bpl @@ -1,13 +1,13 @@ procedure {:checksum "P0$proc#0"} P0();
// Action: verify
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
}
procedure {:checksum "P1$proc#0"} P1();
// Action: verify
-implementation {:checksum "P1$impl#0"} P1()
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
{
call P2();
}
@@ -19,7 +19,7 @@ procedure {:checksum "P2$proc#0"} P2(); procedure {:checksum "P3$proc#0"} P3();
// Action: verify
-implementation {:checksum "P3$impl#0"} P3()
+implementation {:id "P3"} {:checksum "P3$impl#0"} P3()
{
}
diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl index 025a3f5f..392a1648 100644 --- a/Test/snapshots/Snapshots4.v1.bpl +++ b/Test/snapshots/Snapshots4.v1.bpl @@ -1,7 +1,7 @@ procedure {:checksum "P0$proc#0"} P0();
// Action: skip
// Priority: 0
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
}
@@ -9,7 +9,7 @@ implementation {:checksum "P0$impl#0"} P0() procedure {:checksum "P1$proc#0"} P1();
// Action: verify
// Priority: 1
-implementation {:checksum "P1$impl#0"} P1()
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
{
call P2();
}
@@ -18,7 +18,7 @@ implementation {:checksum "P1$impl#0"} P1() procedure {:checksum "P3$proc#0"} P3();
// Action: verify
// Priority: 2
-implementation {:checksum "P3$impl#1"} P3()
+implementation {:id "P3"} {:checksum "P3$impl#1"} P3()
{
assert false;
}
@@ -28,7 +28,7 @@ procedure {:checksum "P2$proc#0"} P2(); ensures G();
// Action: verify
// Priority: 3
-implementation {:checksum "P2$impl#0"} P2()
+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
{
}
diff --git a/Test/snapshots/Snapshots5.v0.bpl b/Test/snapshots/Snapshots5.v0.bpl new file mode 100644 index 00000000..b8652c7b --- /dev/null +++ b/Test/snapshots/Snapshots5.v0.bpl @@ -0,0 +1,11 @@ +procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
+{
+ assert false;
+}
+
+function {:checksum "F#1"} F(n: int) : bool
+{
+ false
+}
diff --git a/Test/snapshots/Snapshots5.v1.bpl b/Test/snapshots/Snapshots5.v1.bpl new file mode 100644 index 00000000..b42b1576 --- /dev/null +++ b/Test/snapshots/Snapshots5.v1.bpl @@ -0,0 +1,11 @@ +procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
+{
+ assert false;
+}
+
+function {:checksum "F#0"} F(n: int) : bool
+{
+ true
+}
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index e54a19bc..b7cb641a 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -4,5 +4,5 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl
+%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl
|