From 3b38b009d086c601cae884ad62ceeb9bb16ae5d5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 5 May 2014 19:51:59 +0100 Subject: Enabled most of the name resolution lit tests. They don't all pass yet due to a bug in -useBaseNameForFileName. --- Test/test0/Answer | 156 ++++++++++++++-------------- Test/test0/Arrays0.bpl | 2 + Test/test0/Arrays1.bpl | 2 + Test/test0/Arrays1.bpl.expect | 3 + Test/test0/AttributeParsing.bpl | 2 + Test/test0/AttributeParsing.bpl.expect | 46 ++++++++ Test/test0/AttributeParsingErr.bpl | 2 + Test/test0/AttributeParsingErr.bpl.expect | 10 ++ Test/test0/AttributeResolution.bpl | 2 + Test/test0/AttributeResolution.bpl.expect | 10 ++ Test/test0/BadLabels0.bpl | 2 + Test/test0/BadLabels0.bpl.expect | 3 + Test/test0/BadLabels1.bpl | 2 + Test/test0/BadLabels1.bpl.expect | 9 ++ Test/test0/BadQuantifier.bpl | 2 + Test/test0/BadQuantifier.bpl.expect | 2 + Test/test0/EmptyCallArgs.bpl | 4 +- Test/test0/LargeLiterals0.bpl | 2 + Test/test0/LineParse.bpl | 2 + Test/test0/LineParse.bpl.expect | 6 ++ Test/test0/LineResolve.bpl | 2 + Test/test0/LineResolve.bpl.expect | 13 +++ Test/test0/MapsResolutionErrors.bpl | 2 + Test/test0/MapsResolutionErrors.bpl.expect | 3 + Test/test0/ModifiedBag.bpl | 2 + Test/test0/NoErrors.expect | 2 + Test/test0/Orderings.bpl | 2 + Test/test0/Orderings.bpl.expect | 5 + Test/test0/PrettyPrint.bpl | 2 + Test/test0/PrettyPrint.bpl.expect | 93 +++++++++++++++++ Test/test0/Prog0.bpl | 2 + Test/test0/Quoting.bpl | 2 + Test/test0/Quoting.bpl.expect | 35 +++++++ Test/test0/SeparateVerification0.bpl | 6 ++ Test/test0/SeparateVerification0.bpl.expect | 2 + Test/test0/SeparateVerification1.bpl | 2 + Test/test0/SeparateVerification1.bpl.expect | 3 + Test/test0/Triggers0.bpl | 2 + Test/test0/Triggers0.bpl.expect | 2 + Test/test0/Triggers1.bpl | 2 + Test/test0/Triggers1.bpl.expect | 21 ++++ Test/test0/Types0.bpl | 2 + Test/test0/Types0.bpl.expect | 3 + Test/test0/Types1.bpl | 2 + Test/test0/Types1.bpl.expect | 4 + Test/test0/WhereParsing.bpl | 2 + Test/test0/WhereParsing.bpl.expect | 4 + Test/test0/WhereParsing0.bpl | 2 + Test/test0/WhereParsing0.bpl.expect | 3 + Test/test0/WhereParsing1.bpl | 2 + Test/test0/WhereParsing1.bpl.expect | 2 + Test/test0/WhereParsing2.bpl | 2 + Test/test0/WhereParsing2.bpl.expect | 2 + Test/test0/WhereResolution.bpl | 2 + Test/test0/WhereResolution.bpl.expect | 3 + 55 files changed, 430 insertions(+), 79 deletions(-) create mode 100644 Test/test0/Arrays1.bpl.expect create mode 100644 Test/test0/AttributeParsing.bpl.expect create mode 100644 Test/test0/AttributeParsingErr.bpl.expect create mode 100644 Test/test0/AttributeResolution.bpl.expect create mode 100644 Test/test0/BadLabels0.bpl.expect create mode 100644 Test/test0/BadLabels1.bpl.expect create mode 100644 Test/test0/BadQuantifier.bpl.expect create mode 100644 Test/test0/LineParse.bpl.expect create mode 100644 Test/test0/LineResolve.bpl.expect create mode 100644 Test/test0/MapsResolutionErrors.bpl.expect create mode 100644 Test/test0/NoErrors.expect create mode 100644 Test/test0/Orderings.bpl.expect create mode 100644 Test/test0/PrettyPrint.bpl.expect create mode 100644 Test/test0/Quoting.bpl.expect create mode 100644 Test/test0/SeparateVerification0.bpl.expect create mode 100644 Test/test0/SeparateVerification1.bpl.expect create mode 100644 Test/test0/Triggers0.bpl.expect create mode 100644 Test/test0/Triggers1.bpl.expect create mode 100644 Test/test0/Types0.bpl.expect create mode 100644 Test/test0/Types1.bpl.expect create mode 100644 Test/test0/WhereParsing.bpl.expect create mode 100644 Test/test0/WhereParsing0.bpl.expect create mode 100644 Test/test0/WhereParsing1.bpl.expect create mode 100644 Test/test0/WhereParsing2.bpl.expect create mode 100644 Test/test0/WhereResolution.bpl.expect (limited to 'Test/test0') 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; 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 -- cgit v1.2.3