Moved the parts of the Prelude that depend on the heap representation into the appropriate Heap objects.

Also added the ability to easily have access to the ASTs that result from the specific heap representation's declarations.

1 files changed, 18 insertions, 7 deletions

diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
index fdb08f32..0b5a0c2d 100644
--- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
+++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
@@ -2,22 +2,33 @@
 // Bytecode Translator prelude

 

 const null: int;

+

 type HeapType = [int,int]int;

-function IsGoodHeap(HeapType): bool;

-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;

+var $Alloc: [int]bool;

+

+procedure {:inline 1} Alloc() returns (x: int);

   modifies $Alloc;

+  free ensures x != 0;

+

+

+

+implementation Alloc() returns (x: int)

 {

-  assume $Alloc[x] == false;

-  $Alloc[x] := true;

+    assume $Alloc[x] == false;

+    $Alloc[x] := true;

 }

 

+

+

+var $Heap: HeapType where IsGoodHeap($Heap);

+

 procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);