diff options
Diffstat (limited to 'Test/dafny0/TypeTests.dfy.expect')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 500b1af9..de0bfbed 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,6 +1,10 @@ -TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -8,7 +12,6 @@ TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, go TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
@@ -56,8 +59,5 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts
-TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
62 resolution/type errors detected in TypeTests.dfy
|