Enabled tests for types introduced in Boogie2 as lit tests.

39 files changed, 310 insertions, 79 deletions

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>[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]c (expected: <b>[b]a)

-TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)

+TypeDecls1.bpl(9,13): Error: invalid type for argument 0 in map select: int (expected: <b>[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]c (expected: <b>[b]a)

+TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[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 (<c>[Field c]a and <d>[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 (<c>[Field c]a and <d>[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]c (expected: <b>[b]a)

-PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

-PolyFuns1.bpl(17,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

-PolyFuns1.bpl(18,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

-PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)

-PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)

-PolyFuns1.bpl(30,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==

-PolyFuns1.bpl(31,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==

-PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)

-PolyFuns1.bpl(41,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==

-PolyFuns1.bpl(42,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==

-PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==

-PolyFuns1.bpl(50,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[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]c (expected: <b>[b]a)

+PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

+PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)

+PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)

+PolyFuns1.bpl(19,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

+PolyFuns1.bpl(20,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==

+PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)

+PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)

+PolyFuns1.bpl(32,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==

+PolyFuns1.bpl(33,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==

+PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)

+PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==

+PolyFuns1.bpl(44,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==

+PolyFuns1.bpl(45,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==

+PolyFuns1.bpl(52,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[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,b,<b2>[b2,b,int]int]int (expected: nested2)

+TypeSynonyms1.bpl(48,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[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 <a>[]C a) to binary operator ==

-PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and <a>[]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 <a>[]C a) to binary operator ==

+PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and <a>[]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>[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>[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>[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>[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>[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<T>(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<alpha>(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 (<c>[Field c]a and <d>[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<a>( <b>[b]a ) returns (bool);

 const M:  <a>[ <b>[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]c (expected: <b>[b]a)
+PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(19,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(20,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)
+PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)
+PolyFuns1.bpl(32,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==
+PolyFuns1.bpl(33,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==
+PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)
+PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==
+PolyFuns1.bpl(44,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(45,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(52,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[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 <a>[]C a) to binary operator ==
+PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and <a>[]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>[]a;

 const q: <a,b>[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>[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> [a] bool, <a> [a] bool) returns (<a> [a] bool);

 

 axiom (forall<alpha>             // 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 : <a>[<b>[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>[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]c (expected: <b>[b]a)
+TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[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 = <a>[ref,Field a]a;
+
+type notAllParams a b = Field b;
+
+type Cyclic0 = Cyclic1;
+
+type Cyclic1 = Cyclic0;
+
+type AlsoCyclic a = <b>[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: <a,b>[notAllParams a b]int;
+
+type ref;
+<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
+<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
+<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
+<console>(24,8): Error: type constructor received wrong number of arguments: Field
+<console>(26,8): Error: type synonym received wrong number of arguments: Set
+<console>(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,b,<b2>[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<a>(x: Set a, y: Set a) : Set a;
+
+axiom (forall<a> 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<a>(x: Set a, y: Set a) : Set a;
+
+axiom (forall<a> 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