diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test0 | |
Initial set of files.
Diffstat (limited to 'Test/test0')
30 files changed, 1644 insertions, 0 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer new file mode 100644 index 00000000..e8ea231e --- /dev/null +++ b/Test/test0/Answer @@ -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
diff --git a/Test/test0/Arrays0.bpl b/Test/test0/Arrays0.bpl new file mode 100644 index 00000000..0098c4a8 --- /dev/null +++ b/Test/test0/Arrays0.bpl @@ -0,0 +1,3 @@ +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 new file mode 100644 index 00000000..db12ecb3 --- /dev/null +++ b/Test/test0/Arrays1.bpl @@ -0,0 +1,16 @@ +var Q: [int,int][int]int;
+
+procedure P()
+{
+ var q: [int]int;
+
+ start:
+ // here's how to do it:
+ q := Q[5,8];
+ q[13] := 21;
+ Q[5,8] := q;
+
+ // not like this:
+ Q[5,8][13] := 21; // error: the updated array must be an identifier
+ return;
+}
diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl new file mode 100644 index 00000000..a6a8418b --- /dev/null +++ b/Test/test0/AttributeParsing.bpl @@ -0,0 +1,25 @@ +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, any, name;
diff --git a/Test/test0/AttributeParsingErr.bpl b/Test/test0/AttributeParsingErr.bpl new file mode 100644 index 00000000..cdf8646f --- /dev/null +++ b/Test/test0/AttributeParsingErr.bpl @@ -0,0 +1,23 @@ +type {:sourcefile "test.ssc"} {1} T;
+
+function {:source "test.scc"} {1} f(int) returns (int);
+
+const {:description "The largest integer value"} {1} unique MAXINT: int;
+
+axiom {:naming "MyFavoriteAxiom"} {1} (forall i: int :: {f(i)} f(i) == i+1);
+
+var {:description "memory"} {1} $Heap: [ref, name]any;
+
+var {(forall i: int :: true)} Bla: [ref, name]any;
+
+procedure {1} {:use_impl 1} foo(x : int) returns(n : int);
+
+implementation {1} {:id 1} foo(x : int) returns(n : int)
+{
+ block1: return;
+}
+
+implementation {:id 2} {1} foo(x : int) returns(n : int)
+{
+ block1: return;
+}
diff --git a/Test/test0/AttributeResolution.bpl b/Test/test0/AttributeResolution.bpl new file mode 100644 index 00000000..c667b530 --- /dev/null +++ b/Test/test0/AttributeResolution.bpl @@ -0,0 +1,38 @@ +type {:sourcefile foo} T;
+
+function {:source bar} f(int) returns (int);
+
+const {:description baz} unique MAXINT: int;
+
+axiom {:naming qux} (forall i: int :: {f(ij)} f(i) == i+1);
+
+var {:description mux} $Heap: [ref, int]bool;
+
+var {:sort_of_like_a_trigger fux} Bla: [ref, int]bool;
+
+procedure {:use_impl bzzt} foo(x : int) returns(n : int);
+
+implementation {:id blt} foo(x : int) returns(n : int)
+{
+ block1: return;
+}
+
+// ------ and here are various correct things
+
+
+
+const {:Correct hux0 + F(hux1)} hux0: int;
+
+function {:Correct F(hux0) + hux1} F(int) returns (int);
+
+axiom {:Correct F(hux0 + hux1)} true;
+
+var {:Correct hux0*hux1} hux1: int;
+
+procedure {:Correct hux0 - hux1} P();
+
+implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} P()
+{
+}
+
+type ref;
diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl new file mode 100644 index 00000000..89cf7a36 --- /dev/null +++ b/Test/test0/BadLabels0.bpl @@ -0,0 +1,13 @@ +procedure Dup(y: int)
+{
+ X:
+ X: // error: duplicate label
+ while (y < 100)
+ {
+ Y:
+ }
+ while (y < 1000)
+ {
+ Y: // error: duplicate label (labels must be unique in entire procedure body)
+ }
+}
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl new file mode 100644 index 00000000..b4bb6948 --- /dev/null +++ b/Test/test0/BadLabels1.bpl @@ -0,0 +1,81 @@ +procedure P0()
+{
+ // these labels don't exist at all
+ goto X; // error: undefined label
+ goto Y; // error: undefined label
+}
+
+procedure P1(y: int)
+{
+ goto X; // error: label out of reach
+ while (y < 100)
+ {
+ X:
+ }
+
+ Q:
+ if (y == 102) {
+ A:
+ goto Q;
+ } else if (y == 104) {
+ B:
+ } else {
+ C:
+ goto K; // error: label out of reach
+ }
+
+ while (y < 1000)
+ {
+ K:
+ goto A; // error: label out of reach
+ if (y % 2 == 0) {
+ goto L;
+ M:
+ }
+ goto K, L;
+ L:
+ if (*) {
+ goto M; // error: label out of reach
+ }
+ }
+ goto B; // error: label out of reach
+}
+
+
+procedure Break(n: int)
+{
+ break; // error: break not inside a loop
+ if (*) {
+ break; // error: label-less break not inside a loop
+ }
+
+ A:
+ if (*) {
+ break A; // this is fine, since the break statement uses a label
+ }
+
+ B:
+ assert 2 <= n;
+ while (*) {
+ break B; // error: B does not label a loop
+ break;
+ C: while (*) { assert n < 100; }
+ break A; // error: A does not label a loop
+ break C; // error: A does not label an enclosing loop
+ F: break F; // error: F does not label an enclosing loop
+ }
+
+ D:
+ while (*) {
+ E:
+ while (*) {
+ if (*) {
+ break;
+ } else if (*) {
+ if (*) { break E; }
+ } else {
+ break D;
+ }
+ }
+ }
+}
diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl new file mode 100644 index 00000000..b06ab0d9 --- /dev/null +++ b/Test/test0/BadQuantifier.bpl @@ -0,0 +1,3 @@ +
+function f(int) returns (bool);
+axiom (forall int x :: f(x) <== x >= 0);
diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl new file mode 100644 index 00000000..eb1c43b7 --- /dev/null +++ b/Test/test0/EmptyCallArgs.bpl @@ -0,0 +1,33 @@ +type C;
+
+procedure P(x:int, y:bool) returns (z:C);
+procedure Q<a>(x:int, y:a) returns (z:a);
+
+procedure CallP() {
+ var x:int;
+ var y:bool;
+ var z:C;
+
+ call z := P(x, y);
+ call * := P(x, y);
+ call z := P(*, y);
+ call z := P(x, *);
+ call * := P(*, y);
+ call * := P(x, *);
+ call z := P(*, *);
+ call * := P(*, *);
+}
+
+procedure CallQ() {
+ var x:int;
+ var y:bool;
+ var z:bool;
+
+ call z := Q(x, y);
+ call * := Q(x, y);
+ call z := Q(*, y);
+ call z := Q(x, *);
+ call * := Q(*, y);
+ call * := Q(x, *); // problem: type parameter cannot be inferred
+ call * := Q(*, *); // problem: type parameter cannot be inferred
+}
\ No newline at end of file diff --git a/Test/test0/LargeLiterals0.bpl b/Test/test0/LargeLiterals0.bpl new file mode 100644 index 00000000..be459bf5 --- /dev/null +++ b/Test/test0/LargeLiterals0.bpl @@ -0,0 +1,7 @@ +// Test to parse large integer literals
+
+axiom 1234567890987654321 == 1234567890987654321;
+
+function f(int) returns (int);
+
+axiom f(1234567890987654321) == 0;
diff --git a/Test/test0/LineParse.bpl b/Test/test0/LineParse.bpl new file mode 100644 index 00000000..a64eed0b --- /dev/null +++ b/Test/test0/LineParse.bpl @@ -0,0 +1,12 @@ +#line
+#line
+#line 0
+#line 0
+
+#dontknow what this is No, I don't well, it's an error is what it is
+
+#define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
+
+// this is line 5; an error occurs on line 6:
+ #line 10 // this is not even scanned like a pragma, because the # is not in column 0
+
diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl new file mode 100644 index 00000000..b0c578c7 --- /dev/null +++ b/Test/test0/LineResolve.bpl @@ -0,0 +1,38 @@ +procedure P() {
+var x: int;
+x :=
+
+ a+ // error: LineResolve.bpl(5,1)
+
+ b+ // error: LineResolve.bpl(7,2)
+#line 12
+c+ // error: LineResolve.bpl(12,0)
+ d+ // error: LineResolve.bpl(13,10)
+#line 12
+e+ // error: LineResolve.bpl(12,0)
+#line 2
+f+ // error: LineResolve.bpl(2,0)
+#line 1000
+#line 900
+g+ // error: LineResolve.bpl(900,0)
+
+#line 10 Abc.txt
+
+ h+ // error: Abc.txt(11,3)
+
+i+ // error: Abc.txt(13,0)
+#line 98
+
+j+ // error: Abc.txt(99,0)
+
+#line 103 c:\Users\leino\Documents\Programs\MyClass.ssc
+
+k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0)
+
+#line -58
+
+#line 12 A B C . txt
+l+ // error: A B C . txt(12,0)
+
+0;
+}
diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl new file mode 100644 index 00000000..d529cb9c --- /dev/null +++ b/Test/test0/MapsResolutionErrors.bpl @@ -0,0 +1,28 @@ +
+var m: []int;
+var p: <a>[]a;
+
+type C _;
+var bad: <a,b>[]C a; // error: b is not used
+
+function F<a>(a, int) returns (bool) { true }
+
+type Set _;
+function EmptySet<a>() returns (Set a);
+function G<a>(a, int) returns (Set a) { EmptySet() }
+
+function H<a>(int) returns (Set a);
+
+function {:inline true} K<a>(int) returns (Set a)
+{ EmptySet() }
+
+
+procedure P<a>(x: int, y: bool) returns (z: int, w: bool); // error: "a" is not used
+
+procedure Q<a>(x: int, y: bool) returns (z: int, w: a);
+procedure R<a>(x: int, y: bool) returns (z: int, w: Set a);
+procedure S<a>(x: a, y: bool) returns (z: int, w: Set a);
+
+
+function K2<a>(int) returns (Set a) // now ok
+{ EmptySet() }
diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl new file mode 100644 index 00000000..09edbd12 --- /dev/null +++ b/Test/test0/ModifiedBag.bpl @@ -0,0 +1,371 @@ +// ----------- BEGIN PRELUDE
+type real;
+
+type elements;
+
+type name;
+
+const $CALL: name;
+
+const $REQ: name;
+
+const $ENS: name;
+
+const $PACK: name;
+
+const $UNPACK: name;
+
+const $HEAD: name;
+
+const $THROW: name;
+
+var $RefHeap: [ref, name]ref;
+
+var $IntHeap: [ref, name]int;
+
+var $RealHeap: [ref, name]real;
+
+var $BoolHeap: [ref, name]bool;
+
+var $ArrayHeap: [ref, name]elements;
+
+const $allocated: name;
+
+const $elements: name;
+
+function $ArrayLength(ref) returns (int);
+
+function $RefArrayGet(elements, int) returns (ref);
+
+function $RefArraySet(elements, int, ref) returns (elements);
+
+function $IntArrayGet(elements, int) returns (value: int);
+
+function $IntArraySet(elements, int, value: int) returns (elements);
+
+function $RealArrayGet(elements, int) returns (value: real);
+
+function $RealArraySet(elements, int, value: real) returns (elements);
+
+function $BoolArrayGet(elements, int) returns (value: bool);
+
+function $BoolArraySet(elements, int, value: bool) returns (elements);
+
+function $ArrayArrayGet(elements, int) returns (value: elements);
+
+function $ArrayArraySet(elements, int, value: elements) returns (elements);
+
+axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x);
+
+axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> $RefArrayGet($RefArraySet(A, i, x), j) == $RefArrayGet(A, j));
+
+axiom (forall A: elements, i: int, x: int :: $IntArrayGet($IntArraySet(A, i, x), i) == x);
+
+axiom (forall A: elements, i: int, j: int, x: int :: i != j ==> $IntArrayGet($IntArraySet(A, i, x), j) == $IntArrayGet(A, j));
+
+axiom (forall A: elements, i: int, x: real :: $RealArrayGet($RealArraySet(A, i, x), i) == x);
+
+axiom (forall A: elements, i: int, j: int, x: real :: i != j ==> $RealArrayGet($RealArraySet(A, i, x), j) == $RealArrayGet(A, j));
+
+axiom (forall A: elements, i: int, x: bool :: $BoolArrayGet($BoolArraySet(A, i, x), i) == x);
+
+axiom (forall A: elements, i: int, j: int, x: bool :: i != j ==> $BoolArrayGet($BoolArraySet(A, i, x), j) == $BoolArrayGet(A, j));
+
+axiom (forall A: elements, i: int, x: elements :: $ArrayArrayGet($ArrayArraySet(A, i, x), i) == x);
+
+axiom (forall A: elements, i: int, j: int, x: elements :: i != j ==> $ArrayArrayGet($ArrayArraySet(A, i, x), j) == $ArrayArrayGet(A, j));
+
+axiom (forall a: ref :: 0 <= $ArrayLength(a));
+
+function $typeof(ref) returns (name);
+
+function $BoolIs(bool, name) returns (bool);
+
+function $RealIs(real, name) returns (bool);
+
+function $IntIs(int, name) returns (bool);
+
+const System.Int16: name;
+
+const System.Int32: name;
+
+const System.Int64: name;
+
+const System.Int16.MinValue: int;
+
+const System.Int16.MaxValue: int;
+
+const System.Int32.MinValue: int;
+
+const System.Int32.MaxValue: int;
+
+const System.Int64.MinValue: int;
+
+const System.Int64.MaxValue: int;
+
+axiom System.Int64.MinValue < System.Int32.MinValue;
+
+axiom System.Int32.MinValue < System.Int16.MinValue;
+
+axiom System.Int16.MinValue < System.Int16.MaxValue;
+
+axiom System.Int16.MaxValue < System.Int32.MaxValue;
+
+axiom System.Int32.MaxValue < System.Int64.MaxValue;
+
+axiom (forall i: int :: $IntIs(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue);
+
+axiom (forall i: int :: $IntIs(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue);
+
+axiom (forall i: int :: $IntIs(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue);
+
+function $RefIs(ref, name) returns (bool);
+
+axiom (forall o: ref, T: name :: $RefIs(o, T) <==> o == null || $typeof(o) <: T);
+
+axiom (forall o: ref, T: name :: $RefIs(o, $NotNull(T)) <==> o != null && $RefIs(o, T));
+
+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $IntArray(T)) && a != null ==> $IntIs($IntArrayGet($ArrayHeap[a, $elements], i), T));
+
+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RealArray(T)) && a != null ==> $RealIs($RealArrayGet($ArrayHeap[a, $elements], i), T));
+
+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $BoolArray(T)) && a != null ==> $BoolIs($BoolArrayGet($ArrayHeap[a, $elements], i), T));
+
+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RefArray(T)) && a != null ==> $RefIs($RefArrayGet($ArrayHeap[a, $elements], i), T));
+
+function $NotNull(name) returns (name);
+
+function $IntArray(name) returns (name);
+
+function $BoolArray(name) returns (name);
+
+function $RealArray(name) returns (name);
+
+function $RefArray(name) returns (name);
+// ----------- END PRELUDE
+const Bag.a: name;
+
+const Bag.n: name;
+
+const Bag: name;
+
+
+
+
+
+procedure Bag..ctor$(this: ref, initialElements$in: ref);
+
+
+
+
+
+
+procedure System.Object..ctor(this: ref);
+
+
+
+procedure System.Array.CopyTo$System.Array$System.Int32(this: ref, array$in: ref, index$in: int);
+
+
+
+procedure Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int);
+ requires 0 <= howMany$in;
+ requires start$in + howMany$in <= $ArrayLength(initialElements$in);
+ modifies $IntHeap, $RefHeap;
+
+
+
+implementation Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int)
+{
+ var initialElements: ref, start: int, howMany: int, stack0i: int, stack0o: ref, stack1i: int, stack2i: int;
+
+ entry:
+ assume $RefIs(this, $NotNull(Bag));
+ initialElements := initialElements$in;
+ assume $RefIs(initialElements, $NotNull($IntArray(System.Int32)));
+ start := start$in;
+ assume $IntIs(start, System.Int32);
+ howMany := howMany$in;
+ assume $IntIs(howMany, System.Int32);
+ goto block165;
+
+ block165:
+ call System.Object..ctor(this);
+ $IntHeap[this, Bag.n] := howMany;
+ stack0i := howMany;
+ havoc stack0o;
+ assume $BoolHeap[stack0o, $allocated] == true && $ArrayLength(stack0o) == stack0i;
+ $RefHeap[this, Bag.a] := stack0o;
+ stack0o := $RefHeap[this, Bag.a];
+ stack1i := 0;
+ stack2i := start + howMany;
+ call System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(initialElements, start, stack0o, stack1i, stack2i);
+ assert this != null;
+ assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
+ return;
+}
+
+
+
+procedure System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(sourceArray$in: ref, sourceIndex$in: int, destinationArray$in: ref, destinationIndex$in: int, length$in: int);
+
+
+
+procedure Bag.Add$System.Int32(this: ref, x$in: int);
+ modifies $ArrayHeap, $IntHeap;
+
+
+
+implementation Bag.Add$System.Int32(this: ref, x$in: int)
+{
+ var x: int, stack0i: int, stack1o: ref, stack1i: int, stack0b: bool, stack0o: ref, stack2i: int, b: ref;
+
+ entry:
+ assume $RefIs(this, $NotNull(Bag));
+ x := x$in;
+ assume $IntIs(x, System.Int32);
+ assert this != null;
+ assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
+ goto block205;
+
+ block205:
+ stack0i := $IntHeap[this, Bag.n];
+ stack1o := $RefHeap[this, Bag.a];
+ stack1i := $ArrayLength(stack1o);
+ stack1i := stack1i;
+ stack0b := stack0i != stack1i;
+ goto trueblock208, falseblock206;
+
+ trueblock208:
+ assume stack0b == true;
+assume false;
+// goto block208;
+return;
+
+ falseblock206:
+ assume stack0b == false;
+ goto block206;
+
+ block206:
+// assert label-([$PACK@0:3:4425:0], $IntHeap[this, Bag.n] <= 2 * $ArrayLength($RefHeap[this, Bag.a]));
+ stack0i := 2;
+ stack1o := $RefHeap[this, Bag.a];
+ stack1i := $ArrayLength(stack1o);
+ stack1i := stack1i;
+ stack0i := stack0i * stack1i;
+ stack0i := stack0i;
+ assert $IntHeap[this, Bag.n] <= stack0i;
+// havoc b;
+// assume $BoolHeap[b, $allocated] == true && $ArrayLength(b) == stack0i;
+// assert label-([$PACK@0:3:4427:0], $IntHeap[this, Bag.n] <= $ArrayLength(b));
+// stack0o := $RefHeap[this, Bag.a];
+// stack1i := 0;
+// call [$CALL@0:7:39:0] System.Array.CopyTo$System.Array$System.Int32(stack0o, b, stack1i);
+// $RefHeap[this, Bag.a] := b;
+// assert label-([$PACK@0:3:4428:0], $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]));
+// goto block208;
+ return;
+
+ block208:
+ stack0o := $RefHeap[this, Bag.a];
+ stack1i := $IntHeap[this, Bag.n];
+ $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], stack1i, x);
+ stack0o := this;
+ stack1o := stack0o;
+ stack1i := $IntHeap[stack1o, Bag.n];
+ stack2i := 1;
+ stack1i := stack1i + stack2i;
+ $IntHeap[stack0o, Bag.n] := stack1i;
+ assert this != null;
+ assert 0 <= $IntHeap[this, Bag.n];
+ assert $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
+ return;
+
+}
+
+
+
+procedure Bag.ExtractMin(this: ref) returns ($result: int);
+ modifies $IntHeap, $ArrayHeap;
+
+
+
+implementation Bag.ExtractMin(this: ref) returns ($result: int)
+{
+ var m: int, mindex: int, i: int, stack0i: int, stack0b: bool, stack0o: ref, stack1o: ref, stack1i: int, stack2i: int, CS$00000003$00000000: int;
+
+ entry:
+ assume $RefIs(this, $NotNull(Bag));
+ assert this != null;
+ assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
+ goto block282;
+
+ block282:
+ m := 2147483647;
+ mindex := 0;
+ i := 1;
+ goto block286;
+
+ block285:
+ stack0i := 1;
+ stack0i := i + stack0i;
+ i := stack0i;
+ goto block286;
+
+ block286:
+ stack0i := $IntHeap[this, Bag.n];
+ stack0b := i <= stack0i;
+ goto trueblock283, falseblock287;
+
+ trueblock283:
+ assume stack0b == true;
+ goto block283;
+
+ falseblock287:
+ assume stack0b == false;
+ goto block287;
+
+ block283:
+ stack0o := $RefHeap[this, Bag.a];
+ stack0i := $IntArrayGet($ArrayHeap[stack0o, $elements], i);
+ stack0b := stack0i >= m;
+ goto trueblock285, falseblock284;
+
+ block287:
+ stack0o := this;
+ stack1o := stack0o;
+ stack1i := $IntHeap[stack1o, Bag.n];
+ stack2i := 1;
+ stack1i := stack1i - stack2i;
+ $IntHeap[stack0o, Bag.n] := stack1i;
+ stack0o := $RefHeap[this, Bag.a];
+ stack1o := $RefHeap[this, Bag.a];
+ stack2i := $IntHeap[this, Bag.n];
+ stack1i := $IntArrayGet($ArrayHeap[stack1o, $elements], stack2i);
+ $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], mindex, stack1i);
+ CS$00000003$00000000 := m;
+ goto block289;
+
+ trueblock285:
+ assume stack0b == true;
+ goto block285;
+
+ falseblock284:
+ assume stack0b == false;
+ goto block284;
+
+ block284:
+ mindex := i;
+ stack0o := $RefHeap[this, Bag.a];
+ m := $IntArrayGet($ArrayHeap[stack0o, $elements], i);
+ goto block285;
+
+ block289:
+ $result := CS$00000003$00000000;
+ assert this != null;
+ assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
+ return;
+}
+
+type ref;
+const null : ref;
diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl new file mode 100644 index 00000000..0ba6c69c --- /dev/null +++ b/Test/test0/Orderings.bpl @@ -0,0 +1,20 @@ +
+type C;
+
+const c:int extends a;
+const d:int extends a complete;
+const e:int extends unique a, b;
+const f:int extends complete;
+
+const a:int;
+const b:int;
+
+const g:int extends x; // error: undeclared parent
+
+const c0:C;
+const c1:C extends c0, c0; // error: parent mentioned twice
+const c2:C extends c2; // error: constant as its own parent
+
+const h:int extends y; // error: variable cannot be parent
+
+var y:int;
\ No newline at end of file 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
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl new file mode 100644 index 00000000..a1f941d8 --- /dev/null +++ b/Test/test0/PrettyPrint.bpl @@ -0,0 +1,40 @@ +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);
+
+// -------------- quantifier key-value decorations
+
+function f(int) returns (int);
+
+axiom (forall x: int :: {:xname "hello"}
+ { :weight 5} {f(x+x)} {:ValueFunc f(x+1) } {f(x)*f(x)} {:nopats f(x+x+x)}
+ f(f(x)) < 200);
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl new file mode 100644 index 00000000..ac87476f --- /dev/null +++ b/Test/test0/Prog0.bpl @@ -0,0 +1,51 @@ +// BoogiePL Examples
+type real;
+type elements;
+
+var x:int; var y:real; var z:ref; // Variables
+var x.3:bool; var $ar:ref; // Names can have glyphs
+
+const a, b, c:int; // Consts
+
+function f (int, int) returns (int); // Function with arity 2
+function g ( int , int) returns (int); // Function with arity 2
+function h(int,int) returns (int); // Function with arity 2
+
+function m (int) returns (int); // Function with arity 1
+function k(int) returns (int); // Function with arity 1
+
+
+axiom
+ (forall x : int :: f(g(h(a,b),c),x) > 100) ;
+
+procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
+
+
+procedure q(x:int, y:ref) returns (z:int) // Procedure with output params
+ requires x > 0; // as many req/ens/mod you want
+ ensures z > 3;
+ ensures old(x) == 1; // old only in ensures..
+ modifies z,y,$ar;
+{
+ var t, s: int;
+ var r: [int,ref]ref;
+
+ start: // one label per block
+ t := x;
+ s := t;
+ z := x + t;
+ call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns
+ goto continue, end ; // as many labels as you like
+
+ continue:
+ return; // ends control flow
+
+ end:
+ goto start;
+}
+
+procedure s(e: elements) { L: return; }
+procedure r (x:int, y:ref) returns (z:int);
+
+type ref;
+const null : ref;
diff --git a/Test/test0/Quoting.bpl b/Test/test0/Quoting.bpl new file mode 100644 index 00000000..eaf8fe7a --- /dev/null +++ b/Test/test0/Quoting.bpl @@ -0,0 +1,16 @@ +function \true() returns(bool);
+
+type \procedure;
+procedure \old(\any : \procedure) returns(\var : \procedure)
+{
+ var \modifies : \procedure;
+ \modifies := \any;
+ \var := \modifies;
+}
+
+procedure qux(a : \procedure)
+{
+ var \var : \procedure; var x : bool;
+ call \var := \old(a);
+ x := \true();
+}
diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl new file mode 100644 index 00000000..6750d77d --- /dev/null +++ b/Test/test0/Triggers0.bpl @@ -0,0 +1,15 @@ +// Trigger errors
+
+function f(int, int) returns (int);
+function P(int, int) returns (bool);
+
+// -------------- tests specific to pattern exclusions
+
+axiom (forall x: int ::
+ {:nopats f(x,10) }
+ { : nopats f(x,10) }
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ {:nopats f(x,10), f(x,x) } // error: a pattern exclusion can only mention one expression
+ f(x,10) == 3);
diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl new file mode 100644 index 00000000..02c63406 --- /dev/null +++ b/Test/test0/Triggers1.bpl @@ -0,0 +1,127 @@ +// Trigger errors
+
+function f(int, int) returns (int);
+function P(int, int) returns (bool);
+
+axiom (forall x: int ::
+ { f(x,10) && f(x,9) } // error: && not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { ((((f(x,10) || f(x,9))))) } // error: || not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { !f(x,10) } // error: ! not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { (!f(x,10)) } // error: ! not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { P(x,10) ==> P(20,x) } // error: ==> not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { P(x,10) <==> P(20,x) } // error: <==> not allowed
+ f(x,10) == 3);
+
+
+axiom (forall x: int ::
+ { f(x,10) == 3 } // error: == not allowed
+ f(x,10) == 3);
+
+axiom (forall x: int ::
+ { f(x,10) < 3 } // error: < not allowed
+ f(x,10) == 3);
+
+
+axiom (forall x: int ::
+ { f(x,10) + f(x,x) != 3 } // yes, != is allowed
+ f(x,10) == 3);
+
+axiom (forall b: bool ::
+ { (forall y: int :: b) } // error: quantifiers not allowed
+ b);
+
+// -------------- tests of free variables
+
+const g: int;
+
+axiom (forall x: int ::
+ { false, 6 } // error: does not mention "x"
+ x < x + 1);
+
+axiom (forall x: int ::
+ { false, x+1, 6 } // allowed
+ x < x + 1);
+
+axiom (forall x: int, y: int ::
+ { x+1 } // error: does not mention "y"
+ { y+1 } // error: does not mention "x"
+ x < y + 1);
+
+axiom (forall x: int ::
+ { g+x != 65 } // allowed
+ x < x + 1);
+
+axiom (forall x: int ::
+ { x } // "x" by itself is not a good trigger
+ x < x + 1);
+
+//axiom (forall x: any :: // PR: removed for the time being
+// { cast(x,int) } // can't fool me, still not allowed
+// x == x );
+
+// --- multiple triggers
+
+axiom (forall x: int, y: int, z: int ::
+ { x+y+z } // good
+ { x+y, y+z } // also good
+ { f(f(x,y),y) } // error: does not mention z
+ x == x );
+
+// --- multi-triggers
+
+axiom (forall x: int, y: int, z: int ::
+ { f(x,x), f(y,y), f(z,z) } // good
+ f(x,y) < f(y,z) );
+
+// --- pattern exclusion
+
+axiom (forall x: int, y: int ::
+ {:nopats x } // error: "x" by itself is not allowed here either
+ {:nopats g } // error: "g" by itself is not allowed here either
+ x < y);
+
+axiom (forall x: int, y: int ::
+ {:nopats f(g,g) } // but it is okay not to mention the bound variables (in a pattern exclusion)
+ x < y);
+
+// --- merging of nested quantifiers
+
+axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK
+axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
+axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // error
+
+// three levels
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(y,z) } f(y,y) > 0))); // error
+axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK
+
+// --- no free variables
+
+var h0: int;
+var h1: [ref,ref]int;
+
+axiom (forall o: ref, f: ref :: h1[o,f] // error: cannot mention free variable "h1"
+ < h0); // error: cannot mention free variable "h0"
+
+const c0: int;
+const c1: [ref,ref]int;
+
+axiom (forall o: ref, f: ref :: c1[o,f] < c0);
+
+type ref;
diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl new file mode 100644 index 00000000..7bb1dcef --- /dev/null +++ b/Test/test0/Types0.bpl @@ -0,0 +1,8 @@ +type T, U;
+type V;
+
+function f([U,V]T, int) returns (U);
+function g(x: [U,V]T, y: int) returns (z: U);
+function h([U,V]T: int, y: int) returns (z: U); // parse error
+function k(T: int, y: int) returns (U: [any]int);
+function l(x) returns (int); // resolve error
diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl new file mode 100644 index 00000000..f743be85 --- /dev/null +++ b/Test/test0/Types1.bpl @@ -0,0 +1,7 @@ +type T, U;
+type V;
+
+function h(T) returns (int);
+function k(x:T) returns (int);
+function l(x) returns (int); // resolve error
+function m(x:int, x) returns (bool); // resolve error
diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl new file mode 100644 index 00000000..ec18dc3b --- /dev/null +++ b/Test/test0/WhereParsing.bpl @@ -0,0 +1,25 @@ +const x: int;
+
+function R(int) returns (bool);
+function Even(int) returns (bool);
+
+var y: int where R(y);
+var g: int where g == 12;
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+ requires x < 100;
+ modifies g;
+ ensures -100 < y;
+
+implementation P(xx: int where xx > 0) // error: where not allowed in implementation decl
+ returns (yy: int where yy < 0) // error: where not allowed in implementation decl
+{
+ var a: int where a == b; // b is not allowed to be mentioned here, but this test is only
+ var b: int; // for parsing, so no complaint will be issued
+
+ start:
+ a := xx;
+ call b := P(a);
+ yy := b;
+ return;
+}
diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl new file mode 100644 index 00000000..84f92741 --- /dev/null +++ b/Test/test0/WhereParsing0.bpl @@ -0,0 +1,28 @@ +const x: int;
+
+function R(int) returns (bool);
+function Even(int) returns (bool);
+
+var y: int where R(y);
+var g: int where g == 12;
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+ requires x < 100;
+ modifies g;
+ ensures -100 < y;
+
+procedure Q(x: int where x > 0) returns (y: int where y < 0)
+ requires x < 100;
+ modifies g;
+ ensures (forall t: int where Even(t) :: -100 < y + t) || // error: where not allowed in quant
+ (exists t: int where Even(t) :: -100 < y + t); // error: where not allowed in quant
+{
+ var a: int;
+ var b: int;
+
+ start:
+ a := x;
+ call b := P(a);
+ y := b;
+ return;
+}
diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl new file mode 100644 index 00000000..402071bf --- /dev/null +++ b/Test/test0/WhereParsing1.bpl @@ -0,0 +1,15 @@ +const x: int;
+
+function R(int) returns (bool);
+function Even(int) returns (bool);
+
+var y: int where R(y);
+var g: int where g == 12;
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+ requires x < 100;
+ modifies g;
+ ensures -100 < y;
+
+function f(a: int, b: int where b < 0) // error: where not allowed among function parameters
+ returns (bool);
diff --git a/Test/test0/WhereParsing2.bpl b/Test/test0/WhereParsing2.bpl new file mode 100644 index 00000000..d85287f3 --- /dev/null +++ b/Test/test0/WhereParsing2.bpl @@ -0,0 +1,2 @@ +const x: int where x < 0; // error: where clauses not allowed on constants
+
diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl new file mode 100644 index 00000000..6b28a035 --- /dev/null +++ b/Test/test0/WhereResolution.bpl @@ -0,0 +1,62 @@ +type double;
+
+function R(int) returns (bool);
+function K(double, bool) returns (bool);
+
+var y: int where R(y);
+var g: int where h ==> g == 12;
+var h: bool where g < 100;
+var k: double where K(k, h);
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+ requires x < 100;
+ modifies g;
+ ensures -100 < y;
+
+implementation P(xx: int) returns (yy: int)
+{
+ var a: int where a == 10;
+ var b: int where a == b && b < g;
+
+ start:
+ a := xx;
+ call b := P(a);
+ yy := b;
+ return;
+}
+
+procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
+ returns (v: bool where v,
+ y: int where x + y + z < 0,
+ z: int where g == 12,
+ alpha: ref where old(alpha) != null, // error: cannot use old in where clause
+ beta: ref where (forall r: ref :: r == beta ==> beta == null))
+ requires x < 100;
+ modifies g;
+ ensures -100 < y;
+{
+ var a: int;
+ var b: int;
+
+ start:
+ a := x;
+ call b := P(a);
+ y := b;
+ return;
+}
+
+const SomeConstant: ref;
+
+procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
+{
+ var m: ref where m != SomeConstant;
+ var k: int where k != SomeConstant;
+ var r: ref where (forall abc: ref :: abc == SomeConstant);
+ var b: bool;
+ start:
+ b := (forall l: ref :: l == SomeConstant);
+ return;
+}
+
+type ref;
+const null : ref;
diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat new file mode 100644 index 00000000..c7c6ee3d --- /dev/null +++ b/Test/test0/runtest.bat @@ -0,0 +1,33 @@ +@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
|