2 files changed, 0 insertions, 347 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer
deleted file mode 100644
index 06f85659..00000000
--- a/Test/test0/Answer
+++ /dev/null
@@ -1,305 +0,0 @@
-
-Boogie program verifier finished with 0 verified, 0 errors
-
-Boogie program verifier finished with 0 verified, 0 errors
-Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
-1 parse errors detected in Triggers0.bpl
-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;
-
-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
-
-Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(14,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
-Arrays1.bpl(18,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(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(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(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(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(16,27): error: ")" expected
-1 parse errors detected in WhereParsing1.bpl
-WhereParsing2.bpl(3,14): error: ";" expected
-1 parse errors detected in WhereParsing2.bpl
-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(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(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(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(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
-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
-
-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
-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;
-
-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(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(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(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(19,6): Error: undeclared identifier: y
-1 name resolution errors detected in SeparateVerification0.bpl
------ SeparateVerification1.bpl SeparateVerification0.bpl
-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
-
-Boogie program verifier finished with 0 verified, 0 errors
------ SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
-
-Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat
deleted file mode 100644
index 5ecc22dc..00000000
--- a/Test/test0/runtest.bat
+++ /dev/null
@@ -1,42 +0,0 @@
-@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-rem set BGEXE=mono ..\..\Binaries\Boogie.exe
-
-%BGEXE% %* /noVerify Prog0.bpl
-%BGEXE% %* /noVerify ModifiedBag.bpl
-%BGEXE% %* /noVerify Triggers0.bpl
-%BGEXE% %* /noVerify Triggers1.bpl
-%BGEXE% %* /noVerify /printInstrumented PrettyPrint.bpl
-%BGEXE% %* /noVerify Arrays0.bpl
-%BGEXE% %* /noVerify Arrays1.bpl
-%BGEXE% %* /noVerify Types0.bpl
-%BGEXE% %* /noVerify Types1.bpl
-%BGEXE% %* /noVerify WhereParsing.bpl
-%BGEXE% %* /noVerify WhereParsing0.bpl
-%BGEXE% %* /noVerify WhereParsing1.bpl
-%BGEXE% %* /noVerify WhereParsing2.bpl
-%BGEXE% %* /noVerify WhereResolution.bpl
-%BGEXE% %* /noVerify BadLabels0.bpl
-%BGEXE% %* /noVerify BadLabels1.bpl
-%BGEXE% %* /noVerify LineParse.bpl
-%BGEXE% %* /noVerify LineResolve.bpl
-%BGEXE% %* /noVerify AttributeParsingErr.bpl
-%BGEXE% %* /noVerify /print:- /env:0 AttributeParsing.bpl
-%BGEXE% %* /noVerify AttributeResolution.bpl
-%BGEXE% %* /noVerify /print:- /env:0 Quoting.bpl
-%BGEXE% %* /noVerify LargeLiterals0.bpl
-%BGEXE% %* /noVerify MapsResolutionErrors.bpl
-%BGEXE% %* /noVerify Orderings.bpl
-%BGEXE% %* /noVerify BadQuantifier.bpl
-%BGEXE% %* /noVerify EmptyCallArgs.bpl
-
-echo ----- SeparateVerification0.bpl
-%BGEXE% %* /noVerify SeparateVerification0.bpl
-echo ----- SeparateVerification1.bpl SeparateVerification0.bpl
-%BGEXE% %* /noVerify SeparateVerification1.bpl SeparateVerification0.bpl
-echo ----- SeparateVerification0.bpl SeparateVerification0.bpl
-%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl
-echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
-%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl