summaryrefslogtreecommitdiff
path: root/Test/test0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0')
-rw-r--r--Test/test0/Answer156
-rw-r--r--Test/test0/Arrays0.bpl2
-rw-r--r--Test/test0/Arrays1.bpl2
-rw-r--r--Test/test0/Arrays1.bpl.expect3
-rw-r--r--Test/test0/AttributeParsing.bpl2
-rw-r--r--Test/test0/AttributeParsing.bpl.expect46
-rw-r--r--Test/test0/AttributeParsingErr.bpl2
-rw-r--r--Test/test0/AttributeParsingErr.bpl.expect10
-rw-r--r--Test/test0/AttributeResolution.bpl2
-rw-r--r--Test/test0/AttributeResolution.bpl.expect10
-rw-r--r--Test/test0/BadLabels0.bpl2
-rw-r--r--Test/test0/BadLabels0.bpl.expect3
-rw-r--r--Test/test0/BadLabels1.bpl2
-rw-r--r--Test/test0/BadLabels1.bpl.expect9
-rw-r--r--Test/test0/BadQuantifier.bpl2
-rw-r--r--Test/test0/BadQuantifier.bpl.expect2
-rw-r--r--Test/test0/EmptyCallArgs.bpl4
-rw-r--r--Test/test0/LargeLiterals0.bpl2
-rw-r--r--Test/test0/LineParse.bpl2
-rw-r--r--Test/test0/LineParse.bpl.expect6
-rw-r--r--Test/test0/LineResolve.bpl2
-rw-r--r--Test/test0/LineResolve.bpl.expect13
-rw-r--r--Test/test0/MapsResolutionErrors.bpl2
-rw-r--r--Test/test0/MapsResolutionErrors.bpl.expect3
-rw-r--r--Test/test0/ModifiedBag.bpl2
-rw-r--r--Test/test0/NoErrors.expect2
-rw-r--r--Test/test0/Orderings.bpl2
-rw-r--r--Test/test0/Orderings.bpl.expect5
-rw-r--r--Test/test0/PrettyPrint.bpl2
-rw-r--r--Test/test0/PrettyPrint.bpl.expect93
-rw-r--r--Test/test0/Prog0.bpl2
-rw-r--r--Test/test0/Quoting.bpl2
-rw-r--r--Test/test0/Quoting.bpl.expect35
-rw-r--r--Test/test0/SeparateVerification0.bpl6
-rw-r--r--Test/test0/SeparateVerification0.bpl.expect2
-rw-r--r--Test/test0/SeparateVerification1.bpl2
-rw-r--r--Test/test0/SeparateVerification1.bpl.expect3
-rw-r--r--Test/test0/Triggers0.bpl2
-rw-r--r--Test/test0/Triggers0.bpl.expect2
-rw-r--r--Test/test0/Triggers1.bpl2
-rw-r--r--Test/test0/Triggers1.bpl.expect21
-rw-r--r--Test/test0/Types0.bpl2
-rw-r--r--Test/test0/Types0.bpl.expect3
-rw-r--r--Test/test0/Types1.bpl2
-rw-r--r--Test/test0/Types1.bpl.expect4
-rw-r--r--Test/test0/WhereParsing.bpl2
-rw-r--r--Test/test0/WhereParsing.bpl.expect4
-rw-r--r--Test/test0/WhereParsing0.bpl2
-rw-r--r--Test/test0/WhereParsing0.bpl.expect3
-rw-r--r--Test/test0/WhereParsing1.bpl2
-rw-r--r--Test/test0/WhereParsing1.bpl.expect2
-rw-r--r--Test/test0/WhereParsing2.bpl2
-rw-r--r--Test/test0/WhereParsing2.bpl.expect2
-rw-r--r--Test/test0/WhereResolution.bpl2
-rw-r--r--Test/test0/WhereResolution.bpl.expect3
55 files changed, 430 insertions, 79 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer
index f4e2b981..51798f57 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -2,28 +2,28 @@
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Triggers0.bpl(14,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
+Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
1 parse errors detected in Triggers0.bpl
-Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(15,9): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(19,10): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(23,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(27,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(32,17): Error: equality is not allowed in triggers
-Triggers1.bpl(36,17): Error: arithmetic comparisons are not allowed in triggers
-Triggers1.bpl(45,10): Error: quantifiers are not allowed in triggers
-Triggers1.bpl(53,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(61,7): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(62,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(70,9): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g
-Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1
-Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0
+Triggers1.bpl(9,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(13,21): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(17,9): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(21,10): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(25,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(29,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(34,17): Error: equality is not allowed in triggers
+Triggers1.bpl(38,17): Error: arithmetic comparisons are not allowed in triggers
+Triggers1.bpl(47,10): Error: quantifiers are not allowed in triggers
+Triggers1.bpl(55,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(63,7): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(64,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(72,9): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(84,7): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(96,16): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(97,16): Error: a matching pattern must be more than just a variable by itself: g
+Triggers1.bpl(107,40): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(121,33): Error: cannot refer to a global variable in this context: h1
+Triggers1.bpl(122,33): Error: cannot refer to a global variable in this context: h0
20 name resolution errors detected in Triggers1.bpl
const x: int;
@@ -120,50 +120,50 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
-Types0.bpl(6,18): error: expected identifier before ':'
-Types0.bpl(6,12): error: expecting an identifier as parameter name
+Types0.bpl(8,18): error: expected identifier before ':'
+Types0.bpl(8,12): error: expecting an identifier as parameter name
2 parse errors detected in Types0.bpl
-Types1.bpl(6,11): Error: undeclared type: x
-Types1.bpl(7,11): Error: undeclared type: x
-Types1.bpl(7,14): Error: undeclared type: x
+Types1.bpl(8,11): Error: undeclared type: x
+Types1.bpl(9,11): Error: undeclared type: x
+Types1.bpl(9,14): Error: undeclared type: x
3 name resolution errors detected in Types1.bpl
-WhereParsing.bpl(14,37): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(15,33): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(32,38): error: attributes are not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(16,37): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(17,33): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(34,38): error: attributes are not allowed on the 'implementation' copies of formals
3 parse errors detected in WhereParsing.bpl
-WhereParsing0.bpl(17,38): error: where clause not allowed on bound variables
-WhereParsing0.bpl(18,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(19,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(20,38): error: where clause not allowed on bound variables
2 parse errors detected in WhereParsing0.bpl
-WhereParsing1.bpl(14,27): error: ")" expected
+WhereParsing1.bpl(16,27): error: ")" expected
1 parse errors detected in WhereParsing1.bpl
-WhereParsing2.bpl(1,14): error: ";" expected
+WhereParsing2.bpl(3,14): error: ";" expected
1 parse errors detected in WhereParsing2.bpl
-WhereResolution.bpl(28,38): Error: undeclared identifier: alpha
-WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts
+WhereResolution.bpl(30,38): Error: undeclared identifier: alpha
+WhereResolution.bpl(34,30): Error: old expressions allowed only in two-state contexts
2 name resolution errors detected in WhereResolution.bpl
-BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
-BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
+BadLabels0.bpl(6,2): Error: more than one declaration of block name: X
+BadLabels0.bpl(13,4): Error: more than one declaration of block name: Y
2 name resolution errors detected in BadLabels0.bpl
-BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined
-BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined
-BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
-BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
-BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
-BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
-BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
-BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
+BadLabels1.bpl(6,3): error: Error: goto label 'X' is undefined
+BadLabels1.bpl(7,3): error: Error: goto label 'Y' is undefined
+BadLabels1.bpl(49,3): error: Error: break statement is not inside a loop
+BadLabels1.bpl(51,5): error: Error: break statement is not inside a loop
+BadLabels1.bpl(62,5): error: Error: break label 'B' must designate an enclosing statement
+BadLabels1.bpl(65,5): error: Error: break label 'A' must designate an enclosing statement
+BadLabels1.bpl(66,5): error: Error: break label 'C' must designate an enclosing statement
+BadLabels1.bpl(67,8): error: Error: break label 'F' must designate an enclosing statement
8 parse errors detected in BadLabels1.bpl
-LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
-LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(4,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
LineParse.bpl(6,2): error: EOF expected
5 parse errors detected in LineParse.bpl
-LineResolve.bpl(5,1): Error: undeclared identifier: a
-LineResolve.bpl(7,2): Error: undeclared identifier: b
+LineResolve.bpl(7,1): Error: undeclared identifier: a
+LineResolve.bpl(9,2): Error: undeclared identifier: b
LineResolve.bpl(12,0): Error: undeclared identifier: c
LineResolve.bpl(13,10): Error: undeclared identifier: d
LineResolve.bpl(12,0): Error: undeclared identifier: e
@@ -175,15 +175,15 @@ Abc.txt(99,0): Error: undeclared identifier: j
c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
A B C . txt(12,0): Error: undeclared identifier: l
12 name resolution errors detected in LineResolve.bpl
-AttributeParsingErr.bpl(1,33): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(5,52): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(7,37): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(9,31): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(11,29): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(13,13): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(15,18): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(20,26): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(5,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(7,52): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(9,37): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(11,31): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(13,29): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(15,13): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(17,18): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(22,26): error: only attributes, not triggers, allowed here
9 parse errors detected in AttributeParsingErr.bpl
type {:sourcefile "test.ssc"} T;
@@ -231,15 +231,15 @@ procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();
const again: int;
Boogie program verifier finished with 0 verified, 0 errors
-AttributeResolution.bpl(1,18): Error: undeclared identifier: foo
-AttributeResolution.bpl(3,18): Error: undeclared identifier: bar
-AttributeResolution.bpl(7,15): Error: undeclared identifier: qux
-AttributeResolution.bpl(7,41): Error: undeclared identifier: ij
-AttributeResolution.bpl(13,21): Error: undeclared identifier: bzzt
-AttributeResolution.bpl(15,20): Error: undeclared identifier: blt
-AttributeResolution.bpl(5,20): Error: undeclared identifier: baz
-AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
-AttributeResolution.bpl(11,29): Error: undeclared identifier: fux
+AttributeResolution.bpl(3,18): Error: undeclared identifier: foo
+AttributeResolution.bpl(5,18): Error: undeclared identifier: bar
+AttributeResolution.bpl(9,15): Error: undeclared identifier: qux
+AttributeResolution.bpl(9,41): Error: undeclared identifier: ij
+AttributeResolution.bpl(15,21): Error: undeclared identifier: bzzt
+AttributeResolution.bpl(17,20): Error: undeclared identifier: blt
+AttributeResolution.bpl(7,20): Error: undeclared identifier: baz
+AttributeResolution.bpl(11,18): Error: undeclared identifier: mux
+AttributeResolution.bpl(13,29): Error: undeclared identifier: fux
9 name resolution errors detected in AttributeResolution.bpl
function \true() : bool;
@@ -278,24 +278,24 @@ implementation qux(a: \procedure)
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-MapsResolutionErrors.bpl(6,9): Error: type variable must occur in map arguments: b
-MapsResolutionErrors.bpl(20,10): Error: type variable must occur in procedure arguments: a
+MapsResolutionErrors.bpl(8,9): Error: type variable must occur in map arguments: b
+MapsResolutionErrors.bpl(22,10): Error: type variable must occur in procedure arguments: a
2 name resolution errors detected in MapsResolutionErrors.bpl
-Orderings.bpl(12,20): Error: undeclared identifier: x
-Orderings.bpl(15,23): Error: c0 occurs more than once as parent
-Orderings.bpl(16,19): Error: constant cannot be its own parent
-Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
+Orderings.bpl(14,20): Error: undeclared identifier: x
+Orderings.bpl(17,23): Error: c0 occurs more than once as parent
+Orderings.bpl(18,19): Error: constant cannot be its own parent
+Orderings.bpl(20,20): Error: the parent of a constant has to be a constant
4 name resolution errors detected in Orderings.bpl
-BadQuantifier.bpl(3,15): error: invalid QuantifierBody
+BadQuantifier.bpl(5,15): error: invalid QuantifierBody
1 parse errors detected in BadQuantifier.bpl
Boogie program verifier finished with 0 verified, 0 errors
----- SeparateVerification0.bpl
-SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
+SeparateVerification0.bpl(19,6): Error: undeclared identifier: y
1 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification1.bpl SeparateVerification0.bpl
-SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
-SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
+SeparateVerification1.bpl(6,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(16,6): Error: undeclared identifier: x
2 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification0.bpl SeparateVerification0.bpl
diff --git a/Test/test0/Arrays0.bpl b/Test/test0/Arrays0.bpl
index 0098c4a8..59ff8d14 100644
--- a/Test/test0/Arrays0.bpl
+++ b/Test/test0/Arrays0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
var one: [int]int;
var two: [int,int]int;
var three: [int,int,int]int; // three's a crowd
diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl
index db12ecb3..1f4b693c 100644
--- a/Test/test0/Arrays1.bpl
+++ b/Test/test0/Arrays1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
var Q: [int,int][int]int;
procedure P()
diff --git a/Test/test0/Arrays1.bpl.expect b/Test/test0/Arrays1.bpl.expect
new file mode 100644
index 00000000..534096ac
--- /dev/null
+++ b/Test/test0/Arrays1.bpl.expect
@@ -0,0 +1,3 @@
+Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+2 type checking errors detected in Arrays1.bpl
diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl
index e2b6101c..0b99dc5f 100644
--- a/Test/test0/AttributeParsing.bpl
+++ b/Test/test0/AttributeParsing.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify -print:- -env:0 %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile "test.ssc"} T;
function {:source "test.scc"} f(int) returns (int);
diff --git a/Test/test0/AttributeParsing.bpl.expect b/Test/test0/AttributeParsing.bpl.expect
new file mode 100644
index 00000000..c2d0289a
--- /dev/null
+++ b/Test/test0/AttributeParsing.bpl.expect
@@ -0,0 +1,46 @@
+
+type {:sourcefile "test.ssc"} T;
+
+function {:source "test.scc"} f(int) : int;
+
+const {:description "The largest integer value"} unique MAXINT: int;
+
+axiom {:naming "MyFavoriteAxiom"} (forall i: int :: { f(i) } f(i) == i + 1);
+
+var {:description "memory"} $Heap: [ref,name]any;
+
+var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref,name]any;
+
+procedure {:use_impl 1} foo(x: int) returns (n: int);
+
+
+
+implementation {:id 1} foo(x: int) returns (n: int)
+{
+ block1:
+ return;
+}
+
+
+
+implementation {:id 2} foo(x: int) returns (n: int)
+{
+ block1:
+ return;
+}
+
+
+
+type ref;
+
+type any;
+
+type name;
+
+procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();
+
+
+
+const again: int;
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/AttributeParsingErr.bpl b/Test/test0/AttributeParsingErr.bpl
index cdf8646f..7329289f 100644
--- a/Test/test0/AttributeParsingErr.bpl
+++ b/Test/test0/AttributeParsingErr.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile "test.ssc"} {1} T;
function {:source "test.scc"} {1} f(int) returns (int);
diff --git a/Test/test0/AttributeParsingErr.bpl.expect b/Test/test0/AttributeParsingErr.bpl.expect
new file mode 100644
index 00000000..4fef56ed
--- /dev/null
+++ b/Test/test0/AttributeParsingErr.bpl.expect
@@ -0,0 +1,10 @@
+AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(5,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(7,52): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(9,37): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(11,31): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(13,29): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(15,13): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(17,18): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(22,26): error: only attributes, not triggers, allowed here
+9 parse errors detected in AttributeParsingErr.bpl
diff --git a/Test/test0/AttributeResolution.bpl b/Test/test0/AttributeResolution.bpl
index c667b530..eae2878e 100644
--- a/Test/test0/AttributeResolution.bpl
+++ b/Test/test0/AttributeResolution.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile foo} T;
function {:source bar} f(int) returns (int);
diff --git a/Test/test0/AttributeResolution.bpl.expect b/Test/test0/AttributeResolution.bpl.expect
new file mode 100644
index 00000000..1a7a43fa
--- /dev/null
+++ b/Test/test0/AttributeResolution.bpl.expect
@@ -0,0 +1,10 @@
+AttributeResolution.bpl(3,18): Error: undeclared identifier: foo
+AttributeResolution.bpl(5,18): Error: undeclared identifier: bar
+AttributeResolution.bpl(9,15): Error: undeclared identifier: qux
+AttributeResolution.bpl(9,41): Error: undeclared identifier: ij
+AttributeResolution.bpl(15,21): Error: undeclared identifier: bzzt
+AttributeResolution.bpl(17,20): Error: undeclared identifier: blt
+AttributeResolution.bpl(7,20): Error: undeclared identifier: baz
+AttributeResolution.bpl(11,18): Error: undeclared identifier: mux
+AttributeResolution.bpl(13,29): Error: undeclared identifier: fux
+9 name resolution errors detected in AttributeResolution.bpl
diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl
index 89cf7a36..ec6ff744 100644
--- a/Test/test0/BadLabels0.bpl
+++ b/Test/test0/BadLabels0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure Dup(y: int)
{
X:
diff --git a/Test/test0/BadLabels0.bpl.expect b/Test/test0/BadLabels0.bpl.expect
new file mode 100644
index 00000000..619a88e8
--- /dev/null
+++ b/Test/test0/BadLabels0.bpl.expect
@@ -0,0 +1,3 @@
+BadLabels0.bpl(6,2): Error: more than one declaration of block name: X
+BadLabels0.bpl(13,4): Error: more than one declaration of block name: Y
+2 name resolution errors detected in BadLabels0.bpl
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl
index c040ce26..cbbe0f5e 100644
--- a/Test/test0/BadLabels1.bpl
+++ b/Test/test0/BadLabels1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure P0()
{
// these labels don't exist at all
diff --git a/Test/test0/BadLabels1.bpl.expect b/Test/test0/BadLabels1.bpl.expect
new file mode 100644
index 00000000..e722a1b1
--- /dev/null
+++ b/Test/test0/BadLabels1.bpl.expect
@@ -0,0 +1,9 @@
+BadLabels1.bpl(6,3): error: Error: goto label 'X' is undefined
+BadLabels1.bpl(7,3): error: Error: goto label 'Y' is undefined
+BadLabels1.bpl(49,3): error: Error: break statement is not inside a loop
+BadLabels1.bpl(51,5): error: Error: break statement is not inside a loop
+BadLabels1.bpl(62,5): error: Error: break label 'B' must designate an enclosing statement
+BadLabels1.bpl(65,5): error: Error: break label 'A' must designate an enclosing statement
+BadLabels1.bpl(66,5): error: Error: break label 'C' must designate an enclosing statement
+BadLabels1.bpl(67,8): error: Error: break label 'F' must designate an enclosing statement
+8 parse errors detected in BadLabels1.bpl
diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl
index b06ab0d9..d202312e 100644
--- a/Test/test0/BadQuantifier.bpl
+++ b/Test/test0/BadQuantifier.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
function f(int) returns (bool);
axiom (forall int x :: f(x) <== x >= 0);
diff --git a/Test/test0/BadQuantifier.bpl.expect b/Test/test0/BadQuantifier.bpl.expect
new file mode 100644
index 00000000..bf16fef7
--- /dev/null
+++ b/Test/test0/BadQuantifier.bpl.expect
@@ -0,0 +1,2 @@
+BadQuantifier.bpl(5,15): error: invalid QuantifierBody
+1 parse errors detected in BadQuantifier.bpl
diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl
index d45633e9..aba48668 100644
--- a/Test/test0/EmptyCallArgs.bpl
+++ b/Test/test0/EmptyCallArgs.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
type C;
procedure P(x:int, y:bool) returns (z:C);
@@ -17,4 +19,4 @@ procedure CallQ() {
var z:bool;
call z := Q(x, y);
-} \ No newline at end of file
+}
diff --git a/Test/test0/LargeLiterals0.bpl b/Test/test0/LargeLiterals0.bpl
index be459bf5..b061688f 100644
--- a/Test/test0/LargeLiterals0.bpl
+++ b/Test/test0/LargeLiterals0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// Test to parse large integer literals
axiom 1234567890987654321 == 1234567890987654321;
diff --git a/Test/test0/LineParse.bpl b/Test/test0/LineParse.bpl
index a64eed0b..ae11b419 100644
--- a/Test/test0/LineParse.bpl
+++ b/Test/test0/LineParse.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
#line
#line
#line 0
diff --git a/Test/test0/LineParse.bpl.expect b/Test/test0/LineParse.bpl.expect
new file mode 100644
index 00000000..668e57dc
--- /dev/null
+++ b/Test/test0/LineParse.bpl.expect
@@ -0,0 +1,6 @@
+LineParse.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(4,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
+LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
+LineParse.bpl(6,2): error: EOF expected
+5 parse errors detected in LineParse.bpl
diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl
index b0c578c7..097943f5 100644
--- a/Test/test0/LineResolve.bpl
+++ b/Test/test0/LineResolve.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure P() {
var x: int;
x :=
diff --git a/Test/test0/LineResolve.bpl.expect b/Test/test0/LineResolve.bpl.expect
new file mode 100644
index 00000000..6ca45551
--- /dev/null
+++ b/Test/test0/LineResolve.bpl.expect
@@ -0,0 +1,13 @@
+LineResolve.bpl(7,1): Error: undeclared identifier: a
+LineResolve.bpl(9,2): Error: undeclared identifier: b
+LineResolve.bpl(12,0): Error: undeclared identifier: c
+LineResolve.bpl(13,10): Error: undeclared identifier: d
+LineResolve.bpl(12,0): Error: undeclared identifier: e
+LineResolve.bpl(2,0): Error: undeclared identifier: f
+LineResolve.bpl(900,0): Error: undeclared identifier: g
+Abc.txt(11,3): Error: undeclared identifier: h
+Abc.txt(13,0): Error: undeclared identifier: i
+Abc.txt(99,0): Error: undeclared identifier: j
+c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
+A B C . txt(12,0): Error: undeclared identifier: l
+12 name resolution errors detected in LineResolve.bpl
diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl
index d529cb9c..8e5d5149 100644
--- a/Test/test0/MapsResolutionErrors.bpl
+++ b/Test/test0/MapsResolutionErrors.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
var m: []int;
var p: <a>[]a;
diff --git a/Test/test0/MapsResolutionErrors.bpl.expect b/Test/test0/MapsResolutionErrors.bpl.expect
new file mode 100644
index 00000000..10070c23
--- /dev/null
+++ b/Test/test0/MapsResolutionErrors.bpl.expect
@@ -0,0 +1,3 @@
+MapsResolutionErrors.bpl(8,9): Error: type variable must occur in map arguments: b
+MapsResolutionErrors.bpl(22,10): Error: type variable must occur in procedure arguments: a
+2 name resolution errors detected in MapsResolutionErrors.bpl
diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
index 5fffc20a..05ab3c05 100644
--- a/Test/test0/ModifiedBag.bpl
+++ b/Test/test0/ModifiedBag.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// ----------- BEGIN PRELUDE
diff --git a/Test/test0/NoErrors.expect b/Test/test0/NoErrors.expect
new file mode 100644
index 00000000..cc5cde4d
--- /dev/null
+++ b/Test/test0/NoErrors.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl
index 0ba6c69c..b14dbd4b 100644
--- a/Test/test0/Orderings.bpl
+++ b/Test/test0/Orderings.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type C;
diff --git a/Test/test0/Orderings.bpl.expect b/Test/test0/Orderings.bpl.expect
new file mode 100644
index 00000000..d58cdc46
--- /dev/null
+++ b/Test/test0/Orderings.bpl.expect
@@ -0,0 +1,5 @@
+Orderings.bpl(14,20): Error: undeclared identifier: x
+Orderings.bpl(17,23): Error: c0 occurs more than once as parent
+Orderings.bpl(18,19): Error: constant cannot be its own parent
+Orderings.bpl(20,20): Error: the parent of a constant has to be a constant
+4 name resolution errors detected in Orderings.bpl
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index 7e4a9ce7..bc22e46d 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify -printInstrumented %s > %t
+// RUN: %diff %s.expect %t
const x: int;
const y: int;
const z: int;
diff --git a/Test/test0/PrettyPrint.bpl.expect b/Test/test0/PrettyPrint.bpl.expect
new file mode 100644
index 00000000..f6f0f995
--- /dev/null
+++ b/Test/test0/PrettyPrint.bpl.expect
@@ -0,0 +1,93 @@
+const x: int;
+
+const y: int;
+
+const z: int;
+
+const r: real;
+
+const s: real;
+
+const t: real;
+
+const P: bool;
+
+const Q: bool;
+
+const R: bool;
+
+axiom x * (y + z) == x + y * z;
+
+axiom x * y + z == (x + y) * z;
+
+axiom x * y * z == x * y * z;
+
+axiom x * y * z * x == x * y * z;
+
+axiom x div y div z == x div (y div z);
+
+axiom x div y div (z div x) == x div y div z;
+
+axiom x + y mod z == y mod z + x;
+
+axiom (x + y) mod z == x mod z + y mod z;
+
+axiom x / y / z == x / (y / z);
+
+axiom x / y / (z / x) == x / y / z;
+
+axiom x / s / z == x / (s / z);
+
+axiom x / s / (z / x) == x / s / z;
+
+axiom r / s / t == r / (s / t);
+
+axiom r / s / (t / r) == r / s / t;
+
+axiom r * s / t == r * s / t;
+
+axiom r / s * t == r / s * t;
+
+axiom (r * s) ** t == r ** t * s ** t;
+
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+
+axiom r >= 0e0 ==> real(int(r)) <= r;
+
+axiom int(0e0 - 2e-2) == 0;
+
+axiom int(0e0 - 35e0) == -35;
+
+axiom int(27e-1) == 2;
+
+axiom x - y - z == x - (y - z);
+
+axiom x - y - (z - x) == x - y - z;
+
+axiom x + y - z - x + y == 0;
+
+axiom x + y - z - x + y == x + y - (z - (x + y));
+
+axiom P ==> Q ==> R <==> P ==> Q ==> R;
+
+axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R;
+
+axiom P <==> Q <==> R;
+
+axiom P ==> Q <==> Q ==> R <==> R ==> P;
+
+axiom (P && Q) || (Q && R);
+
+axiom (P || Q) && (Q || R);
+
+axiom P || Q || Q || R;
+
+axiom P && Q && Q && R;
+
+function f(int) : int;
+
+axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl
index 79a4d2ab..974bd9eb 100644
--- a/Test/test0/Prog0.bpl
+++ b/Test/test0/Prog0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// BoogiePL Examples
type elements;
diff --git a/Test/test0/Quoting.bpl b/Test/test0/Quoting.bpl
index eaf8fe7a..64564ad9 100644
--- a/Test/test0/Quoting.bpl
+++ b/Test/test0/Quoting.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify -print:- -env:0 %s > %t
+// RUN: %diff %s.expect %t
function \true() returns(bool);
type \procedure;
diff --git a/Test/test0/Quoting.bpl.expect b/Test/test0/Quoting.bpl.expect
new file mode 100644
index 00000000..3a1037aa
--- /dev/null
+++ b/Test/test0/Quoting.bpl.expect
@@ -0,0 +1,35 @@
+
+function \true() : bool;
+
+type \procedure;
+
+procedure \old(any: \procedure) returns (\var: \procedure);
+
+
+
+implementation \old(any: \procedure) returns (\var: \procedure)
+{
+ var \modifies: \procedure;
+
+ \modifies := any;
+ \var := \modifies;
+}
+
+
+
+procedure qux(a: \procedure);
+
+
+
+implementation qux(a: \procedure)
+{
+ var \var: \procedure;
+ var x: bool;
+
+ call \var := \old(a);
+ x := \true();
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl
index 5a8ef283..f598fe6f 100644
--- a/Test/test0/SeparateVerification0.bpl
+++ b/Test/test0/SeparateVerification0.bpl
@@ -1,3 +1,9 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
+// RUN: %boogie -noVerify %s %s > %t
+// RUN: %diff NoErrors.expect %t
+// RUN: %boogie -noVerify %s %s SeparateVerification1.bpl > %t
+// RUN: %diff NoErrors.expect %t
// need to include this file twice for it to include all necessary declarations
#if FILE_0
diff --git a/Test/test0/SeparateVerification0.bpl.expect b/Test/test0/SeparateVerification0.bpl.expect
new file mode 100644
index 00000000..ab1318bd
--- /dev/null
+++ b/Test/test0/SeparateVerification0.bpl.expect
@@ -0,0 +1,2 @@
+SeparateVerification0.bpl(19,6): Error: undeclared identifier: y
+1 name resolution errors detected in SeparateVerification0.bpl
diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl
index 0e3e7926..683b24e1 100644
--- a/Test/test0/SeparateVerification1.bpl
+++ b/Test/test0/SeparateVerification1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s SeparateVerification0.bpl > %t
+// RUN: %diff %s.expect %t
// to be used with SeparateVerification0.bpl
// x and y are declared in SeparateVerification0.bpl
diff --git a/Test/test0/SeparateVerification1.bpl.expect b/Test/test0/SeparateVerification1.bpl.expect
new file mode 100644
index 00000000..48b21162
--- /dev/null
+++ b/Test/test0/SeparateVerification1.bpl.expect
@@ -0,0 +1,3 @@
+SeparateVerification1.bpl(6,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(16,6): Error: undeclared identifier: x
+2 name resolution errors detected in SeparateVerification0.bpl
diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl
index 6750d77d..bbf37517 100644
--- a/Test/test0/Triggers0.bpl
+++ b/Test/test0/Triggers0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
// Trigger errors
function f(int, int) returns (int);
diff --git a/Test/test0/Triggers0.bpl.expect b/Test/test0/Triggers0.bpl.expect
new file mode 100644
index 00000000..72ee6160
--- /dev/null
+++ b/Test/test0/Triggers0.bpl.expect
@@ -0,0 +1,2 @@
+Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
+1 parse errors detected in Triggers0.bpl
diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl
index d079ea03..bda65ea2 100644
--- a/Test/test0/Triggers1.bpl
+++ b/Test/test0/Triggers1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
// Trigger errors
function f(int, int) returns (int);
diff --git a/Test/test0/Triggers1.bpl.expect b/Test/test0/Triggers1.bpl.expect
new file mode 100644
index 00000000..d7ede824
--- /dev/null
+++ b/Test/test0/Triggers1.bpl.expect
@@ -0,0 +1,21 @@
+Triggers1.bpl(9,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(13,21): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(17,9): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(21,10): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(25,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(29,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(34,17): Error: equality is not allowed in triggers
+Triggers1.bpl(38,17): Error: arithmetic comparisons are not allowed in triggers
+Triggers1.bpl(47,10): Error: quantifiers are not allowed in triggers
+Triggers1.bpl(55,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(63,7): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(64,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(72,9): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(84,7): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(96,16): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(97,16): Error: a matching pattern must be more than just a variable by itself: g
+Triggers1.bpl(107,40): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(121,33): Error: cannot refer to a global variable in this context: h1
+Triggers1.bpl(122,33): Error: cannot refer to a global variable in this context: h0
+20 name resolution errors detected in Triggers1.bpl
diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl
index 7bb1dcef..4e6e607b 100644
--- a/Test/test0/Types0.bpl
+++ b/Test/test0/Types0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type T, U;
type V;
diff --git a/Test/test0/Types0.bpl.expect b/Test/test0/Types0.bpl.expect
new file mode 100644
index 00000000..046c6ceb
--- /dev/null
+++ b/Test/test0/Types0.bpl.expect
@@ -0,0 +1,3 @@
+Types0.bpl(8,18): error: expected identifier before ':'
+Types0.bpl(8,12): error: expecting an identifier as parameter name
+2 parse errors detected in Types0.bpl
diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl
index 4c6e31ae..1e4d7033 100644
--- a/Test/test0/Types1.bpl
+++ b/Test/test0/Types1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type T, U;
type V;
diff --git a/Test/test0/Types1.bpl.expect b/Test/test0/Types1.bpl.expect
new file mode 100644
index 00000000..6c9f6784
--- /dev/null
+++ b/Test/test0/Types1.bpl.expect
@@ -0,0 +1,4 @@
+Types1.bpl(8,11): Error: undeclared type: x
+Types1.bpl(9,11): Error: undeclared type: x
+Types1.bpl(9,14): Error: undeclared type: x
+3 name resolution errors detected in Types1.bpl
diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl
index 33e500d6..6c203258 100644
--- a/Test/test0/WhereParsing.bpl
+++ b/Test/test0/WhereParsing.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing.bpl.expect b/Test/test0/WhereParsing.bpl.expect
new file mode 100644
index 00000000..d6621f60
--- /dev/null
+++ b/Test/test0/WhereParsing.bpl.expect
@@ -0,0 +1,4 @@
+WhereParsing.bpl(16,37): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(17,33): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(34,38): error: attributes are not allowed on the 'implementation' copies of formals
+3 parse errors detected in WhereParsing.bpl
diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl
index f99dc1ab..7b3d21b2 100644
--- a/Test/test0/WhereParsing0.bpl
+++ b/Test/test0/WhereParsing0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing0.bpl.expect b/Test/test0/WhereParsing0.bpl.expect
new file mode 100644
index 00000000..c41c598d
--- /dev/null
+++ b/Test/test0/WhereParsing0.bpl.expect
@@ -0,0 +1,3 @@
+WhereParsing0.bpl(19,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(20,38): error: where clause not allowed on bound variables
+2 parse errors detected in WhereParsing0.bpl
diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl
index 402071bf..7be165d2 100644
--- a/Test/test0/WhereParsing1.bpl
+++ b/Test/test0/WhereParsing1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing1.bpl.expect b/Test/test0/WhereParsing1.bpl.expect
new file mode 100644
index 00000000..ad079f26
--- /dev/null
+++ b/Test/test0/WhereParsing1.bpl.expect
@@ -0,0 +1,2 @@
+WhereParsing1.bpl(16,27): error: ")" expected
+1 parse errors detected in WhereParsing1.bpl
diff --git a/Test/test0/WhereParsing2.bpl b/Test/test0/WhereParsing2.bpl
index d85287f3..e098036f 100644
--- a/Test/test0/WhereParsing2.bpl
+++ b/Test/test0/WhereParsing2.bpl
@@ -1,2 +1,4 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int where x < 0; // error: where clauses not allowed on constants
diff --git a/Test/test0/WhereParsing2.bpl.expect b/Test/test0/WhereParsing2.bpl.expect
new file mode 100644
index 00000000..17484299
--- /dev/null
+++ b/Test/test0/WhereParsing2.bpl.expect
@@ -0,0 +1,2 @@
+WhereParsing2.bpl(3,14): error: ";" expected
+1 parse errors detected in WhereParsing2.bpl
diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl
index 6b28a035..0c2cf539 100644
--- a/Test/test0/WhereResolution.bpl
+++ b/Test/test0/WhereResolution.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type double;
function R(int) returns (bool);
diff --git a/Test/test0/WhereResolution.bpl.expect b/Test/test0/WhereResolution.bpl.expect
new file mode 100644
index 00000000..27cdd915
--- /dev/null
+++ b/Test/test0/WhereResolution.bpl.expect
@@ -0,0 +1,3 @@
+WhereResolution.bpl(30,38): Error: undeclared identifier: alpha
+WhereResolution.bpl(34,30): Error: old expressions allowed only in two-state contexts
+2 name resolution errors detected in WhereResolution.bpl