diff options
Diffstat (limited to 'BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt')
| -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);
|