Initial set of files.

1 files changed, 252 insertions, 0 deletions

diff --git a/Test/test0/Output b/Test/test0/Output
new file mode 100644
index 00000000..e8ea231e
--- /dev/null
+++ b/Test/test0/Output
@@ -0,0 +1,252 @@
+

+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

+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(106,40): Error: trigger must mention all quantified variables, but does not mention: x

+Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z

+Triggers1.bpl(110,57): 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: x

+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

+23 name resolution errors detected in Triggers1.bpl

+const x: int;

+

+const y: int;

+

+const z: int;

+

+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 / y / z == x / (y / z);

+

+axiom x / y / (z / x) == x / y / z;

+

+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) returns (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

+

+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 method's modifies clause: Q

+Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

+2 type checking errors detected in Arrays1.bpl

+Types0.bpl(6,18): Error: expected identifier before ':'

+1 parse errors detected in Types0.bpl

+Types1.bpl(6,11): Error: undeclared type: x

+Types1.bpl(7,18): Error: undeclared type: x

+2 name resolution errors detected in Types1.bpl

+WhereParsing.bpl(14,37): Error: where clause not allowed here

+WhereParsing.bpl(15,33): Error: where clause not allowed here

+2 parse errors detected in WhereParsing.bpl

+WhereParsing0.bpl(17,38): Error: where clause not allowed here

+WhereParsing0.bpl(18,38): Error: where clause not allowed here

+2 parse errors detected in WhereParsing0.bpl

+WhereParsing1.bpl(14,27): syntax error: ) expected

+1 parse errors detected in WhereParsing1.bpl

+WhereParsing2.bpl(1,14): syntax 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

+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

+2 name resolution errors detected in BadLabels0.bpl

+BadLabels1.bpl(4,3): Error: Error: goto label 'X' is undefined or out of reach

+BadLabels1.bpl(5,3): Error: Error: goto label 'Y' is undefined or out of reach

+BadLabels1.bpl(10,3): Error: Error: goto label 'X' is undefined or out of reach

+BadLabels1.bpl(24,5): Error: Error: goto label 'K' is undefined or out of reach

+BadLabels1.bpl(30,5): Error: Error: goto label 'A' is undefined or out of reach

+BadLabels1.bpl(38,7): Error: Error: goto label 'M' is undefined or out of reach

+BadLabels1.bpl(41,3): Error: Error: goto label 'B' is undefined or out of reach

+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

+13 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(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): syntax 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(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

+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

+9 parse errors detected in AttributeParsingErr.bpl

+

+type {:sourcefile "test.ssc"} T;

+

+function {:source "test.scc"} f(int) returns (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;

+

+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

+9 name resolution errors detected in AttributeResolution.bpl

+

+function \true() returns (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

+

+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

+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

+4 name resolution errors detected in Orderings.bpl

+BadQuantifier.bpl(3,15): syntax error: invalid QuantifierBody

+1 parse errors detected in BadQuantifier.bpl

+EmptyCallArgs.bpl(31,2): Error: type variable must occur in types of given arguments: a

+EmptyCallArgs.bpl(32,2): Error: type variable must occur in types of given arguments: a

+2 name resolution errors detected in EmptyCallArgs.bpl