From 0999203f82d0ff7d0a1f3e981adaa4225b26022d Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Thu, 14 Aug 2014 17:43:34 -0700 Subject: Reword error message for type error in lambda requires clause --- Test/hofs/ResolveError.dfy | 7 +++++++ Test/hofs/ResolveError.dfy.expect | 6 ++++-- 2 files changed, 11 insertions(+), 2 deletions(-) (limited to 'Test/hofs') 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 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 -- cgit v1.2.3