0. Deleted other heap representations except SplitField and General

1. first cut at implementing structs

6 files changed, 8 insertions, 1488 deletions

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 703c908f..87514ae9 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -3,8 +3,6 @@
 

 const null: ref;

 

-type box;

-

 type ref = int;

 

 type HeapType = [ref,Field]box;

@@ -188,8 +186,6 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
 

 

 

-type Field;

-

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

 

 function Box2Int(box) : int;

@@ -210,6 +206,10 @@ function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType
   H[o, f := v]

 }

 

+type Field;

+

+type box;

+

 type Type;

 

 function $DynamicType(ref) : Type;

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 5245bf3d..e6d6e7fd 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -188,6 +188,10 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
 

 

 

+type Field;

+

+type box;

+

 type Type;

 

 function $DynamicType(ref) : Type;

diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
index cef103b7..b0dd1907 100644
--- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
+++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
@@ -102,15 +102,9 @@
     </ProjectReference>

   </ItemGroup>

   <ItemGroup>

-    <EmbeddedResource Include="TwoDIntHeapInput.txt" />

-  </ItemGroup>

-  <ItemGroup>

     <EmbeddedResource Include="SplitFieldsHeapInput.txt" />

   </ItemGroup>

   <ItemGroup>

-    <EmbeddedResource Include="TwoDBoxHeapInput.txt" />

-  </ItemGroup>

-  <ItemGroup>

     <EmbeddedResource Include="GeneralHeapInput.txt" />

   </ItemGroup>

   <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
deleted file mode 100644
index c23df829..00000000
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ /dev/null
@@ -1,729 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.

-// Bytecode Translator prelude

-

-const null: int;

-

-type box;

-

-type HeapType = [int,int]box;

-

-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 DelegateAdd(a: int, b: int) returns (c: int);

-

-

-

-implementation DelegateAdd(a: int, b: int) returns (c: int)

-{

-  var m: int;

-  var o: int;

-

-    if (a == 0)

-    {

-        c := b;

-        return;

-    }

-    else if (b == 0)

-    {

-        c := a;

-        return;

-    }

-

-    call m, o := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Method[c] := $Method[a];

-    $Receiver[c] := $Receiver[a];

-    call c := DelegateAddHelper(c, m, o);

-}

-

-

-

-procedure DelegateRemove(a: int, b: int) returns (c: int);

-

-

-

-implementation DelegateRemove(a: int, b: int) returns (c: int)

-{

-  var m: int;

-  var o: int;

-

-    if (a == 0)

-    {

-        c := 0;

-        return;

-    }

-    else if (b == 0)

-    {

-        c := a;

-        return;

-    }

-

-    call m, o := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Method[c] := $Method[a];

-    $Receiver[c] := $Receiver[a];

-    call c := DelegateRemoveHelper(c, m, o);

-}

-

-

-

-procedure GetFirstElement(i: int) returns (m: int, o: int);

-

-

-

-implementation GetFirstElement(i: int) returns (m: int, o: int)

-{

-  var first: int;

-

-    first := $Next[i][$Head[i]];

-    m := $Method[i][first];

-    o := $Receiver[i][first];

-}

-

-

-

-procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int);

-

-

-

-implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)

-{

-  var x: int;

-  var h: int;

-

-    if (oldi == 0)

-    {

-        call i := Alloc();

-        call x := Alloc();

-        $Head[i] := x;

-        $Next[i] := $Next[i][x := x];

-    }

-    else

-    {

-        i := oldi;

-    }

-

-    h := $Head[i];

-    $Method[i] := $Method[i][h := m];

-    $Receiver[i] := $Receiver[i][h := o];

-    call x := Alloc();

-    $Next[i] := $Next[i][x := $Next[i][h]];

-    $Next[i] := $Next[i][h := x];

-    $Head[i] := x;

-}

-

-

-

-procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int);

-

-

-

-implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)

