summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Dan Rosén <danr@chalmers.se>2014-08-14 17:45:39 -0700
committerGravatar Dan Rosén <danr@chalmers.se>2014-08-14 17:45:39 -0700
commitf6f433a22fe5149eb1726c98cb0b3bfed7e9ffce (patch)
tree3fc1e358809eb157d6ec3f6039f6781261cd24ff /Test
parent777457959bc063f89e19715d202d71b78576e477 (diff)
Make arrow types not look like reference types for the resolver
Diffstat (limited to 'Test')
-rw-r--r--Test/hofs/ResolveError.dfy5
-rw-r--r--Test/hofs/ResolveError.dfy.expect4
2 files changed, 8 insertions, 1 deletions
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 1e389f04..31de9424 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -56,3 +56,8 @@ method Bla() {
assert Bool;
}
+method Pli(f : A -> B) requires f != null;
+{
+ var o : object;
+ assert f != o;
+}
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index a95d9bac..d7de049a 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -13,4 +13,6 @@ ResolveError.dfy(39,13): Error: wrong number of function arguments (got 2, expec
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
+ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)
+ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)
+17 resolution/type errors detected in ResolveError.dfy