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/dafny0/DisplayExpressions.dfy | |
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/dafny0/DisplayExpressions.dfy')
-rw-r--r-- | Test/dafny0/DisplayExpressions.dfy | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/Test/dafny0/DisplayExpressions.dfy b/Test/dafny0/DisplayExpressions.dfy index 767cfcdb..ef7d4062 100644 --- a/Test/dafny0/DisplayExpressions.dfy +++ b/Test/dafny0/DisplayExpressions.dfy @@ -2,20 +2,25 @@ // RUN: %diff "%s.expect" "%t"
method M()
{
- var m := map[];
+ var m := map[]; // error: underspecified type
}
method N()
{
- var n := multiset{};
+ var n := multiset{}; // error: underspecified type
}
method O()
{
- var o := [];
+ var o := []; // error: underspecified type
}
method P()
{
- var p := {};
+ var p := {}; // error: underspecified type
+}
+
+method Q()
+{
+ assert (((map[]))) == (((((map[]))))); // error (but not 10 errors)
}
|