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 | |
| parent | 73d20fd1f40d380f10a4a62cb8853137e340514a (diff) | |
Fixed problem with propagating allocation information about array elements.
Improved situation with (reducing bogosity of) type checking of "object".
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 12 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/Array.dfy | 21 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 22 |
4 files changed, 56 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ffc6715b..b6fce82c 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -662,6 +662,18 @@ axiom (forall r: ref, f: Field BoxType, h: HeapType :: $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
GenericAlloc(read(h, r, f), h));
+axiom (forall h: HeapType, r: ref, j: int ::
+ { read(h, r, IndexField(j)) }
+ $IsGoodHeap(h) && r != null && read(h, r, alloc)
+ ==>
+ GenericAlloc(read(h, r, IndexField(j)), h));
+axiom (forall h: HeapType, r: ref, m: Field BoxType, j: int ::
+ { read(h, r, MultiIndexField(m, j)) }
+ $IsGoodHeap(h) && r != null && read(h, r, alloc)
+ ==>
+ GenericAlloc(read(h, r, MultiIndexField(m, j)), h));
+
+
// ---------------------------------------------------------------
// -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0904e544..a409f39e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3670,7 +3670,7 @@ namespace Microsoft.Dafny #if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
var other = a is ObjectType ? b : a;
- if (other is BoolType || other is IntType || other is RealType || other is SetType || other is SeqType || other.IsDatatype) {
+ if (!other.IsRefType) {
return false;
}
// allow anything else with object; this is BOGUS
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index d8bffce4..4cd06e53 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -253,3 +253,24 @@ method Test_ArrayElementLhsOfCall(a: array<int>, i: int, c: Cdefg<int>) returns class Cdefg<T> {
var t: T;
}
+
+// ---------- allocation business -----------
+
+class MyClass {
+ ghost var Repr: set<object>;
+}
+
+method AllocationBusinessA(a: array<MyClass>, j: int)
+ requires a != null && 0 <= j < a.Length;
+ requires a[j] != null;
+{
+ var c := new MyClass;
+ assert c !in a[j].Repr; // the proof requires allocation axioms for arrays
+}
+method AllocationBusinessB(a: array2<MyClass>, i: int, j: int)
+ requires a != null && 0 <= i < a.Length0 && 0 <= j < a.Length1;
+ requires a[i,j] != null;
+{
+ var c := new MyClass;
+ assert c !in a[i,j].Repr; // the proof requires allocation axioms for multi-dim arrays
+}
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
+ }
+}
|