-{

-  var prev: int;

-  var iter: int;

-  var niter: int;

-

-    i := oldi;

-    if (i == 0)

-    {

-        return;

-    }

-

-    prev := 0;

-    iter := $Head[i];

-    while (true)

-    {

-        niter := $Next[i][iter];

-        if (niter == $Head[i])

-        {

-            break;

-        }

-

-        if ($Method[i][niter] == m && $Receiver[i][niter] == o)

-        {

-            prev := iter;

-        }

-

-        iter := niter;

-    }

-

-    if (prev == 0)

-    {

-        return;

-    }

-

-    $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

-    if ($Next[i][$Head[i]] == $Head[i])

-    {

-        i := 0;

-    }

-}

-

-

-

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

-

-function Box2Int(box) : int;

-

-function Box2Bool(box) : bool;

-

-function Int2Box(int) : box;

-

-function Bool2Box(bool) : box;

-

-type Type;

-

-function $DynamicType(ref) : Type;

-

-function $TypeOf(Type) : ref;

-

-var $Head: [int]int;

-

-var $Next: [int][int]int;

-

-var $Method: [int][int]int;

-

-var $Receiver: [int][int]int;

-

-const unique RegressionTestInput.ClassWithArrayTypes: Type;

-

-var RegressionTestInput.ClassWithArrayTypes.s: int;

-

-const unique RegressionTestInput.ClassWithArrayTypes.a: int;

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main1();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main1()

-{

-  var local_0: int;

-  var $tmp0: int;

-  var local_1: int;

-  var $tmp1: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;

-    call $tmp0 := Alloc();

-    local_0 := $tmp0;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

-    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;

-    assert $ArrayContents[local_0][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;

-    call $tmp1 := Alloc();

-    local_1 := $tmp1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;

-    $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;

-    assert $ArrayContents[local_1][0] == 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;

-    assert $ArrayContents[local_0][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main2();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main2()

-{

-  var $tmp2: int;

-  var local_0: int;

-  var $tmp3: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;

-    call $tmp2 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;

-    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;

-    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;

-    call $tmp3 := Alloc();

-    local_0 := $tmp3;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;

-    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;

-    assert $ArrayContents[local_0][0] == 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;

-    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;

-    $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x := 42]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;

-    $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1 := 43]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;

-    assert $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1] == $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x] + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)

-{

-  var xs: int;

-

-    xs := xs$in;

-    if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true))

-    {

-        assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;

-        $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][0 := $ArrayContents[xs][0]]];

-    }

-    else

-    {

-    }

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);

-

-

-

-procedure System.Object.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)

-{

-    $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0);

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.#cctor();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()

-{

-    RegressionTestInput.ClassWithArrayTypes.s := 0;

-}

-

-

-

-const unique RegressionTestInput.Class0: Type;

-

-var RegressionTestInput.Class0.StaticInt: int;

-

-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;

-    $result := x + 1;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)

-{

-  var x: int;

-  var __temp_1: int;

-  var $tmp4: int;

-  var local_0: int;

-

-    x := x$in;

-    $tmp4 := x;

-    assert $tmp4 != 0;

-    __temp_1 := 5 / $tmp4;

-    x := 3;

-    local_0 := __temp_1 + 3;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;

-    assert (if x == 3 then local_0 <= 8 else false);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;

-    RegressionTestInput.Class0.StaticInt := local_0;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;

-    assert local_0 == RegressionTestInput.Class0.StaticInt;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)

-{

-  var x: int;

-  var y: int;

-

-    x := x$in;

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)

-{

-  var b: bool;

-

-    b := b$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)

-{

-  var c: int;

-

-    c := c$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)

