diff options
| author |  mikebarnett <unknown> | 2011-01-21 04:53:34 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-01-21 04:53:34 +0000 |
| commit | 115b3d54e06527160ad895274982d2a955160132 (patch) | |
| tree | 403f035ac098fe00dca2f363ab15f915db916b13 /BCT/RegressionTests | |
| parent | afb451a67a6a8f9cb8f412421ce294058b1ffdb2 (diff) | |
Put back the prelude for the split fields heap that had been there before.
Diffstat (limited to 'BCT/RegressionTests')
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index aa1f71e0..307d0eb5 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -1,6 +1,34 @@ // Copyright (c) 2010, Microsoft Corp.
// Bytecode Translator prelude
+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);
+ modifies $Alloc;
+ free ensures x != 0;
+
+
+
+implementation Alloc() returns (x: int)
+{
+ assume $Alloc[x] == false;
+ $Alloc[x] := true;
+}
+
+
+
procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);
|