Enabled "Benchmarks for error messages" lit tests.

The test15/CaptureState.bpl test fails on Linux
using (Z3 4.2) due to additional (but not meaningful)
parentheses in the outputted model.

11 files changed, 153 insertions, 17 deletions

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 229835f4..7a5cb92f 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -12,9 +12,9 @@ tickleBool -> {
   else -> true

 }

 *** END_MODEL

-NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

+NullInModel.bpl(4,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    NullInModel.bpl(2,3): anon0

+    NullInModel.bpl(4,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -30,9 +30,9 @@ tickleBool -> {
   else -> true

 }

 *** END_MODEL

-IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

+IntInModel.bpl(4,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    IntInModel.bpl(2,3): anon0

+    IntInModel.bpl(4,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -51,32 +51,32 @@ tickleBool -> {
   else -> true

 }

 *** END_MODEL

-ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

+ModelTest.bpl(9,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    ModelTest.bpl(3,5): anon0

+    ModelTest.bpl(5,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- InterpretedFunctionTests --------------------

-InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.

+InterpretedFunctionTests.bpl(6,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(2,3): anon0

-InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.

+    InterpretedFunctionTests.bpl(4,3): anon0

+InterpretedFunctionTests.bpl(12,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(8,3): anon0

-InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.

+    InterpretedFunctionTests.bpl(10,3): anon0

+InterpretedFunctionTests.bpl(18,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    InterpretedFunctionTests.bpl(14,3): anon0

+    InterpretedFunctionTests.bpl(16,3): anon0

 

 Boogie program verifier finished with 0 verified, 3 errors

 

 -------------------- CaptureState --------------------

-CaptureState.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.

-CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.

+CaptureState.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.

+CaptureState.bpl(10,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    CaptureState.bpl(12,3): anon0

-    CaptureState.bpl(16,5): anon4_Then

-    CaptureState.bpl(24,5): anon3

+    CaptureState.bpl(14,3): anon0

+    CaptureState.bpl(18,5): anon4_Then

+    CaptureState.bpl(26,5): anon3

 *** MODEL

 $mv_state_const -> 3

 %lbl%@293 -> false

diff --git a/Test/test15/CaptureState.bpl b/Test/test15/CaptureState.bpl
index 7635ecdc..5ed6ddcc 100644
--- a/Test/test15/CaptureState.bpl
+++ b/Test/test15/CaptureState.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s -mv:- > %t

+// RUN: %diff %s.expect %t

 type Ref;

 type FieldName;

 var Heap: [Ref,FieldName]int;

diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect
new file mode 100644
index 00000000..2c8722d9
--- /dev/null
+++ b/Test/test15/CaptureState.bpl.expect
@@ -0,0 +1,63 @@
+CaptureState.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.
+CaptureState.bpl(10,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    CaptureState.bpl(14,3): anon0
+    CaptureState.bpl(18,5): anon4_Then
+    CaptureState.bpl(26,5): anon3
+*** MODEL
+$mv_state_const -> 3
+%lbl%@293 -> false
+%lbl%+112 -> true
+%lbl%+114 -> true
+%lbl%+118 -> true
+%lbl%+148 -> true
+F -> T@FieldName!val!0
+Heap -> T@[Ref,FieldName]Int!val!0
+m -> **m
+m@0 -> -276
+m@1 -> -275
+m@3 -> -275
+r -> **r
+r@0 -> -550
+this -> T@Ref!val!0
+x -> 719
+y -> **y
+Select_[Ref,FieldName]$int -> {
+  T@[Ref,FieldName]Int!val!0 T@Ref!val!0 T@FieldName!val!0 -> -276
+  else -> -276
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+$mv_state -> {
+  3 0 -> true
+  3 1 -> true
+  3 2 -> true
+  3 5 -> true
+  else -> true
+}
+*** STATE <initial>
+  Heap -> T@[Ref,FieldName]Int!val!0
+  this -> T@Ref!val!0
+  x -> 719
+  y -> **y
+  r -> **r
+  m -> **m
+*** END_STATE
+*** STATE top
+*** END_STATE
+*** STATE then
+  m -> -276
+*** END_STATE
+*** STATE postUpdate0
+  m -> -275
+*** END_STATE
+*** STATE end
+  r -> -550
+  m -> 7
+*** END_STATE
+*** END_MODEL
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test15/IntInModel.bpl b/Test/test15/IntInModel.bpl
index 09fc1436..68108e5e 100644
--- a/Test/test15/IntInModel.bpl
+++ b/Test/test15/IntInModel.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -printModel:2 %s > %t

+// RUN: %diff %s.expect %t

 procedure M (i: int) {

   assert i != 0;

 }

diff --git a/Test/test15/IntInModel.bpl.expect b/Test/test15/IntInModel.bpl.expect
new file mode 100644
index 00000000..1350a6f1
--- /dev/null
+++ b/Test/test15/IntInModel.bpl.expect
@@ -0,0 +1,16 @@
+*** MODEL
+%lbl%@39 -> false
+%lbl%+23 -> true
+%lbl%+29 -> true
+i -> 0
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+IntInModel.bpl(4,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    IntInModel.bpl(4,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test15/InterpretedFunctionTests.bpl b/Test/test15/InterpretedFunctionTests.bpl
index ec57ae8e..711a57f3 100644
--- a/Test/test15/InterpretedFunctionTests.bpl
+++ b/Test/test15/InterpretedFunctionTests.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie %s > %t

+// RUN: %diff %s.expect %t

 procedure addition(x: int, y: int) {

   assume x == 1;

   assume y == 2;

diff --git a/Test/test15/InterpretedFunctionTests.bpl.expect b/Test/test15/InterpretedFunctionTests.bpl.expect
new file mode 100644
index 00000000..b539ce86
--- /dev/null
+++ b/Test/test15/InterpretedFunctionTests.bpl.expect
@@ -0,0 +1,11 @@
+InterpretedFunctionTests.bpl(6,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    InterpretedFunctionTests.bpl(4,3): anon0
+InterpretedFunctionTests.bpl(12,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    InterpretedFunctionTests.bpl(10,3): anon0
+InterpretedFunctionTests.bpl(18,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    InterpretedFunctionTests.bpl(16,3): anon0
+
+Boogie program verifier finished with 0 verified, 3 errors
diff --git a/Test/test15/ModelTest.bpl b/Test/test15/ModelTest.bpl
index 6f03d0bd..2f03d3c9 100644
--- a/Test/test15/ModelTest.bpl
+++ b/Test/test15/ModelTest.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -printModel:2 %s > %t

+// RUN: %diff %s.expect %t

 procedure M (s : ref, r : ref) {

   var  i : int, j : int;

   i := 0 + 1;

diff --git a/Test/test15/ModelTest.bpl.expect b/Test/test15/ModelTest.bpl.expect
new file mode 100644
index 00000000..45d3c8aa
--- /dev/null
+++ b/Test/test15/ModelTest.bpl.expect
@@ -0,0 +1,19 @@
+*** MODEL
+%lbl%@147 -> false
+%lbl%+64 -> true
+%lbl%+84 -> true
+i@0 -> 1
+j@0 -> 2
+j@1 -> 3
+j@2 -> 4
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+ModelTest.bpl(9,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    ModelTest.bpl(5,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test15/NullInModel.bpl b/Test/test15/NullInModel.bpl
index 67c34e3d..6bac5c73 100644
--- a/Test/test15/NullInModel.bpl
+++ b/Test/test15/NullInModel.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -printModel:2 %s > %t

+// RUN: %diff %s.expect %t

 procedure M (s: ref) {

   assert s != null;

 }

diff --git a/Test/test15/NullInModel.bpl.expect b/Test/test15/NullInModel.bpl.expect
new file mode 100644
index 00000000..299aef12
--- /dev/null
+++ b/Test/test15/NullInModel.bpl.expect
@@ -0,0 +1,17 @@
+*** MODEL
+%lbl%@47 -> false
+%lbl%+24 -> true
+%lbl%+37 -> true
+null -> T@ref!val!0
+s -> T@ref!val!0
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+NullInModel.bpl(4,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    NullInModel.bpl(4,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error