From 1c20ac79616789d3b28f2dcb7557c38d075e7eb8 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 6 Mar 2013 22:18:58 -0800
Subject: Disallow allocations in ghost contexts

---
 Binaries/DafnyPrelude.bpl | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 7b932078..561a29a1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -520,12 +520,14 @@ axiom (forall<T> cl : ClassName, nm: NameFamily ::
    {FieldOfDecl(cl, nm): Field T}
    DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
 
+function $IsGhostField<T>(Field T): bool;
+
 // ---------------------------------------------------------------
 // -- Allocatedness ----------------------------------------------
 // ---------------------------------------------------------------
 
 const unique alloc: Field bool;
-axiom FDim(alloc) == 0;
+axiom FDim(alloc) == 0 && !$IsGhostField(alloc);  // treat as non-ghost field, because it cannot be changed by ghost code
 
 function DtAlloc(DatatypeType, HeapType): bool;
 axiom (forall h, k: HeapType, d: DatatypeType ::
@@ -611,6 +613,13 @@ axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
 axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
   $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
 
+function $HeapSuccGhost(HeapType, HeapType): bool;
+axiom (forall h: HeapType, k: HeapType :: { $HeapSuccGhost(h,k) }
+  $HeapSuccGhost(h,k) ==>
+    $HeapSucc(h,k) &&
+    (forall<alpha> o: ref, f: Field alpha :: { read(k, o, f) }
+      !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
+
 // ---------------------------------------------------------------
 // -- Useful macros ----------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3