diff options
| author |  leino <unknown> | 2014-12-02 14:04:53 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-12-02 14:04:53 -0800 |
| commit | 682a34e72274aff3ef4ebcbe54244d1c2ca0ba2f (patch) | |
| tree | 448289d84b91a081f7658710f0fcb9cc425805c8 /Test/dafny0/TypeTests.dfy.expect | |
| parent | d5685d5afcd053a0bb2178425e1b1d12cd85eb52 (diff) | |
Snapshot, to be continued
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 55fc916c..0a15ad67 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -1,13 +1,13 @@ TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)
-TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)
-TypeTests.dfy(8,13): Error: incorrect type of function argument 1 (expected D, got int)
-TypeTests.dfy(14,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
-TypeTests.dfy(15,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
+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)
+TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, got int)
+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
|