Enabled most of the name resolution lit tests. They don't all pass

yet due to a bug in -useBaseNameForFileName.

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