From 0ac9e0dde34a98a3f97f26dd224ff5b9d5b13630 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 18:08:49 +0100 Subject: Enabled tests for types introduced in Boogie2 as lit tests. --- Test/test20/Answer | 158 ++++++++++++++--------------- Test/test20/Coercions.bpl | 2 + Test/test20/Coercions.bpl.expect | 5 + Test/test20/EmptySeq.bpl | 2 + Test/test20/EmptySeq.bpl.expect | 2 + Test/test20/ParallelAssignment.bpl | 2 + Test/test20/ParallelAssignment.bpl.expect | 4 + Test/test20/ParallelAssignment2.bpl | 2 + Test/test20/ParallelAssignment2.bpl.expect | 3 + Test/test20/PolyFuns0.bpl | 2 + Test/test20/PolyFuns0.bpl.expect | 5 + Test/test20/PolyFuns1.bpl | 2 + Test/test20/PolyFuns1.bpl.expect | 17 ++++ Test/test20/PolyPolyPoly.bpl | 2 + Test/test20/PolyPolyPoly.bpl.expect | 4 + Test/test20/PolyPolyPoly2.bpl | 2 + Test/test20/PolyPolyPoly2.bpl.expect | 12 +++ Test/test20/PolyProcs0.bpl | 2 + Test/test20/PolyProcs0.bpl.expect | 7 ++ Test/test20/ProcParamReordering.bpl | 2 + Test/test20/ProcParamReordering.bpl.expect | 3 + Test/test20/Prog0.bpl | 2 + Test/test20/Prog0.bpl.expect | 5 + Test/test20/Prog1.bpl | 2 + Test/test20/Prog1.bpl.expect | 4 + Test/test20/Prog2.bpl | 2 + Test/test20/Prog2.bpl.expect | 2 + Test/test20/TypeDecls0.bpl | 2 + Test/test20/TypeDecls0.bpl.expect | 13 +++ Test/test20/TypeDecls1.bpl | 2 + Test/test20/TypeDecls1.bpl.expect | 5 + Test/test20/TypeSynonyms0.bpl | 4 + Test/test20/TypeSynonyms0.bpl.expect | 7 ++ Test/test20/TypeSynonyms0.bpl.print.expect | 37 +++++++ Test/test20/TypeSynonyms1.bpl | 2 + Test/test20/TypeSynonyms1.bpl.expect | 2 + Test/test20/TypeSynonyms2.bpl | 4 + Test/test20/TypeSynonyms2.bpl.expect | 2 + Test/test20/TypeSynonyms2.bpl.print.expect | 52 ++++++++++ 39 files changed, 310 insertions(+), 79 deletions(-) create mode 100644 Test/test20/Coercions.bpl.expect create mode 100644 Test/test20/EmptySeq.bpl.expect create mode 100644 Test/test20/ParallelAssignment.bpl.expect create mode 100644 Test/test20/ParallelAssignment2.bpl.expect create mode 100644 Test/test20/PolyFuns0.bpl.expect create mode 100644 Test/test20/PolyFuns1.bpl.expect create mode 100644 Test/test20/PolyPolyPoly.bpl.expect create mode 100644 Test/test20/PolyPolyPoly2.bpl.expect create mode 100644 Test/test20/PolyProcs0.bpl.expect create mode 100644 Test/test20/ProcParamReordering.bpl.expect create mode 100644 Test/test20/Prog0.bpl.expect create mode 100644 Test/test20/Prog1.bpl.expect create mode 100644 Test/test20/Prog2.bpl.expect create mode 100644 Test/test20/TypeDecls0.bpl.expect create mode 100644 Test/test20/TypeDecls1.bpl.expect create mode 100644 Test/test20/TypeSynonyms0.bpl.expect create mode 100644 Test/test20/TypeSynonyms0.bpl.print.expect create mode 100644 Test/test20/TypeSynonyms1.bpl.expect create mode 100644 Test/test20/TypeSynonyms2.bpl.expect create mode 100644 Test/test20/TypeSynonyms2.bpl.print.expect (limited to 'Test/test20') diff --git a/Test/test20/Answer b/Test/test20/Answer index 4127471b..7e7af57b 100644 --- a/Test/test20/Answer +++ b/Test/test20/Answer @@ -1,69 +1,69 @@ -TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C -TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a -TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a -TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b -TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C -TypeDecls0.bpl(24,9): Error: undeclared type: A0 -TypeDecls0.bpl(25,9): Error: undeclared type: F -TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(22,5): Error: more than one declaration of type name: C +TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a +TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a +TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b +TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C +TypeDecls0.bpl(26,9): Error: undeclared type: A0 +TypeDecls0.bpl(27,9): Error: undeclared type: F TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E -TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(40,11): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(40,13): Error: type constructor received wrong number of arguments: E 12 name resolution errors detected in TypeDecls0.bpl -TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: [b]a) -TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool) -TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: [[b]a]bool (expected: [b]a) +TypeDecls1.bpl(9,13): Error: invalid type for argument 0 in map select: int (expected: [b]a) +TypeDecls1.bpl(15,25): Error: right-hand side in map store with wrong type: int (expected: bool) +TypeDecls1.bpl(21,36): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: [[b]a]bool (expected: [b]a) 4 type checking errors detected in TypeDecls1.bpl -Prog0.bpl(17,10): Error: type variable must occur in map arguments: a -Prog0.bpl(29,27): Error: more than one declaration of type variable: beta -Prog0.bpl(32,22): Error: undeclared type: alpha -Prog0.bpl(33,35): Error: undeclared type: alpha +Prog0.bpl(19,10): Error: type variable must occur in map arguments: a +Prog0.bpl(31,27): Error: more than one declaration of type variable: beta +Prog0.bpl(34,22): Error: undeclared type: alpha +Prog0.bpl(35,35): Error: undeclared type: alpha 4 name resolution errors detected in Prog0.bpl -Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref) -Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a) -Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >= +Prog1.bpl(20,11): Error: invalid type for argument 0 in map select: int (expected: ref) +Prog1.bpl(21,14): Error: invalid type for argument 1 in map select: int (expected: Field a) +Prog1.bpl(22,17): Error: invalid argument types (bool and int) to binary operator >= 3 type checking errors detected in Prog1.bpl -Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either +Prog2.bpl(8,14): Error: trigger does not mention alpha, which does not occur in variables types either 1 type checking errors detected in Prog2.bpl -PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a) -PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a) -PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a) -PolyFuns0.bpl(53,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +PolyFuns0.bpl(25,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a) +PolyFuns0.bpl(42,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a) +PolyFuns0.bpl(43,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a) +PolyFuns0.bpl(55,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == 4 type checking errors detected in PolyFuns0.bpl -PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) -PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) -PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) -PolyFuns1.bpl(17,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == -PolyFuns1.bpl(18,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == -PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu:
[Field dd]dd (expected: [Field c]a) -PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: [Field cc]T (expected: [Field d]d) -PolyFuns1.bpl(30,12): Error: invalid argument types ([Field cc]T and
[Field dd]dd) to binary operator == -PolyFuns1.bpl(31,12): Error: invalid argument types (
[Field dd]dd (expected: [Field c]a) +PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: [Field cc]T (expected: [Field d]d) +PolyFuns1.bpl(32,12): Error: invalid argument types ([Field cc]T and
[Field dd]dd) to binary operator == +PolyFuns1.bpl(33,12): Error: invalid argument types (
[Field dd]dd and [Field cc]T) to binary operator == +PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: [Field T]ee (expected: [Field d]d) +PolyFuns1.bpl(43,11): Error: invalid argument types ([a,a]int and [b,int]int) to binary operator == +PolyFuns1.bpl(44,11): Error: invalid argument types ([b,int]int and [int,c]int) to binary operator == +PolyFuns1.bpl(45,11): Error: invalid argument types ([a,a]int and [int,c]int) to binary operator == +PolyFuns1.bpl(52,11): Error: invalid argument types ([a,a,b]int and [a,b,b]int) to binary operator == +PolyFuns1.bpl(59,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator == 16 type checking errors detected in PolyFuns1.bpl -PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref) -PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a) -PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref) -PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) -PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int) -PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) +PolyProcs0.bpl(13,16): Error: invalid type for argument 0 in map select: Field b (expected: ref) +PolyProcs0.bpl(13,19): Error: invalid type for argument 1 in map select: ref (expected: Field a) +PolyProcs0.bpl(23,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref) +PolyProcs0.bpl(23,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) +PolyProcs0.bpl(27,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int) +PolyProcs0.bpl(28,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) 6 type checking errors detected in PolyProcs0.bpl -TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) -TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field -TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set -TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a +TypeSynonyms0.bpl(13,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(14,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(16,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(26,10): Error: type constructor received wrong number of arguments: Field +TypeSynonyms0.bpl(27,10): Error: type synonym received wrong number of arguments: Set +TypeSynonyms0.bpl(30,10): Error: type variable must occur in map arguments: a 6 name resolution errors detected in TypeSynonyms0.bpl -TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: [b,b,[b2,b,int]int]int (expected: nested2) +TypeSynonyms1.bpl(48,8): Error: invalid type for argument 0 in application of h: [b,b,[b2,b,int]int]int (expected: nested2) 1 type checking errors detected in TypeSynonyms1.bpl Boogie program verifier finished with 1 verified, 0 errors @@ -156,36 +156,36 @@ implementation P() Boogie program verifier finished with 0 verified, 0 errors -PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and []C a) to binary operator == -PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and []C a) to binary operator == -PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a) +PolyPolyPoly.bpl(14,26): Error: invalid argument types ([]? and []C a) to binary operator == +PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and []C a) to binary operator == +PolyPolyPoly.bpl(23,57): Error: invalid type for argument 1 in map select: b (expected: a) 3 type checking errors detected in PolyPolyPoly.bpl -PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to [arg0]res -PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17 -PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17 -PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0 -PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int -PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(9,8): Warning: type parameter a is ambiguous, instantiating to [arg0]res +PolyPolyPoly2.bpl(13,8): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(13,15): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(13,27): Warning: type parameter a is ambiguous, instantiating to bv17 +PolyPolyPoly2.bpl(14,8): Warning: type parameter a is ambiguous, instantiating to bv17 +PolyPolyPoly2.bpl(14,15): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(24,7): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(34,3): Warning: type parameter a is ambiguous, instantiating to int Boogie program verifier finished with 0 verified, 0 errors -ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation) -ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P +ProcParamReordering.bpl(15,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation) +ProcParamReordering.bpl(17,15): Error: mismatched number of type parameters in procedure implementation: P 2 type checking errors detected in ProcParamReordering.bpl -ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int) -ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int) -ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z +ParallelAssignment.bpl(19,2): Error: mismatched types in assignment command (cannot assign bool to int) +ParallelAssignment.bpl(20,4): Error: invalid type for argument 0 in map assignment: bool (expected: int) +ParallelAssignment.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z 3 type checking errors detected in ParallelAssignment.bpl -ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides -ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment +ParallelAssignment2.bpl(11,7): Error: number of left-hand sides does not match number of right-hand sides +ParallelAssignment2.bpl(12,9): Error: variable a is assigned more than once in parallel assignment 2 name resolution errors detected in ParallelAssignment2.bpl -Coercions.bpl(11,8): Error: int cannot be coerced to E [a]int -Coercions.bpl(13,8): Error: C cannot be coerced to D -Coercions.bpl(15,9): Error: int cannot be coerced to D -Coercions.bpl(16,9): Error: int cannot be coerced to E int +Coercions.bpl(13,8): Error: int cannot be coerced to E [a]int +Coercions.bpl(15,8): Error: C cannot be coerced to D +Coercions.bpl(17,9): Error: int cannot be coerced to D +Coercions.bpl(18,9): Error: int cannot be coerced to E int 4 type checking errors detected in Coercions.bpl Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl index cab68149..3836332a 100644 --- a/Test/test20/Coercions.bpl +++ b/Test/test20/Coercions.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type C, D, E _; diff --git a/Test/test20/Coercions.bpl.expect b/Test/test20/Coercions.bpl.expect new file mode 100644 index 00000000..899e0cec --- /dev/null +++ b/Test/test20/Coercions.bpl.expect @@ -0,0 +1,5 @@ +Coercions.bpl(13,8): Error: int cannot be coerced to E [a]int +Coercions.bpl(15,8): Error: C cannot be coerced to D +Coercions.bpl(17,9): Error: int cannot be coerced to D +Coercions.bpl(18,9): Error: int cannot be coerced to E int +4 type checking errors detected in Coercions.bpl diff --git a/Test/test20/EmptySeq.bpl b/Test/test20/EmptySeq.bpl index 8fecfdf4..b32ca98f 100644 --- a/Test/test20/EmptySeq.bpl +++ b/Test/test20/EmptySeq.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type Seq T; function Seq#Length(Seq T) returns (int); diff --git a/Test/test20/EmptySeq.bpl.expect b/Test/test20/EmptySeq.bpl.expect new file mode 100644 index 00000000..cc5cde4d --- /dev/null +++ b/Test/test20/EmptySeq.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test20/ParallelAssignment.bpl b/Test/test20/ParallelAssignment.bpl index 3ca196c8..b79d1a10 100644 --- a/Test/test20/ParallelAssignment.bpl +++ b/Test/test20/ParallelAssignment.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t // Examples from the Boogie2 language report // (stuff where resolution succeeds, but typechecking might fail) diff --git a/Test/test20/ParallelAssignment.bpl.expect b/Test/test20/ParallelAssignment.bpl.expect new file mode 100644 index 00000000..450616bf --- /dev/null +++ b/Test/test20/ParallelAssignment.bpl.expect @@ -0,0 +1,4 @@ +ParallelAssignment.bpl(19,2): Error: mismatched types in assignment command (cannot assign bool to int) +ParallelAssignment.bpl(20,4): Error: invalid type for argument 0 in map assignment: bool (expected: int) +ParallelAssignment.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z +3 type checking errors detected in ParallelAssignment.bpl diff --git a/Test/test20/ParallelAssignment2.bpl b/Test/test20/ParallelAssignment2.bpl index 7d1f0daf..0e36bcdd 100644 --- a/Test/test20/ParallelAssignment2.bpl +++ b/Test/test20/ParallelAssignment2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t // Examples from the Boogie2 language report // (examples where already resolution fails) diff --git a/Test/test20/ParallelAssignment2.bpl.expect b/Test/test20/ParallelAssignment2.bpl.expect new file mode 100644 index 00000000..1fa69035 --- /dev/null +++ b/Test/test20/ParallelAssignment2.bpl.expect @@ -0,0 +1,3 @@ +ParallelAssignment2.bpl(11,7): Error: number of left-hand sides does not match number of right-hand sides +ParallelAssignment2.bpl(12,9): Error: variable a is assigned more than once in parallel assignment +2 name resolution errors detected in ParallelAssignment2.bpl diff --git a/Test/test20/PolyFuns0.bpl b/Test/test20/PolyFuns0.bpl index 938bc197..0df74e15 100644 --- a/Test/test20/PolyFuns0.bpl +++ b/Test/test20/PolyFuns0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t function size(x : alpha) returns (int); diff --git a/Test/test20/PolyFuns0.bpl.expect b/Test/test20/PolyFuns0.bpl.expect new file mode 100644 index 00000000..8e03b446 --- /dev/null +++ b/Test/test20/PolyFuns0.bpl.expect @@ -0,0 +1,5 @@ +PolyFuns0.bpl(25,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a) +PolyFuns0.bpl(42,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a) +PolyFuns0.bpl(43,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a) +PolyFuns0.bpl(55,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +4 type checking errors detected in PolyFuns0.bpl diff --git a/Test/test20/PolyFuns1.bpl b/Test/test20/PolyFuns1.bpl index eaca67bf..cc38b720 100644 --- a/Test/test20/PolyFuns1.bpl +++ b/Test/test20/PolyFuns1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t function F( [b]a ) returns (bool); const M: [ [b]a ] bool; diff --git a/Test/test20/PolyFuns1.bpl.expect b/Test/test20/PolyFuns1.bpl.expect new file mode 100644 index 00000000..fcb8305e --- /dev/null +++ b/Test/test20/PolyFuns1.bpl.expect @@ -0,0 +1,17 @@ +PolyFuns1.bpl(12,9): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) +PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) +PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +PolyFuns1.bpl(19,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +PolyFuns1.bpl(20,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu:
[Field dd]dd (expected: [Field c]a) +PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: [Field cc]T (expected: [Field d]d) +PolyFuns1.bpl(32,12): Error: invalid argument types ([Field cc]T and
[Field dd]dd) to binary operator == +PolyFuns1.bpl(33,12): Error: invalid argument types (
[Field dd]dd and [Field cc]T) to binary operator == +PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: [Field T]ee (expected: [Field d]d) +PolyFuns1.bpl(43,11): Error: invalid argument types ([a,a]int and [b,int]int) to binary operator == +PolyFuns1.bpl(44,11): Error: invalid argument types ([b,int]int and [int,c]int) to binary operator == +PolyFuns1.bpl(45,11): Error: invalid argument types ([a,a]int and [int,c]int) to binary operator == +PolyFuns1.bpl(52,11): Error: invalid argument types ([a,a,b]int and [a,b,b]int) to binary operator == +PolyFuns1.bpl(59,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator == +16 type checking errors detected in PolyFuns1.bpl diff --git a/Test/test20/PolyPolyPoly.bpl b/Test/test20/PolyPolyPoly.bpl index 8666d1fc..e45a24be 100644 --- a/Test/test20/PolyPolyPoly.bpl +++ b/Test/test20/PolyPolyPoly.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type C _; diff --git a/Test/test20/PolyPolyPoly.bpl.expect b/Test/test20/PolyPolyPoly.bpl.expect new file mode 100644 index 00000000..c1f48d98 --- /dev/null +++ b/Test/test20/PolyPolyPoly.bpl.expect @@ -0,0 +1,4 @@ +PolyPolyPoly.bpl(14,26): Error: invalid argument types ([]? and []C a) to binary operator == +PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and []C a) to binary operator == +PolyPolyPoly.bpl(23,57): Error: invalid type for argument 1 in map select: b (expected: a) +3 type checking errors detected in PolyPolyPoly.bpl diff --git a/Test/test20/PolyPolyPoly2.bpl b/Test/test20/PolyPolyPoly2.bpl index b07c565a..b9249553 100644 --- a/Test/test20/PolyPolyPoly2.bpl +++ b/Test/test20/PolyPolyPoly2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t const p: []a; const q: [a]b; diff --git a/Test/test20/PolyPolyPoly2.bpl.expect b/Test/test20/PolyPolyPoly2.bpl.expect new file mode 100644 index 00000000..f36d4aaf --- /dev/null +++ b/Test/test20/PolyPolyPoly2.bpl.expect @@ -0,0 +1,12 @@ +PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(9,8): Warning: type parameter a is ambiguous, instantiating to [arg0]res +PolyPolyPoly2.bpl(13,8): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(13,15): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(13,27): Warning: type parameter a is ambiguous, instantiating to bv17 +PolyPolyPoly2.bpl(14,8): Warning: type parameter a is ambiguous, instantiating to bv17 +PolyPolyPoly2.bpl(14,15): Warning: type parameter a is ambiguous, instantiating to bv0 +PolyPolyPoly2.bpl(24,7): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int +PolyPolyPoly2.bpl(34,3): Warning: type parameter a is ambiguous, instantiating to int + +Boogie program verifier finished with 0 verified, 0 errors diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl index 06d4206c..4867614a 100644 --- a/Test/test20/PolyProcs0.bpl +++ b/Test/test20/PolyProcs0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type Field a; diff --git a/Test/test20/PolyProcs0.bpl.expect b/Test/test20/PolyProcs0.bpl.expect new file mode 100644 index 00000000..b5742f5e --- /dev/null +++ b/Test/test20/PolyProcs0.bpl.expect @@ -0,0 +1,7 @@ +PolyProcs0.bpl(13,16): Error: invalid type for argument 0 in map select: Field b (expected: ref) +PolyProcs0.bpl(13,19): Error: invalid type for argument 1 in map select: ref (expected: Field a) +PolyProcs0.bpl(23,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref) +PolyProcs0.bpl(23,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) +PolyProcs0.bpl(27,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int) +PolyProcs0.bpl(28,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b) +6 type checking errors detected in PolyProcs0.bpl diff --git a/Test/test20/ProcParamReordering.bpl b/Test/test20/ProcParamReordering.bpl index 404b41a3..f88aaea5 100644 --- a/Test/test20/ProcParamReordering.bpl +++ b/Test/test20/ProcParamReordering.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type C _; diff --git a/Test/test20/ProcParamReordering.bpl.expect b/Test/test20/ProcParamReordering.bpl.expect new file mode 100644 index 00000000..fb2a811c --- /dev/null +++ b/Test/test20/ProcParamReordering.bpl.expect @@ -0,0 +1,3 @@ +ProcParamReordering.bpl(15,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation) +ProcParamReordering.bpl(17,15): Error: mismatched number of type parameters in procedure implementation: P +2 type checking errors detected in ProcParamReordering.bpl diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl index 8fc7b7c7..2aa974c5 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t // Let's test some Boogie 2 features ... type elements; diff --git a/Test/test20/Prog0.bpl.expect b/Test/test20/Prog0.bpl.expect new file mode 100644 index 00000000..c3454422 --- /dev/null +++ b/Test/test20/Prog0.bpl.expect @@ -0,0 +1,5 @@ +Prog0.bpl(19,10): Error: type variable must occur in map arguments: a +Prog0.bpl(31,27): Error: more than one declaration of type variable: beta +Prog0.bpl(34,22): Error: undeclared type: alpha +Prog0.bpl(35,35): Error: undeclared type: alpha +4 name resolution errors detected in Prog0.bpl diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index 0e9413c1..cdc88779 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t // Let's test some Boogie 2 features ... type elements; diff --git a/Test/test20/Prog1.bpl.expect b/Test/test20/Prog1.bpl.expect new file mode 100644 index 00000000..b00ccdc1 --- /dev/null +++ b/Test/test20/Prog1.bpl.expect @@ -0,0 +1,4 @@ +Prog1.bpl(20,11): Error: invalid type for argument 0 in map select: int (expected: ref) +Prog1.bpl(21,14): Error: invalid type for argument 1 in map select: int (expected: Field a) +Prog1.bpl(22,17): Error: invalid argument types (bool and int) to binary operator >= +3 type checking errors detected in Prog1.bpl diff --git a/Test/test20/Prog2.bpl b/Test/test20/Prog2.bpl index 43b9b28f..c186eafc 100644 --- a/Test/test20/Prog2.bpl +++ b/Test/test20/Prog2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t function union( [a] bool, [a] bool) returns ( [a] bool); axiom (forall // error: alpha has to occur in dummy types diff --git a/Test/test20/Prog2.bpl.expect b/Test/test20/Prog2.bpl.expect new file mode 100644 index 00000000..82f5fcfd --- /dev/null +++ b/Test/test20/Prog2.bpl.expect @@ -0,0 +1,2 @@ +Prog2.bpl(8,14): Error: trigger does not mention alpha, which does not occur in variables types either +1 type checking errors detected in Prog2.bpl diff --git a/Test/test20/TypeDecls0.bpl b/Test/test20/TypeDecls0.bpl index 898e0d1a..cb4dc1d3 100644 --- a/Test/test20/TypeDecls0.bpl +++ b/Test/test20/TypeDecls0.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t type C a _ b; type D; type E _; diff --git a/Test/test20/TypeDecls0.bpl.expect b/Test/test20/TypeDecls0.bpl.expect new file mode 100644 index 00000000..78f3ce5c --- /dev/null +++ b/Test/test20/TypeDecls0.bpl.expect @@ -0,0 +1,13 @@ +TypeDecls0.bpl(22,5): Error: more than one declaration of type name: C +TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a +TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a +TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b +TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C +TypeDecls0.bpl(26,9): Error: undeclared type: A0 +TypeDecls0.bpl(27,9): Error: undeclared type: F +TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(40,11): Error: type constructor received wrong number of arguments: E +TypeDecls0.bpl(40,13): Error: type constructor received wrong number of arguments: E +12 name resolution errors detected in TypeDecls0.bpl diff --git a/Test/test20/TypeDecls1.bpl b/Test/test20/TypeDecls1.bpl index 02c5536a..7b64cd5b 100644 --- a/Test/test20/TypeDecls1.bpl +++ b/Test/test20/TypeDecls1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t // set of maps from anything to a specific type a const mapSet : [[b]a]bool; diff --git a/Test/test20/TypeDecls1.bpl.expect b/Test/test20/TypeDecls1.bpl.expect new file mode 100644 index 00000000..afb271eb --- /dev/null +++ b/Test/test20/TypeDecls1.bpl.expect @@ -0,0 +1,5 @@ +TypeDecls1.bpl(9,13): Error: invalid type for argument 0 in map select: int (expected: [b]a) +TypeDecls1.bpl(15,25): Error: right-hand side in map store with wrong type: int (expected: bool) +TypeDecls1.bpl(21,36): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: [[b]a]bool (expected: [b]a) +4 type checking errors detected in TypeDecls1.bpl diff --git a/Test/test20/TypeSynonyms0.bpl b/Test/test20/TypeSynonyms0.bpl index d161b5df..f43366f2 100644 --- a/Test/test20/TypeSynonyms0.bpl +++ b/Test/test20/TypeSynonyms0.bpl @@ -1,3 +1,7 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t +// RUN: %boogie -noVerify -print:- -env:0 %s > %t +// RUN: %diff %s.print.expect %t type Set a = [a]bool; diff --git a/Test/test20/TypeSynonyms0.bpl.expect b/Test/test20/TypeSynonyms0.bpl.expect new file mode 100644 index 00000000..42271d33 --- /dev/null +++ b/Test/test20/TypeSynonyms0.bpl.expect @@ -0,0 +1,7 @@ +TypeSynonyms0.bpl(13,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(14,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(16,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) +TypeSynonyms0.bpl(26,10): Error: type constructor received wrong number of arguments: Field +TypeSynonyms0.bpl(27,10): Error: type synonym received wrong number of arguments: Set +TypeSynonyms0.bpl(30,10): Error: type variable must occur in map arguments: a +6 name resolution errors detected in TypeSynonyms0.bpl diff --git a/Test/test20/TypeSynonyms0.bpl.print.expect b/Test/test20/TypeSynonyms0.bpl.print.expect new file mode 100644 index 00000000..0d2dcaf4 --- /dev/null +++ b/Test/test20/TypeSynonyms0.bpl.print.expect @@ -0,0 +1,37 @@ + +type Set a = [a]bool; + +type Field _; + +type Heap = [ref,Field a]a; + +type notAllParams a b = Field b; + +type Cyclic0 = Cyclic1; + +type Cyclic1 = Cyclic0; + +type AlsoCyclic a = [AlsoCyclic b]int; + +type C _ _; + +type C2 b a = C a b; + +function f(C int bool) : int; + +const x: C2 bool int; + +const y: Field int bool; + +const z: Set int bool; + +const d: [notAllParams a b]int; + +type ref; +(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving) +(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving) +(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving) +(24,8): Error: type constructor received wrong number of arguments: Field +(26,8): Error: type synonym received wrong number of arguments: Set +(28,8): Error: type variable must occur in map arguments: a +6 name resolution errors detected in TypeSynonyms0.bpl diff --git a/Test/test20/TypeSynonyms1.bpl b/Test/test20/TypeSynonyms1.bpl index 45b7e46d..890f494f 100644 --- a/Test/test20/TypeSynonyms1.bpl +++ b/Test/test20/TypeSynonyms1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noVerify %s > %t +// RUN: %diff %s.expect %t diff --git a/Test/test20/TypeSynonyms1.bpl.expect b/Test/test20/TypeSynonyms1.bpl.expect new file mode 100644 index 00000000..92b35ccf --- /dev/null +++ b/Test/test20/TypeSynonyms1.bpl.expect @@ -0,0 +1,2 @@ +TypeSynonyms1.bpl(48,8): Error: invalid type for argument 0 in application of h: [b,b,[b2,b,int]int]int (expected: nested2) +1 type checking errors detected in TypeSynonyms1.bpl diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl index f6fee1f3..90450c2a 100644 --- a/Test/test20/TypeSynonyms2.bpl +++ b/Test/test20/TypeSynonyms2.bpl @@ -1,3 +1,7 @@ +// RUN: %boogie %s > %t +// RUN: %diff %s.expect %t +// RUN: %boogie -noVerify -print:- -env:0 -printDesugared %s > %t +// RUN: %diff %s.print.expect %t type Set a = [a]bool; diff --git a/Test/test20/TypeSynonyms2.bpl.expect b/Test/test20/TypeSynonyms2.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test20/TypeSynonyms2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test20/TypeSynonyms2.bpl.print.expect b/Test/test20/TypeSynonyms2.bpl.print.expect new file mode 100644 index 00000000..72b889d9 --- /dev/null +++ b/Test/test20/TypeSynonyms2.bpl.print.expect @@ -0,0 +1,52 @@ + +type Set a = [a]bool; + +function union(x: Set a, y: Set a) : Set a; + +axiom (forall x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]); + +const intSet0: Set int; + +axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); + +const intSet1: Set int; + +axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3)); + +procedure P(); + + + +implementation P() +{ + assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3)); +} + + + +type Set a = [a]bool; + +function union(x: Set a, y: Set a) : Set a; + +axiom (forall x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]); + +const intSet0: Set int; + +axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); + +const intSet1: Set int; + +axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3); + +procedure P(); + + + +implementation P() +{ + assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3); +} + + + +Boogie program verifier finished with 0 verified, 0 errors -- cgit v1.2.3
[Field dd]dd and [Field cc]T) to binary operator == -PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: [Field T]ee (expected: [Field d]d) -PolyFuns1.bpl(41,11): Error: invalid argument types ([a,a]int and [b,int]int) to binary operator == -PolyFuns1.bpl(42,11): Error: invalid argument types ([b,int]int and [int,c]int) to binary operator == -PolyFuns1.bpl(43,11): Error: invalid argument types ([a,a]int and [int,c]int) to binary operator == -PolyFuns1.bpl(50,11): Error: invalid argument types ([a,a,b]int and [a,b,b]int) to binary operator == -PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator == +PolyFuns1.bpl(12,9): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) +PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: [c]c (expected: [b]a) +PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: [c]c (expected: [b]a) +PolyFuns1.bpl(19,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +PolyFuns1.bpl(20,55): Error: invalid argument types ([Field c]a and [Field d]d) to binary operator == +PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu: