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/hofs | |
| parent | d5685d5afcd053a0bb2178425e1b1d12cd85eb52 (diff) | |
Snapshot, to be continued
Diffstat (limited to 'Test/hofs')
| -rw-r--r-- | Test/hofs/Field.dfy.expect | 8 | ||||
| -rw-r--r-- | Test/hofs/ResolveError.dfy.expect | 10 |
2 files changed, 9 insertions, 9 deletions
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect index 927d8b06..9f6998f5 100644 --- a/Test/hofs/Field.dfy.expect +++ b/Test/hofs/Field.dfy.expect @@ -1,14 +1,14 @@ -Field.dfy(12,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
Field.dfy(12,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,10): Error: assertion violation
+Field.dfy(12,15): Error: assertion violation
Execution trace:
(0,0): anon0
Field.dfy(21,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
+Field.dfy(21,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
Dafny program verifier finished with 2 verified, 4 errors
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect index 2cf19369..c3e0c242 100644 --- a/Test/hofs/ResolveError.dfy.expect +++ b/Test/hofs/ResolveError.dfy.expect @@ -1,5 +1,5 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable to LHS (of type (int,bool) -> real)
-ResolveError.dfy(91,14): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
+ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)
ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)
ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)
ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment
@@ -8,12 +8,12 @@ ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)
ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)
ResolveError.dfy(33,13): Error: type mismatch for argument 0 (function expects int, got bool)
-ResolveError.dfy(34,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(34,22): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(35,25): Error: arguments must have the same type (got bool and int)
-ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expected 1)
-ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected int, got bool)
+ResolveError.dfy(36,21): Error: wrong number of arguments to function application (function 'requires' expects 1, got 2)
+ResolveError.dfy(37,19): Error: type mismatch for argument 0 (function expects int, got bool)
ResolveError.dfy(38,22): Error: arguments must have the same type (got set<object> and int)
-ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expected 1)
+ResolveError.dfy(39,18): Error: wrong number of arguments to function application (function 'reads' expects 1, got 2)
ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)
ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)
ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool
|