From 115b3d54e06527160ad895274982d2a955160132 Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Fri, 21 Jan 2011 04:53:34 +0000
Subject: Put back the prelude for the split fields heap that had been there
 before.

---
 BCT/BytecodeTranslator/Heap.cs | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

(limited to 'BCT/BytecodeTranslator')

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 087f4c69..0ff10c0b 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -65,9 +65,7 @@ procedure {:inline 1} Alloc() returns (x: int)
       heap = this;
       program = null;
       var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
-      if (!b) return false;
-      heap = this;
-      return true;
+      return b;
     }
 
     /// <summary>
@@ -130,10 +128,32 @@ procedure {:inline 1} Alloc() returns (x: int)
   /// </summary>
   public class SplitFieldsHeap : HeapFactory {
 
+    /// <summary>
+    /// Prelude text for which access to the ASTs is not needed
+    /// </summary>
+    private readonly string InitialPreludeText =
+      @"const null: int;
+type HeapType = [int,int]int;
+var $Heap: HeapType where IsGoodHeap($Heap);
+function IsGoodHeap(HeapType): bool;
+var $ArrayContents: [int][int]int;
+var $ArrayLength: [int]int;
+
+var $Alloc: [int] bool;
+procedure {:inline 1} Alloc() returns (x: int)
+  free ensures x != 0;
+  modifies $Alloc;
+{
+  assume $Alloc[x] == false;
+  $Alloc[x] := true;
+}
+";
+
     public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
       heap = new HeapRepresentation(sink);
       program = null;
-      return true;
+      var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+      return b;
     }
 
     private class HeapRepresentation : IHeap {
-- 
cgit v1.2.3