Removed Output files. These are created on a local machine when the tests are run.

1 files changed, 0 insertions, 252 deletions

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

-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