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 /Binaries | |
| 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 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 12 |
1 files changed, 12 insertions, 0 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 -----------------------------------------------------
// ---------------------------------------------------------------
|