-{

-  var $tmp5: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;

-    call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

-    $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

-

-

-

-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

-{

-    assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;

-    x$out := 3 + RegressionTestInput.Class0.StaticInt;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;

-    $result := x$out;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

-

-

-

-implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

-{

-    x$out := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;

-    x$out := x$out + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;

-    RegressionTestInput.Class0.StaticInt := x$out;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;

-    $result := x$out;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;

-    x := x + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;

-    RegressionTestInput.Class0.StaticInt := x;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;

-    $result := x;

-    return;

-}

-

-

-

-procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;

-    $result := x;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

-{

-  var y: int;

-  var $tmp6: int;

-

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;

-    call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);

-    $result := $tmp6;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.Class0.#ctor(this: int)

-{

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.#cctor();

-

-

-

-implementation RegressionTestInput.Class0.#cctor()

-{

-    RegressionTestInput.Class0.StaticInt := 0;

-}

-

-

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)

-{

-    assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));

-    assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)

-{

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()

-{

-}

-

-

-

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

-

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

-

-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;

-

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

-{

-  var x: int;

-  var y: int;

-

-    x := x$in;

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;

-    $result := x < y;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)

-{

-  var z: bool;

-

-    z := z$in;

-    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

-    call System.Object.#ctor(this);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

-    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

-    if (z)

-    {

-        assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

-        RegressionTestInput.ClassWithBoolTypes.staticB := z;

-    }

-    else

-    {

-    }

-

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.Main();

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.Main()

-{

-  var $tmp7: bool;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;

-    call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()

-{

-    RegressionTestInput.ClassWithBoolTypes.staticB := false;

-}

-

-

-

-const unique RegressionTestInput.AsyncAttribute: Type;

-

-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);

-

-

-

-procedure System.Attribute.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)

-{

-    call System.Attribute.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.AsyncAttribute.#cctor();

-

-

-

-implementation RegressionTestInput.AsyncAttribute.#cctor()

-{

-}

-

-

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
deleted file mode 100644
index 262958c0..00000000
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ /dev/null
@@ -1,719 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.

-// Bytecode Translator prelude

-

-const null: int;

-

-type HeapType = [int,int]int;

-

-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 DelegateAdd(a: int, b: int) returns (c: int);

-

-

-

-implementation DelegateAdd(a: int, b: int) returns (c: int)

-{

-  var m: int;

-  var o: int;

-

-    if (a == 0)

-    {

-        c := b;

-        return;

-    }

-    else if (b == 0)

-    {

-        c := a;

-        return;

-    }

-

-    call m, o := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Method[c] := $Method[a];

-    $Receiver[c] := $Receiver[a];

-    call c := DelegateAddHelper(c, m, o);

-}

-

-

-

-procedure DelegateRemove(a: int, b: int) returns (c: int);

-

-

-

-implementation DelegateRemove(a: int, b: int) returns (c: int)

-{

-  var m: int;

-  var o: int;

-

-    if (a == 0)

-    {

-        c := 0;

-        return;

-    }

-    else if (b == 0)

-    {

-        c := a;

-        return;

-    }

-

-    call m, o := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Method[c] := $Method[a];

-    $Receiver[c] := $Receiver[a];

-    call c := DelegateRemoveHelper(c, m, o);

-}

-

-

-

-procedure GetFirstElement(i: int) returns (m: int, o: int);

-

-

-

-implementation GetFirstElement(i: int) returns (m: int, o: int)

-{

-  var first: int;

-

-    first := $Next[i][$Head[i]];

-    m := $Method[i][first];

-    o := $Receiver[i][first];

-}

-

-

-

-procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int);

-

-

-

-implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)

-{

-  var x: int;

-  var h: int;

-

-    if (oldi == 0)

-    {

-        call i := Alloc();

-        call x := Alloc();

-        $Head[i] := x;

-        $Next[i] := $Next[i][x := x];

-    }

-    else

-    {

-        i := oldi;

-    }

-

-    h := $Head[i];

-    $Method[i] := $Method[i][h := m];

-    $Receiver[i] := $Receiver[i][h := o];

-    call x := Alloc();

-    $Next[i] := $Next[i][x := $Next[i][h]];

-    $Next[i] := $Next[i][h := x];

-    $Head[i] := x;

-}

