diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -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 -----------------------------------------------------
// ---------------------------------------------------------------
|