From 909884fcf5c2ec6af2e68ceae36d72401d542cb3 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 8 Oct 2014 15:47:13 -0700 Subject: Stricter rules about that types need to be completely resolved. Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it). If the type of literal "null" is unresolved, make the type "object". The need to translate unresolved proxies is now assumed to be gone. --- Test/hofs/Underspecified.dfy.expect | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Test/hofs') diff --git a/Test/hofs/Underspecified.dfy.expect b/Test/hofs/Underspecified.dfy.expect index 04394d78..a5970830 100644 --- a/Test/hofs/Underspecified.dfy.expect +++ b/Test/hofs/Underspecified.dfy.expect @@ -1,5 +1,8 @@ +Underspecified.dfy(6,6): Error: the type of this variable is underspecified Underspecified.dfy(6,11): Error: type of bound variable '_v0' could not be determined; please specify the type explicitly +Underspecified.dfy(7,6): Error: the type of this variable is underspecified Underspecified.dfy(7,12): Error: type of bound variable '_v1' could not be determined; please specify the type explicitly Underspecified.dfy(7,15): Error: type of bound variable '_v2' could not be determined; please specify the type explicitly +Underspecified.dfy(8,6): Error: the type of this variable is underspecified Underspecified.dfy(8,11): Error: type of bound variable 'a' could not be determined; please specify the type explicitly -4 resolution/type errors detected in Underspecified.dfy +7 resolution/type errors detected in Underspecified.dfy -- cgit v1.2.3