-

-

-

-procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int);

-

-

-

-implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)

-{

-  var prev: int;

-  var iter: int;

-  var niter: int;

-

-    i := oldi;

-    if (i == 0)

-    {

-        return;

-    }

-

-    prev := 0;

-    iter := $Head[i];

-    while (true)

-    {

-        niter := $Next[i][iter];

-        if (niter == $Head[i])

-        {

-            break;

-        }

-

-        if ($Method[i][niter] == m && $Receiver[i][niter] == o)

-        {

-            prev := iter;

-        }

-

-        iter := niter;

-    }

-

-    if (prev == 0)

-    {

-        return;

-    }

-

-    $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

-    if ($Next[i][$Head[i]] == $Head[i])

-    {

-        i := 0;

-    }

-}

-

-

-

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

-

-type Type;

-

-function $DynamicType(ref) : Type;

-

-function $TypeOf(Type) : ref;

-

-var $Head: [int]int;

-

-var $Next: [int][int]int;

-

-var $Method: [int][int]int;

-

-var $Receiver: [int][int]int;

-

-const unique RegressionTestInput.ClassWithArrayTypes: Type;

-

-var RegressionTestInput.ClassWithArrayTypes.s: int;

-

-const unique RegressionTestInput.ClassWithArrayTypes.a: int;

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main1();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main1()

-{

-  var local_0: int;

-  var $tmp0: int;

-  var local_1: int;

-  var $tmp1: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;

-    call $tmp0 := Alloc();

-    local_0 := $tmp0;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

-    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;

-    assert $ArrayContents[local_0][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;

-    call $tmp1 := Alloc();

-    local_1 := $tmp1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;

-    $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;

-    assert $ArrayContents[local_1][0] == 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;

-    assert $ArrayContents[local_0][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main2();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main2()

-{

-  var $tmp2: int;

-  var local_0: int;

-  var $tmp3: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;

-    call $tmp2 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;

-    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;

-    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;

-    call $tmp3 := Alloc();

-    local_0 := $tmp3;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;

-    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;

-    assert $ArrayContents[local_0][0] == 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;

-    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;

-    $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x := 42]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;

-    $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1 := 43]];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;

-    assert $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1] == $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x] + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)

-{

-  var xs: int;

-

-    xs := xs$in;

-    if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true))

-    {

-        assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;

-        $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][0 := $ArrayContents[xs][0]]];

-    }

-    else

-    {

-    }

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);

-

-

-

-procedure System.Object.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)

-{

-    $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0;

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithArrayTypes.#cctor();

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()

-{

-    RegressionTestInput.ClassWithArrayTypes.s := 0;

-}

-

-

-

-const unique RegressionTestInput.Class0: Type;

-

-var RegressionTestInput.Class0.StaticInt: int;

-

-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;

-    $result := x + 1;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)

-{

-  var x: int;

-  var __temp_1: int;

-  var $tmp4: int;

-  var local_0: int;

-

-    x := x$in;

-    $tmp4 := x;

-    assert $tmp4 != 0;

-    __temp_1 := 5 / $tmp4;

-    x := 3;

-    local_0 := __temp_1 + 3;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;

-    assert (if x == 3 then local_0 <= 8 else false);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;

-    RegressionTestInput.Class0.StaticInt := local_0;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;

-    assert local_0 == RegressionTestInput.Class0.StaticInt;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)

-{

-  var x: int;

-  var y: int;

-

-    x := x$in;

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)

-{

-  var b: bool;

-

-    b := b$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)

-{

-  var c: int;

-

-    c := c$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)

-{

-  var $tmp5: int;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;

-    call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

-    $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);

-

-

-

-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)

-{

-    assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;

-    x$out := 3 + RegressionTestInput.Class0.StaticInt;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;

-    $result := x$out;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);

-

-

