Enable codeexpr lit tests.

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