diff options
| author |  leino <unknown> | 2014-10-08 15:47:13 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-08 15:47:13 -0700 |
| commit | 909884fcf5c2ec6af2e68ceae36d72401d542cb3 (patch) | |
| tree | 219a88e5417fdcc7d999a34e005e26eb735061f1 /Test/hofs | |
| parent | 8dcec3ddb5269c5e7195a8072d13e8e547b14323 (diff) | |
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.
Diffstat (limited to 'Test/hofs')
| -rw-r--r-- | Test/hofs/Underspecified.dfy.expect | 5 |
1 files changed, 4 insertions, 1 deletions
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
|