diff options
Diffstat (limited to 'Test/test0')
55 files changed, 430 insertions, 79 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index f4e2b981..51798f57 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -2,28 +2,28 @@ Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Triggers0.bpl(14,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
+Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
1 parse errors detected in Triggers0.bpl
-Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(15,9): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(19,10): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(23,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(27,17): Error: boolean operators are not allowed in triggers
-Triggers1.bpl(32,17): Error: equality is not allowed in triggers
-Triggers1.bpl(36,17): Error: arithmetic comparisons are not allowed in triggers
-Triggers1.bpl(45,10): Error: quantifiers are not allowed in triggers
-Triggers1.bpl(53,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(61,7): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(62,7): Error: trigger must mention all quantified variables, but does not mention: x
-Triggers1.bpl(70,9): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x
-Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g
-Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y
-Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z
-Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1
-Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0
+Triggers1.bpl(9,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(13,21): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(17,9): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(21,10): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(25,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(29,17): Error: boolean operators are not allowed in triggers
+Triggers1.bpl(34,17): Error: equality is not allowed in triggers
+Triggers1.bpl(38,17): Error: arithmetic comparisons are not allowed in triggers
+Triggers1.bpl(47,10): Error: quantifiers are not allowed in triggers
+Triggers1.bpl(55,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(63,7): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(64,7): Error: trigger must mention all quantified variables, but does not mention: x
+Triggers1.bpl(72,9): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(84,7): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(96,16): Error: a matching pattern must be more than just a variable by itself: x
+Triggers1.bpl(97,16): Error: a matching pattern must be more than just a variable by itself: g
+Triggers1.bpl(107,40): Error: trigger must mention all quantified variables, but does not mention: y
+Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: z
+Triggers1.bpl(121,33): Error: cannot refer to a global variable in this context: h1
+Triggers1.bpl(122,33): Error: cannot refer to a global variable in this context: h0
20 name resolution errors detected in Triggers1.bpl
const x: int;
@@ -120,50 +120,50 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
+Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
-Types0.bpl(6,18): error: expected identifier before ':'
-Types0.bpl(6,12): error: expecting an identifier as parameter name
+Types0.bpl(8,18): error: expected identifier before ':'
+Types0.bpl(8,12): error: expecting an identifier as parameter name
2 parse errors detected in Types0.bpl
-Types1.bpl(6,11): Error: undeclared type: x
-Types1.bpl(7,11): Error: undeclared type: x
-Types1.bpl(7,14): Error: undeclared type: x
+Types1.bpl(8,11): Error: undeclared type: x
+Types1.bpl(9,11): Error: undeclared type: x
+Types1.bpl(9,14): Error: undeclared type: x
3 name resolution errors detected in Types1.bpl
-WhereParsing.bpl(14,37): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(15,33): error: where clause not allowed on the 'implementation' copies of formals
-WhereParsing.bpl(32,38): error: attributes are not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(16,37): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(17,33): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(34,38): error: attributes are not allowed on the 'implementation' copies of formals
3 parse errors detected in WhereParsing.bpl
-WhereParsing0.bpl(17,38): error: where clause not allowed on bound variables
-WhereParsing0.bpl(18,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(19,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(20,38): error: where clause not allowed on bound variables
2 parse errors detected in WhereParsing0.bpl
-WhereParsing1.bpl(14,27): error: ")" expected
+WhereParsing1.bpl(16,27): error: ")" expected
1 parse errors detected in WhereParsing1.bpl
-WhereParsing2.bpl(1,14): error: ";" expected
+WhereParsing2.bpl(3,14): error: ";" expected
1 parse errors detected in WhereParsing2.bpl
-WhereResolution.bpl(28,38): Error: undeclared identifier: alpha
-WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts
+WhereResolution.bpl(30,38): Error: undeclared identifier: alpha
+WhereResolution.bpl(34,30): Error: old expressions allowed only in two-state contexts
2 name resolution errors detected in WhereResolution.bpl
-BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
-BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
+BadLabels0.bpl(6,2): Error: more than one declaration of block name: X
+BadLabels0.bpl(13,4): Error: more than one declaration of block name: Y
2 name resolution errors detected in BadLabels0.bpl
-BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined
-BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined
-BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
-BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
-BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
-BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
-BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
-BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
+BadLabels1.bpl(6,3): error: Error: goto label 'X' is undefined
+BadLabels1.bpl(7,3): error: Error: goto label 'Y' is undefined
+BadLabels1.bpl(49,3): error: Error: break statement is not inside a loop
+BadLabels1.bpl(51,5): error: Error: break statement is not inside a loop
+BadLabels1.bpl(62,5): error: Error: break label 'B' must designate an enclosing statement
+BadLabels1.bpl(65,5): error: Error: break label 'A' must designate an enclosing statement
+BadLabels1.bpl(66,5): error: Error: break label 'C' must designate an enclosing statement
+BadLabels1.bpl(67,8): error: Error: break label 'F' must designate an enclosing statement
8 parse errors detected in BadLabels1.bpl
-LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
-LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line
+LineParse.bpl(4,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
LineParse.bpl(6,2): error: EOF expected
5 parse errors detected in LineParse.bpl
-LineResolve.bpl(5,1): Error: undeclared identifier: a
-LineResolve.bpl(7,2): Error: undeclared identifier: b
+LineResolve.bpl(7,1): Error: undeclared identifier: a
+LineResolve.bpl(9,2): Error: undeclared identifier: b
LineResolve.bpl(12,0): Error: undeclared identifier: c
LineResolve.bpl(13,10): Error: undeclared identifier: d
LineResolve.bpl(12,0): Error: undeclared identifier: e
@@ -175,15 +175,15 @@ Abc.txt(99,0): Error: undeclared identifier: j c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
A B C . txt(12,0): Error: undeclared identifier: l
12 name resolution errors detected in LineResolve.bpl
-AttributeParsingErr.bpl(1,33): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(5,52): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(7,37): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(9,31): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(11,29): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(13,13): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(15,18): error: only attributes, not triggers, allowed here
-AttributeParsingErr.bpl(20,26): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(5,33): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(7,52): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(9,37): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(11,31): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(13,29): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(15,13): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(17,18): error: only attributes, not triggers, allowed here
+AttributeParsingErr.bpl(22,26): error: only attributes, not triggers, allowed here
9 parse errors detected in AttributeParsingErr.bpl
type {:sourcefile "test.ssc"} T;
@@ -231,15 +231,15 @@ procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P(); const again: int;
Boogie program verifier finished with 0 verified, 0 errors
-AttributeResolution.bpl(1,18): Error: undeclared identifier: foo
-AttributeResolution.bpl(3,18): Error: undeclared identifier: bar
-AttributeResolution.bpl(7,15): Error: undeclared identifier: qux
-AttributeResolution.bpl(7,41): Error: undeclared identifier: ij
-AttributeResolution.bpl(13,21): Error: undeclared identifier: bzzt
-AttributeResolution.bpl(15,20): Error: undeclared identifier: blt
-AttributeResolution.bpl(5,20): Error: undeclared identifier: baz
-AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
-AttributeResolution.bpl(11,29): Error: undeclared identifier: fux
+AttributeResolution.bpl(3,18): Error: undeclared identifier: foo
+AttributeResolution.bpl(5,18): Error: undeclared identifier: bar
+AttributeResolution.bpl(9,15): Error: undeclared identifier: qux
+AttributeResolution.bpl(9,41): Error: undeclared identifier: ij
+AttributeResolution.bpl(15,21): Error: undeclared identifier: bzzt
+AttributeResolution.bpl(17,20): Error: undeclared identifier: blt
+AttributeResolution.bpl(7,20): Error: undeclared identifier: baz
+AttributeResolution.bpl(11,18): Error: undeclared identifier: mux
+AttributeResolution.bpl(13,29): Error: undeclared identifier: fux
9 name resolution errors detected in AttributeResolution.bpl
function \true() : bool;
@@ -278,24 +278,24 @@ implementation qux(a: \procedure) Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
-MapsResolutionErrors.bpl(6,9): Error: type variable must occur in map arguments: b
-MapsResolutionErrors.bpl(20,10): Error: type variable must occur in procedure arguments: a
+MapsResolutionErrors.bpl(8,9): Error: type variable must occur in map arguments: b
+MapsResolutionErrors.bpl(22,10): Error: type variable must occur in procedure arguments: a
2 name resolution errors detected in MapsResolutionErrors.bpl
-Orderings.bpl(12,20): Error: undeclared identifier: x
-Orderings.bpl(15,23): Error: c0 occurs more than once as parent
-Orderings.bpl(16,19): Error: constant cannot be its own parent
-Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
+Orderings.bpl(14,20): Error: undeclared identifier: x
+Orderings.bpl(17,23): Error: c0 occurs more than once as parent
+Orderings.bpl(18,19): Error: constant cannot be its own parent
+Orderings.bpl(20,20): Error: the parent of a constant has to be a constant
4 name resolution errors detected in Orderings.bpl
-BadQuantifier.bpl(3,15): error: invalid QuantifierBody
+BadQuantifier.bpl(5,15): error: invalid QuantifierBody
1 parse errors detected in BadQuantifier.bpl
Boogie program verifier finished with 0 verified, 0 errors
----- SeparateVerification0.bpl
-SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
+SeparateVerification0.bpl(19,6): Error: undeclared identifier: y
1 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification1.bpl SeparateVerification0.bpl
-SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
-SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
+SeparateVerification1.bpl(6,6): Error: undeclared identifier: x
+SeparateVerification0.bpl(16,6): Error: undeclared identifier: x
2 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification0.bpl SeparateVerification0.bpl
diff --git a/Test/test0/Arrays0.bpl b/Test/test0/Arrays0.bpl index 0098c4a8..59ff8d14 100644 --- a/Test/test0/Arrays0.bpl +++ b/Test/test0/Arrays0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
var one: [int]int;
var two: [int,int]int;
var three: [int,int,int]int; // three's a crowd
diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl index db12ecb3..1f4b693c 100644 --- a/Test/test0/Arrays1.bpl +++ b/Test/test0/Arrays1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
var Q: [int,int][int]int;
procedure P()
diff --git a/Test/test0/Arrays1.bpl.expect b/Test/test0/Arrays1.bpl.expect new file mode 100644 index 00000000..534096ac --- /dev/null +++ b/Test/test0/Arrays1.bpl.expect @@ -0,0 +1,3 @@ +Arrays1.bpl(13,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q +Arrays1.bpl(16,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q +2 type checking errors detected in Arrays1.bpl diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl index e2b6101c..0b99dc5f 100644 --- a/Test/test0/AttributeParsing.bpl +++ b/Test/test0/AttributeParsing.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify -print:- -env:0 %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile "test.ssc"} T;
function {:source "test.scc"} f(int) returns (int);
diff --git a/Test/test0/AttributeParsing.bpl.expect b/Test/test0/AttributeParsing.bpl.expect new file mode 100644 index 00000000..c2d0289a --- /dev/null +++ b/Test/test0/AttributeParsing.bpl.expect @@ -0,0 +1,46 @@ + +type {:sourcefile "test.ssc"} T; + +function {:source "test.scc"} f(int) : int; + +const {:description "The largest integer value"} unique MAXINT: int; + +axiom {:naming "MyFavoriteAxiom"} (forall i: int :: { f(i) } f(i) == i + 1); + +var {:description "memory"} $Heap: [ref,name]any; + +var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref,name]any; + +procedure {:use_impl 1} foo(x: int) returns (n: int); + + + +implementation {:id 1} foo(x: int) returns (n: int) +{ + block1: + return; +} + + + +implementation {:id 2} foo(x: int) returns (n: int) +{ + block1: + return; +} + + + +type ref; + +type any; + +type name; + +procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P(); + + + +const again: int; + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test0/AttributeParsingErr.bpl b/Test/test0/AttributeParsingErr.bpl index cdf8646f..7329289f 100644 --- a/Test/test0/AttributeParsingErr.bpl +++ b/Test/test0/AttributeParsingErr.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile "test.ssc"} {1} T;
function {:source "test.scc"} {1} f(int) returns (int);
diff --git a/Test/test0/AttributeParsingErr.bpl.expect b/Test/test0/AttributeParsingErr.bpl.expect new file mode 100644 index 00000000..4fef56ed --- /dev/null +++ b/Test/test0/AttributeParsingErr.bpl.expect @@ -0,0 +1,10 @@ +AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(5,33): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(7,52): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(9,37): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(11,31): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(13,29): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(15,13): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(17,18): error: only attributes, not triggers, allowed here +AttributeParsingErr.bpl(22,26): error: only attributes, not triggers, allowed here +9 parse errors detected in AttributeParsingErr.bpl diff --git a/Test/test0/AttributeResolution.bpl b/Test/test0/AttributeResolution.bpl index c667b530..eae2878e 100644 --- a/Test/test0/AttributeResolution.bpl +++ b/Test/test0/AttributeResolution.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type {:sourcefile foo} T;
function {:source bar} f(int) returns (int);
diff --git a/Test/test0/AttributeResolution.bpl.expect b/Test/test0/AttributeResolution.bpl.expect new file mode 100644 index 00000000..1a7a43fa --- /dev/null +++ b/Test/test0/AttributeResolution.bpl.expect @@ -0,0 +1,10 @@ +AttributeResolution.bpl(3,18): Error: undeclared identifier: foo +AttributeResolution.bpl(5,18): Error: undeclared identifier: bar +AttributeResolution.bpl(9,15): Error: undeclared identifier: qux +AttributeResolution.bpl(9,41): Error: undeclared identifier: ij +AttributeResolution.bpl(15,21): Error: undeclared identifier: bzzt +AttributeResolution.bpl(17,20): Error: undeclared identifier: blt +AttributeResolution.bpl(7,20): Error: undeclared identifier: baz +AttributeResolution.bpl(11,18): Error: undeclared identifier: mux +AttributeResolution.bpl(13,29): Error: undeclared identifier: fux +9 name resolution errors detected in AttributeResolution.bpl diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl index 89cf7a36..ec6ff744 100644 --- a/Test/test0/BadLabels0.bpl +++ b/Test/test0/BadLabels0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure Dup(y: int)
{
X:
diff --git a/Test/test0/BadLabels0.bpl.expect b/Test/test0/BadLabels0.bpl.expect new file mode 100644 index 00000000..619a88e8 --- /dev/null +++ b/Test/test0/BadLabels0.bpl.expect @@ -0,0 +1,3 @@ +BadLabels0.bpl(6,2): Error: more than one declaration of block name: X +BadLabels0.bpl(13,4): Error: more than one declaration of block name: Y +2 name resolution errors detected in BadLabels0.bpl diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl index c040ce26..cbbe0f5e 100644 --- a/Test/test0/BadLabels1.bpl +++ b/Test/test0/BadLabels1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure P0()
{
// these labels don't exist at all
diff --git a/Test/test0/BadLabels1.bpl.expect b/Test/test0/BadLabels1.bpl.expect new file mode 100644 index 00000000..e722a1b1 --- /dev/null +++ b/Test/test0/BadLabels1.bpl.expect @@ -0,0 +1,9 @@ +BadLabels1.bpl(6,3): error: Error: goto label 'X' is undefined +BadLabels1.bpl(7,3): error: Error: goto label 'Y' is undefined +BadLabels1.bpl(49,3): error: Error: break statement is not inside a loop +BadLabels1.bpl(51,5): error: Error: break statement is not inside a loop +BadLabels1.bpl(62,5): error: Error: break label 'B' must designate an enclosing statement +BadLabels1.bpl(65,5): error: Error: break label 'A' must designate an enclosing statement +BadLabels1.bpl(66,5): error: Error: break label 'C' must designate an enclosing statement +BadLabels1.bpl(67,8): error: Error: break label 'F' must designate an enclosing statement +8 parse errors detected in BadLabels1.bpl diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl index b06ab0d9..d202312e 100644 --- a/Test/test0/BadQuantifier.bpl +++ b/Test/test0/BadQuantifier.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
function f(int) returns (bool);
axiom (forall int x :: f(x) <== x >= 0);
diff --git a/Test/test0/BadQuantifier.bpl.expect b/Test/test0/BadQuantifier.bpl.expect new file mode 100644 index 00000000..bf16fef7 --- /dev/null +++ b/Test/test0/BadQuantifier.bpl.expect @@ -0,0 +1,2 @@ +BadQuantifier.bpl(5,15): error: invalid QuantifierBody +1 parse errors detected in BadQuantifier.bpl diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl index d45633e9..aba48668 100644 --- a/Test/test0/EmptyCallArgs.bpl +++ b/Test/test0/EmptyCallArgs.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
type C;
procedure P(x:int, y:bool) returns (z:C);
@@ -17,4 +19,4 @@ procedure CallQ() { var z:bool;
call z := Q(x, y);
-}
\ No newline at end of file +}
diff --git a/Test/test0/LargeLiterals0.bpl b/Test/test0/LargeLiterals0.bpl index be459bf5..b061688f 100644 --- a/Test/test0/LargeLiterals0.bpl +++ b/Test/test0/LargeLiterals0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// Test to parse large integer literals
axiom 1234567890987654321 == 1234567890987654321;
diff --git a/Test/test0/LineParse.bpl b/Test/test0/LineParse.bpl index a64eed0b..ae11b419 100644 --- a/Test/test0/LineParse.bpl +++ b/Test/test0/LineParse.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
#line
#line
#line 0
diff --git a/Test/test0/LineParse.bpl.expect b/Test/test0/LineParse.bpl.expect new file mode 100644 index 00000000..668e57dc --- /dev/null +++ b/Test/test0/LineParse.bpl.expect @@ -0,0 +1,6 @@ +LineParse.bpl(3,0): error: Malformed (#line num [filename]) pragma: #line +LineParse.bpl(4,0): error: Malformed (#line num [filename]) pragma: #line +LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is +LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0) +LineParse.bpl(6,2): error: EOF expected +5 parse errors detected in LineParse.bpl diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl index b0c578c7..097943f5 100644 --- a/Test/test0/LineResolve.bpl +++ b/Test/test0/LineResolve.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
procedure P() {
var x: int;
x :=
diff --git a/Test/test0/LineResolve.bpl.expect b/Test/test0/LineResolve.bpl.expect new file mode 100644 index 00000000..6ca45551 --- /dev/null +++ b/Test/test0/LineResolve.bpl.expect @@ -0,0 +1,13 @@ +LineResolve.bpl(7,1): Error: undeclared identifier: a +LineResolve.bpl(9,2): Error: undeclared identifier: b +LineResolve.bpl(12,0): Error: undeclared identifier: c +LineResolve.bpl(13,10): Error: undeclared identifier: d +LineResolve.bpl(12,0): Error: undeclared identifier: e +LineResolve.bpl(2,0): Error: undeclared identifier: f +LineResolve.bpl(900,0): Error: undeclared identifier: g +Abc.txt(11,3): Error: undeclared identifier: h +Abc.txt(13,0): Error: undeclared identifier: i +Abc.txt(99,0): Error: undeclared identifier: j +c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k +A B C . txt(12,0): Error: undeclared identifier: l +12 name resolution errors detected in LineResolve.bpl diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl index d529cb9c..8e5d5149 100644 --- a/Test/test0/MapsResolutionErrors.bpl +++ b/Test/test0/MapsResolutionErrors.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
var m: []int;
var p: <a>[]a;
diff --git a/Test/test0/MapsResolutionErrors.bpl.expect b/Test/test0/MapsResolutionErrors.bpl.expect new file mode 100644 index 00000000..10070c23 --- /dev/null +++ b/Test/test0/MapsResolutionErrors.bpl.expect @@ -0,0 +1,3 @@ +MapsResolutionErrors.bpl(8,9): Error: type variable must occur in map arguments: b +MapsResolutionErrors.bpl(22,10): Error: type variable must occur in procedure arguments: a +2 name resolution errors detected in MapsResolutionErrors.bpl diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index 5fffc20a..05ab3c05 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// ----------- BEGIN PRELUDE
diff --git a/Test/test0/NoErrors.expect b/Test/test0/NoErrors.expect new file mode 100644 index 00000000..cc5cde4d --- /dev/null +++ b/Test/test0/NoErrors.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl index 0ba6c69c..b14dbd4b 100644 --- a/Test/test0/Orderings.bpl +++ b/Test/test0/Orderings.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type C;
diff --git a/Test/test0/Orderings.bpl.expect b/Test/test0/Orderings.bpl.expect new file mode 100644 index 00000000..d58cdc46 --- /dev/null +++ b/Test/test0/Orderings.bpl.expect @@ -0,0 +1,5 @@ +Orderings.bpl(14,20): Error: undeclared identifier: x +Orderings.bpl(17,23): Error: c0 occurs more than once as parent +Orderings.bpl(18,19): Error: constant cannot be its own parent +Orderings.bpl(20,20): Error: the parent of a constant has to be a constant +4 name resolution errors detected in Orderings.bpl diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index 7e4a9ce7..bc22e46d 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify -printInstrumented %s > %t
+// RUN: %diff %s.expect %t
const x: int;
const y: int;
const z: int;
diff --git a/Test/test0/PrettyPrint.bpl.expect b/Test/test0/PrettyPrint.bpl.expect new file mode 100644 index 00000000..f6f0f995 --- /dev/null +++ b/Test/test0/PrettyPrint.bpl.expect @@ -0,0 +1,93 @@ +const x: int; + +const y: int; + +const z: int; + +const r: real; + +const s: real; + +const t: real; + +const P: bool; + +const Q: bool; + +const R: bool; + +axiom x * (y + z) == x + y * z; + +axiom x * y + z == (x + y) * z; + +axiom x * y * z == x * y * z; + +axiom x * y * z * x == x * y * z; + +axiom x div y div z == x div (y div z); + +axiom x div y div (z div x) == x div y div z; + +axiom x + y mod z == y mod z + x; + +axiom (x + y) mod z == x mod z + y mod z; + +axiom x / y / z == x / (y / z); + +axiom x / y / (z / x) == x / y / z; + +axiom x / s / z == x / (s / z); + +axiom x / s / (z / x) == x / s / z; + +axiom r / s / t == r / (s / t); + +axiom r / s / (t / r) == r / s / t; + +axiom r * s / t == r * s / t; + +axiom r / s * t == r / s * t; + +axiom (r * s) ** t == r ** t * s ** t; + +axiom r ** (s + t) == r ** s * r ** t; + +axiom int(real(x)) == x; + +axiom r >= 0e0 ==> real(int(r)) <= r; + +axiom int(0e0 - 2e-2) == 0; + +axiom int(0e0 - 35e0) == -35; + +axiom int(27e-1) == 2; + +axiom x - y - z == x - (y - z); + +axiom x - y - (z - x) == x - y - z; + +axiom x + y - z - x + y == 0; + +axiom x + y - z - x + y == x + y - (z - (x + y)); + +axiom P ==> Q ==> R <==> P ==> Q ==> R; + +axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R; + +axiom P <==> Q <==> R; + +axiom P ==> Q <==> Q ==> R <==> R ==> P; + +axiom (P && Q) || (Q && R); + +axiom (P || Q) && (Q || R); + +axiom P || Q || Q || R; + +axiom P && Q && Q && R; + +function f(int) : int; + +axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200); + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index 79a4d2ab..974bd9eb 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff NoErrors.expect %t
// BoogiePL Examples
type elements;
diff --git a/Test/test0/Quoting.bpl b/Test/test0/Quoting.bpl index eaf8fe7a..64564ad9 100644 --- a/Test/test0/Quoting.bpl +++ b/Test/test0/Quoting.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify -print:- -env:0 %s > %t
+// RUN: %diff %s.expect %t
function \true() returns(bool);
type \procedure;
diff --git a/Test/test0/Quoting.bpl.expect b/Test/test0/Quoting.bpl.expect new file mode 100644 index 00000000..3a1037aa --- /dev/null +++ b/Test/test0/Quoting.bpl.expect @@ -0,0 +1,35 @@ + +function \true() : bool; + +type \procedure; + +procedure \old(any: \procedure) returns (\var: \procedure); + + + +implementation \old(any: \procedure) returns (\var: \procedure) +{ + var \modifies: \procedure; + + \modifies := any; + \var := \modifies; +} + + + +procedure qux(a: \procedure); + + + +implementation qux(a: \procedure) +{ + var \var: \procedure; + var x: bool; + + call \var := \old(a); + x := \true(); +} + + + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl index 5a8ef283..f598fe6f 100644 --- a/Test/test0/SeparateVerification0.bpl +++ b/Test/test0/SeparateVerification0.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
+// RUN: %boogie -noVerify %s %s > %t
+// RUN: %diff NoErrors.expect %t
+// RUN: %boogie -noVerify %s %s SeparateVerification1.bpl > %t
+// RUN: %diff NoErrors.expect %t
// need to include this file twice for it to include all necessary declarations
#if FILE_0
diff --git a/Test/test0/SeparateVerification0.bpl.expect b/Test/test0/SeparateVerification0.bpl.expect new file mode 100644 index 00000000..ab1318bd --- /dev/null +++ b/Test/test0/SeparateVerification0.bpl.expect @@ -0,0 +1,2 @@ +SeparateVerification0.bpl(19,6): Error: undeclared identifier: y +1 name resolution errors detected in SeparateVerification0.bpl diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl index 0e3e7926..683b24e1 100644 --- a/Test/test0/SeparateVerification1.bpl +++ b/Test/test0/SeparateVerification1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s SeparateVerification0.bpl > %t
+// RUN: %diff %s.expect %t
// to be used with SeparateVerification0.bpl
// x and y are declared in SeparateVerification0.bpl
diff --git a/Test/test0/SeparateVerification1.bpl.expect b/Test/test0/SeparateVerification1.bpl.expect new file mode 100644 index 00000000..48b21162 --- /dev/null +++ b/Test/test0/SeparateVerification1.bpl.expect @@ -0,0 +1,3 @@ +SeparateVerification1.bpl(6,6): Error: undeclared identifier: x +SeparateVerification0.bpl(16,6): Error: undeclared identifier: x +2 name resolution errors detected in SeparateVerification0.bpl diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl index 6750d77d..bbf37517 100644 --- a/Test/test0/Triggers0.bpl +++ b/Test/test0/Triggers0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
// Trigger errors
function f(int, int) returns (int);
diff --git a/Test/test0/Triggers0.bpl.expect b/Test/test0/Triggers0.bpl.expect new file mode 100644 index 00000000..72ee6160 --- /dev/null +++ b/Test/test0/Triggers0.bpl.expect @@ -0,0 +1,2 @@ +Triggers0.bpl(16,31): error: the 'nopats' quantifier attribute expects a string-literal parameter +1 parse errors detected in Triggers0.bpl diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl index d079ea03..bda65ea2 100644 --- a/Test/test0/Triggers1.bpl +++ b/Test/test0/Triggers1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
// Trigger errors
function f(int, int) returns (int);
diff --git a/Test/test0/Triggers1.bpl.expect b/Test/test0/Triggers1.bpl.expect new file mode 100644 index 00000000..d7ede824 --- /dev/null +++ b/Test/test0/Triggers1.bpl.expect @@ -0,0 +1,21 @@ +Triggers1.bpl(9,17): Error: boolean operators are not allowed in triggers +Triggers1.bpl(13,21): Error: boolean operators are not allowed in triggers +Triggers1.bpl(17,9): Error: boolean operators are not allowed in triggers +Triggers1.bpl(21,10): Error: boolean operators are not allowed in triggers +Triggers1.bpl(25,17): Error: boolean operators are not allowed in triggers +Triggers1.bpl(29,17): Error: boolean operators are not allowed in triggers +Triggers1.bpl(34,17): Error: equality is not allowed in triggers +Triggers1.bpl(38,17): Error: arithmetic comparisons are not allowed in triggers +Triggers1.bpl(47,10): Error: quantifiers are not allowed in triggers +Triggers1.bpl(55,7): Error: trigger must mention all quantified variables, but does not mention: x +Triggers1.bpl(63,7): Error: trigger must mention all quantified variables, but does not mention: y +Triggers1.bpl(64,7): Error: trigger must mention all quantified variables, but does not mention: x +Triggers1.bpl(72,9): Error: a matching pattern must be more than just a variable by itself: x +Triggers1.bpl(84,7): Error: trigger must mention all quantified variables, but does not mention: z +Triggers1.bpl(96,16): Error: a matching pattern must be more than just a variable by itself: x +Triggers1.bpl(97,16): Error: a matching pattern must be more than just a variable by itself: g +Triggers1.bpl(107,40): Error: trigger must mention all quantified variables, but does not mention: y +Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: z +Triggers1.bpl(121,33): Error: cannot refer to a global variable in this context: h1 +Triggers1.bpl(122,33): Error: cannot refer to a global variable in this context: h0 +20 name resolution errors detected in Triggers1.bpl diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl index 7bb1dcef..4e6e607b 100644 --- a/Test/test0/Types0.bpl +++ b/Test/test0/Types0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type T, U;
type V;
diff --git a/Test/test0/Types0.bpl.expect b/Test/test0/Types0.bpl.expect new file mode 100644 index 00000000..046c6ceb --- /dev/null +++ b/Test/test0/Types0.bpl.expect @@ -0,0 +1,3 @@ +Types0.bpl(8,18): error: expected identifier before ':' +Types0.bpl(8,12): error: expecting an identifier as parameter name +2 parse errors detected in Types0.bpl diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl index 4c6e31ae..1e4d7033 100644 --- a/Test/test0/Types1.bpl +++ b/Test/test0/Types1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type T, U;
type V;
diff --git a/Test/test0/Types1.bpl.expect b/Test/test0/Types1.bpl.expect new file mode 100644 index 00000000..6c9f6784 --- /dev/null +++ b/Test/test0/Types1.bpl.expect @@ -0,0 +1,4 @@ +Types1.bpl(8,11): Error: undeclared type: x +Types1.bpl(9,11): Error: undeclared type: x +Types1.bpl(9,14): Error: undeclared type: x +3 name resolution errors detected in Types1.bpl diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl index 33e500d6..6c203258 100644 --- a/Test/test0/WhereParsing.bpl +++ b/Test/test0/WhereParsing.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing.bpl.expect b/Test/test0/WhereParsing.bpl.expect new file mode 100644 index 00000000..d6621f60 --- /dev/null +++ b/Test/test0/WhereParsing.bpl.expect @@ -0,0 +1,4 @@ +WhereParsing.bpl(16,37): error: where clause not allowed on the 'implementation' copies of formals +WhereParsing.bpl(17,33): error: where clause not allowed on the 'implementation' copies of formals +WhereParsing.bpl(34,38): error: attributes are not allowed on the 'implementation' copies of formals +3 parse errors detected in WhereParsing.bpl diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl index f99dc1ab..7b3d21b2 100644 --- a/Test/test0/WhereParsing0.bpl +++ b/Test/test0/WhereParsing0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing0.bpl.expect b/Test/test0/WhereParsing0.bpl.expect new file mode 100644 index 00000000..c41c598d --- /dev/null +++ b/Test/test0/WhereParsing0.bpl.expect @@ -0,0 +1,3 @@ +WhereParsing0.bpl(19,38): error: where clause not allowed on bound variables +WhereParsing0.bpl(20,38): error: where clause not allowed on bound variables +2 parse errors detected in WhereParsing0.bpl diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl index 402071bf..7be165d2 100644 --- a/Test/test0/WhereParsing1.bpl +++ b/Test/test0/WhereParsing1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int;
function R(int) returns (bool);
diff --git a/Test/test0/WhereParsing1.bpl.expect b/Test/test0/WhereParsing1.bpl.expect new file mode 100644 index 00000000..ad079f26 --- /dev/null +++ b/Test/test0/WhereParsing1.bpl.expect @@ -0,0 +1,2 @@ +WhereParsing1.bpl(16,27): error: ")" expected +1 parse errors detected in WhereParsing1.bpl diff --git a/Test/test0/WhereParsing2.bpl b/Test/test0/WhereParsing2.bpl index d85287f3..e098036f 100644 --- a/Test/test0/WhereParsing2.bpl +++ b/Test/test0/WhereParsing2.bpl @@ -1,2 +1,4 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
const x: int where x < 0; // error: where clauses not allowed on constants
diff --git a/Test/test0/WhereParsing2.bpl.expect b/Test/test0/WhereParsing2.bpl.expect new file mode 100644 index 00000000..17484299 --- /dev/null +++ b/Test/test0/WhereParsing2.bpl.expect @@ -0,0 +1,2 @@ +WhereParsing2.bpl(3,14): error: ";" expected +1 parse errors detected in WhereParsing2.bpl diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl index 6b28a035..0c2cf539 100644 --- a/Test/test0/WhereResolution.bpl +++ b/Test/test0/WhereResolution.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t
+// RUN: %diff %s.expect %t
type double;
function R(int) returns (bool);
diff --git a/Test/test0/WhereResolution.bpl.expect b/Test/test0/WhereResolution.bpl.expect new file mode 100644 index 00000000..27cdd915 --- /dev/null +++ b/Test/test0/WhereResolution.bpl.expect @@ -0,0 +1,3 @@ +WhereResolution.bpl(30,38): Error: undeclared identifier: alpha +WhereResolution.bpl(34,30): Error: old expressions allowed only in two-state contexts +2 name resolution errors detected in WhereResolution.bpl |