-

-implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)

-{

-    x$out := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;

-    x$out := x$out + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;

-    RegressionTestInput.Class0.StaticInt := x$out;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;

-    $result := x$out;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;

-    x := x + 1;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;

-    RegressionTestInput.Class0.StaticInt := x;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;

-    $result := x;

-    return;

-}

-

-

-

-procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

-{

-  var x: int;

-

-    x := x$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;

-    $result := x;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);

-

-

-

-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

-{

-  var y: int;

-  var $tmp6: int;

-

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;

-    call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);

-    $result := $tmp6;

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.Class0.#ctor(this: int)

-{

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.Class0.#cctor();

-

-

-

-implementation RegressionTestInput.Class0.#cctor()

-{

-    RegressionTestInput.Class0.StaticInt := 0;

-}

-

-

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)

-{

-    assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x];

-    assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)

-{

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0;

-    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0;

-    call System.Object.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()

-{

-}

-

-

-

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

-

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

-

-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;

-

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

-{

-  var x: int;

-  var y: int;

-

-    x := x$in;

-    y := y$in;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;

-    $result := x < y;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)

-{

-  var z: bool;

-

-    z := z$in;

-    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;

-    call System.Object.#ctor(this);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

-    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

-    if (z)

-    {

-        assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

-        RegressionTestInput.ClassWithBoolTypes.staticB := z;

-    }

-    else

-    {

-    }

-

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.Main();

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.Main()

-{

-  var $tmp7: bool;

-

-    assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;

-    call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

-    assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;

-    return;

-}

-

-

-

-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()

-{

-    RegressionTestInput.ClassWithBoolTypes.staticB := false;

-}

-

-

-

-const unique RegressionTestInput.AsyncAttribute: Type;

-

-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);

-

-

-

-procedure System.Attribute.#ctor(this: int);

-

-

-

-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)

-{

-    call System.Attribute.#ctor(this);

-    return;

-}

-

-

-

-procedure RegressionTestInput.AsyncAttribute.#cctor();

-

-

-

-implementation RegressionTestInput.AsyncAttribute.#cctor()

-{

-}

-

-

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index dadeb4e5..99b6e680 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -68,21 +68,6 @@ namespace TranslationTest {
     }

 

     [TestMethod]

-    public void TwoDIntHeap() {

-      string dir = TestContext.DeploymentDirectory;

-      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

-      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDIntHeapInput.txt");

-      StreamReader reader = new StreamReader(resource);

-      string expected = reader.ReadToEnd();

-      var result = ExecuteTest(fullPath, new TwoDIntHeap());

-      if (result != expected) {

-        string resultFile = Path.GetFullPath("TwoDIntHeapOutput.txt");

-        File.WriteAllText(resultFile, result);

-        Assert.Fail("Output didn't match TwoDIntHeapInput.txt: " + resultFile);

-      }

-    }

-

-    [TestMethod]

     public void SplitFieldsHeap() {

       string dir = TestContext.DeploymentDirectory;

       var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

@@ -98,21 +83,6 @@ namespace TranslationTest {
     }

 

     [TestMethod]

-    public void TwoDBoxHeap() {

-      string dir = TestContext.DeploymentDirectory;

-      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

-      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDBoxHeapInput.txt");

-      StreamReader reader = new StreamReader(resource);

-      string expected = reader.ReadToEnd();

-      var result = ExecuteTest(fullPath, new TwoDBoxHeap());

-      if (result != expected) {

-        string resultFile = Path.GetFullPath("TwoDBoxHeapOutput.txt");

-        File.WriteAllText(resultFile, result);

-        Assert.Fail("Output didn't match TwoDBoxHeapInput.txt: " + resultFile);

-      }

-    }

-

-    [TestMethod]

     public void GeneralHeap() {

       string dir = TestContext.DeploymentDirectory;

       var fullPath = Path.Combine(dir, "RegressionTestInput.dll");