diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-14 17:43:34 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-14 17:43:34 -0700 |
| commit | 0999203f82d0ff7d0a1f3e981adaa4225b26022d (patch) | |
| tree | 9b29c39bd692d8010c5ef7e38a21dc3f8cfc02a2 | |
| parent | 4ab6c9f4cfa6295369fde54084f3e1f4ed70d5e4 (diff) | |
Reword error message for type error in lambda requires clause
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/hofs/ResolveError.dfy | 7 | ||||
| -rw-r--r-- | Test/hofs/ResolveError.dfy.expect | 6 |
3 files changed, 12 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 35086275..7c2c5759 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6983,7 +6983,7 @@ namespace Microsoft.Dafny ResolveExpression(e.Range, twoState, codeContext);
Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.Range.Type, Type.Bool)) {
- Error(expr, "requires clause for lambda must be bool (instead got {0})", e.Range.Type);
+ Error(expr, "Precondition must be boolean (got {0})", e.Range.Type);
}
}
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy index fa5ffb0c..1e389f04 100644 --- a/Test/hofs/ResolveError.dfy +++ b/Test/hofs/ResolveError.dfy @@ -40,6 +40,13 @@ method RequiresFail(f : int -> int) { } +method Bogus() +{ + var f; + f := x reads 1 => x; + f := x requires 1 => x; +} + predicate method Bool() { true diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect index acc01b73..a95d9bac 100644 --- a/Test/hofs/ResolveError.dfy.expect +++ b/Test/hofs/ResolveError.dfy.expect @@ -10,5 +10,7 @@ ResolveError.dfy(36,13): Error: wrong number of function arguments (got 2, expec ResolveError.dfy(37,13): Error: incorrect type of function argument 0 (expected 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(49,9): Error: condition is expected to be of type bool, but is () -> bool
-13 resolution/type errors detected in ResolveError.dfy
+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
+15 resolution/type errors detected in ResolveError.dfy
|