diff options
| author |  leino <unknown> | 2015-09-28 13:16:15 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
| commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
| tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Test/dafny0/TypeTests.dfy.expect | |
| parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) | |
Changed computation of ghosts until pass 2 of resolution.
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
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 8206fd43..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,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-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
|