diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:10:41 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-07 20:10:41 +0100 |
| commit | 5bd01834f018249e5d27350ae3cfdf8dd6896637 (patch) | |
| tree | fb0aa7b1afe693f20b93dcd7071d548afd2824f5 /Test | |
| parent | f45eb9f44f32cbab80e0aaaff167f6b60b9abbc3 (diff) | |
Enable codeexpr lit tests.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/codeexpr/Answer | 26 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr0.bpl | 2 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr0.bpl.expect | 11 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr1.bpl | 2 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr1.bpl.expect | 12 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr2.bpl | 2 | ||||
| -rw-r--r-- | Test/codeexpr/CodeExpr2.bpl.expect | 2 |
7 files changed, 44 insertions, 13 deletions
diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer index 9c22ca61..15cced53 100644 --- a/Test/codeexpr/Answer +++ b/Test/codeexpr/Answer @@ -1,28 +1,28 @@ ------------------------------ CodeExpr0.bpl ---------------------
-CodeExpr0.bpl(15,3): Error BP5001: This assertion might not hold.
+CodeExpr0.bpl(17,3): Error BP5001: This assertion might not hold.
Execution trace:
- CodeExpr0.bpl(15,3): anon0
-CodeExpr0.bpl(20,3): Error BP5001: This assertion might not hold.
+ CodeExpr0.bpl(17,3): anon0
+CodeExpr0.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- CodeExpr0.bpl(20,3): anon0
-CodeExpr0.bpl(52,3): Error BP5001: This assertion might not hold.
+ CodeExpr0.bpl(22,3): anon0
+CodeExpr0.bpl(54,3): Error BP5001: This assertion might not hold.
Execution trace:
- CodeExpr0.bpl(52,3): anon0
+ CodeExpr0.bpl(54,3): anon0
Boogie program verifier finished with 3 verified, 3 errors
------------------------------ CodeExpr1.bpl ---------------------
-CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold on this return path.
-CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.
+CodeExpr1.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
+CodeExpr1.bpl(42,3): Related location: This is the postcondition that might not hold.
Execution trace:
- CodeExpr1.bpl(42,3): start
-CodeExpr1.bpl(52,5): Error BP5001: This assertion might not hold.
+ CodeExpr1.bpl(44,3): start
+CodeExpr1.bpl(54,5): Error BP5001: This assertion might not hold.
Execution trace:
- CodeExpr1.bpl(49,3): start
-CodeExpr1.bpl(66,5): Error BP5001: This assertion might not hold.
+ CodeExpr1.bpl(51,3): start
+CodeExpr1.bpl(68,5): Error BP5001: This assertion might not hold.
Execution trace:
- CodeExpr1.bpl(57,3): start
+ CodeExpr1.bpl(59,3): start
Boogie program verifier finished with 3 verified, 3 errors
diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl index 62a4225f..58568cea 100644 --- a/Test/codeexpr/CodeExpr0.bpl +++ b/Test/codeexpr/CodeExpr0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
procedure P()
{
assert |{ A: return true; }|;
diff --git a/Test/codeexpr/CodeExpr0.bpl.expect b/Test/codeexpr/CodeExpr0.bpl.expect new file mode 100644 index 00000000..82e7e61f --- /dev/null +++ b/Test/codeexpr/CodeExpr0.bpl.expect @@ -0,0 +1,11 @@ +CodeExpr0.bpl(17,3): Error BP5001: This assertion might not hold. +Execution trace: + CodeExpr0.bpl(17,3): anon0 +CodeExpr0.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + CodeExpr0.bpl(22,3): anon0 +CodeExpr0.bpl(54,3): Error BP5001: This assertion might not hold. +Execution trace: + CodeExpr0.bpl(54,3): anon0 + +Boogie program verifier finished with 3 verified, 3 errors diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl index 3cc92333..20617cc8 100644 --- a/Test/codeexpr/CodeExpr1.bpl +++ b/Test/codeexpr/CodeExpr1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// ------ the good ------
procedure F(x: int, y: int) returns (z: bool)
diff --git a/Test/codeexpr/CodeExpr1.bpl.expect b/Test/codeexpr/CodeExpr1.bpl.expect new file mode 100644 index 00000000..b3960bca --- /dev/null +++ b/Test/codeexpr/CodeExpr1.bpl.expect @@ -0,0 +1,12 @@ +CodeExpr1.bpl(46,5): Error BP5003: A postcondition might not hold on this return path. +CodeExpr1.bpl(42,3): Related location: This is the postcondition that might not hold. +Execution trace: + CodeExpr1.bpl(44,3): start +CodeExpr1.bpl(54,5): Error BP5001: This assertion might not hold. +Execution trace: + CodeExpr1.bpl(51,3): start +CodeExpr1.bpl(68,5): Error BP5001: This assertion might not hold. +Execution trace: + CodeExpr1.bpl(59,3): start + +Boogie program verifier finished with 3 verified, 3 errors diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl index 61758d5a..f42ed4f2 100644 --- a/Test/codeexpr/CodeExpr2.bpl +++ b/Test/codeexpr/CodeExpr2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
type T;
const zero: T;
diff --git a/Test/codeexpr/CodeExpr2.bpl.expect b/Test/codeexpr/CodeExpr2.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/codeexpr/CodeExpr2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors |