diff options
| author |  Rustan Leino <unknown> | 2014-03-20 15:01:57 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-03-20 15:01:57 -0700 |
| commit | 912adaa06621d89a47460d6a6befd8809ded5c85 (patch) | |
| tree | 1016a8998a8fd80042aaf36997e98bbfb5f9c236 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 73d20fd1f40d380f10a4a62cb8853137e340514a (diff) | |
Fixed problem with propagating allocation information about array elements.
Improved situation with (reducing bogosity of) type checking of "object".
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 40963e36..f7a7ed3e 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -804,3 +804,25 @@ module GhostLetExpr { G(5, xyz)
}
}
+
+module ObjectType {
+ type B
+ datatype Dt = Blue | Green
+ codatatype CoDt = Cons(int, CoDt)
+ class MyClass { }
+
+ method M<G>(zz: array<B>, j: int, b: B, co: CoDt, g: G) returns (o: object)
+ requires zz != null && 0 <= j < zz.Length;
+ {
+ o := b; // error
+ o := 17; // error
+ o := zz[j]; // error
+ o := null;
+ o := zz;
+ o := new MyClass;
+ o := o;
+ o := g; // error
+ o := Blue; // error
+ o := co; // error
+ }
+}
|