diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index db08a280..6508df2d 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -555,6 +555,14 @@ const $FunctionContextHeight: int; const $InMethodContext: bool;
// ---------------------------------------------------------------
+// -- Layers of function encodings -------------------------------
+// ---------------------------------------------------------------
+
+type LayerType;
+const $LZ: LayerType;
+function $LS(LayerType): LayerType;
+
+// ---------------------------------------------------------------
// -- Fields -----------------------------------------------------
// ---------------------------------------------------------------
@@ -686,6 +694,13 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSuccGhost(h,k) } !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
// ---------------------------------------------------------------
+// -- Non-determinism --------------------------------------------
+// ---------------------------------------------------------------
+
+type TickType;
+var $Tick: TickType;
+
+// ---------------------------------------------------------------
// -- Useful macros ----------------------------------------------
// ---------------------------------------------------------------
@@ -723,10 +738,3 @@ procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: re ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
// ---------------------------------------------------------------
-// -- Non-determinism --------------------------------------------
-// ---------------------------------------------------------------
-
-type TickType;
-var $Tick: TickType;
-
-// ---------------------------------------------------------------
|