Fix stub support (still not completely finished).

Fix generation of delegate methods so that they happen after translating all
input assemblies and not per assembly.
Fix translation of typeof() expressions.

4 files changed, 740 insertions, 836 deletions

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 2453ca20..703c908f 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -214,6 +214,8 @@ type Type;
 

 function $DynamicType(ref) : Type;

 

+function $TypeOf(Type) : ref;

+

 var $Head: [int]int;

 

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

@@ -222,165 +224,6 @@ var $Method: [int][int]int;
 

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

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

-

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

-

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

-

-

-

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

-{

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

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

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

-    return;

-}

-

-

-

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

-

-

-

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

-

-

-

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

-{

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

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

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

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()

-{

-}

-

-

-

-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()

-{

-}

-

-

-

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

-

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

-

-const unique RegressionTestInput.ClassWithBoolTypes.b: Field;

-

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

-  var local_0: bool;

-

-    x := x$in;

-    y := y$in;

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

-    local_0 := x < y;

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

-    $result := local_0;

-    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 := Write($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 := Write($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 $tmp0: bool;

-

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

-    call $tmp0 := 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.ClassWithArrayTypes: Type;

 

 var RegressionTestInput.ClassWithArrayTypes.s: int;

@@ -394,20 +237,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

-  var $tmp1: int;

+  var $tmp0: int;

   var local_1: int;

-  var $tmp2: int;

+  var $tmp1: int;

 

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

-    call $tmp1 := Alloc();

-    local_0 := $tmp1;

+    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 $tmp2 := Alloc();

-    local_1 := $tmp2;

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

@@ -426,20 +269,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: int;

+  var $tmp2: int;

   var local_0: int;

-  var $tmp4: int;

+  var $tmp3: int;

 

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

-    call $tmp3 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    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 $tmp4 := Alloc();

-    local_0 := $tmp4;

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

@@ -501,6 +344,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

 

 

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

+

+

+

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

 {

     $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Int2Box(0));

@@ -532,13 +379,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return
 implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x + 1;

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

-    $result := local_0;

+    $result := x + 1;

     return;

 }

 

@@ -552,13 +396,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 {

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp4: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp4 := x;

+    assert $tmp4 != 0;

+    __temp_1 := 5 / $tmp4;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -626,14 +470,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var local_0: int;

-  var $tmp6: int;

+  var $tmp5: int;

 

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

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

-    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

-    $result := local_0;

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

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

     return;

 }

 

@@ -645,14 +486,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (
 

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

 {

-  var local_0: int;

-

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

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

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

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -664,17 +501,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int
 

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

 {

-  var local_0: 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 44} true;

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -687,17 +520,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i
 implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: 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 50} true;

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -710,13 +540,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr
 implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -729,15 +556,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$i
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

 {

   var y: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp6: int;

 

     y := y$in;

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

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

-    local_0 := $tmp7;

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

-    $result := local_0;

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

+    $result := $tmp6;

     return;

 }

 

@@ -765,3 +589,155 @@ implementation RegressionTestInput.Class0.#cctor()
 }

 

 

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

+

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

+

+

+

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

+{

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

+    $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($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 := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));

+    $Heap := Write($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: Field;

+

+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 := Write($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 := Write($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/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 0a042d98..5245bf3d 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -192,6 +192,8 @@ type Type;
 

 function $DynamicType(ref) : Type;

 

+function $TypeOf(Type) : ref;

+

 var $Head: [int]int;

 

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

@@ -200,165 +202,6 @@ var $Method: [int][int]int;
 

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

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

-

-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int;

-

-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int;

-

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

-

-

-

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

-{

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

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

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

-    return;

-}

-

-

-

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

-

-

-

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

-

-

-

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

-{

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

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

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

-    return;

-}

-

-

-

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();

-

-

-

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()

-{

-}

-

-

-

-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()

-{

-}

-

-

-

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

-

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

-

-var RegressionTestInput.ClassWithBoolTypes.b: [int]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;

-  var local_0: bool;

-

-    x := x$in;

-    y := y$in;

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

-    local_0 := x < y;

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

-    $result := local_0;

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

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

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

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

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

-    RegressionTestInput.ClassWithBoolTypes.b[this] := 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 $tmp0: bool;

-

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

-    call $tmp0 := 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.ClassWithArrayTypes: Type;

 

 var RegressionTestInput.ClassWithArrayTypes.s: int;

@@ -372,20 +215,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

-  var $tmp1: int;

+  var $tmp0: int;

   var local_1: int;

-  var $tmp2: int;

+  var $tmp1: int;

 

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

-    call $tmp1 := Alloc();

-    local_0 := $tmp1;

+    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 $tmp2 := Alloc();

-    local_1 := $tmp2;

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

@@ -404,20 +247,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: int;

+  var $tmp2: int;

   var local_0: int;

-  var $tmp4: int;

+  var $tmp3: int;

 

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

-    call $tmp3 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    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 $tmp4 := Alloc();

-    local_0 := $tmp4;

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

@@ -479,6 +322,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

 

 

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

+

+

+

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

 {

     RegressionTestInput.ClassWithArrayTypes.a[this] := 0;

@@ -510,13 +357,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return
 implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x + 1;

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

-    $result := local_0;

+    $result := x + 1;

     return;

 }

 

@@ -530,13 +374,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 {

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp4: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp4 := x;

+    assert $tmp4 != 0;

+    __temp_1 := 5 / $tmp4;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -604,14 +448,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var local_0: int;

-  var $tmp6: int;

+  var $tmp5: int;

 

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

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

-    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

-    $result := local_0;

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

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

     return;

 }

 

@@ -623,14 +464,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (
 

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

 {

-  var local_0: int;

-

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

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

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

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -642,17 +479,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int
 

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

 {

-  var local_0: 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 44} true;

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -665,17 +498,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i
 implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: 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 50} true;

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -688,13 +518,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr
 implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -707,15 +534,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$i
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

 {

   var y: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp6: int;

 

     y := y$in;

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

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

-    local_0 := $tmp7;

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

-    $result := local_0;

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

+    $result := $tmp6;

     return;

 }

 

@@ -743,3 +567,155 @@ implementation RegressionTestInput.Class0.#cctor()
 }

 

 

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

+

+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int;

+

+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int;

+

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

+

+

+

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

+{

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

+    RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];

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

+    return;

+}

+

+

+

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

+

+

+

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

+{

+    RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;

+    RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 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;

+

+var RegressionTestInput.ClassWithBoolTypes.b: [int]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;

+    RegressionTestInput.ClassWithBoolTypes.b[this] := false;

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

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

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

+    RegressionTestInput.ClassWithBoolTypes.b[this] := 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/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index 0f3d356b..c23df829 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -200,6 +200,8 @@ type Type;
 

 function $DynamicType(ref) : Type;

 

+function $TypeOf(Type) : ref;

+

 var $Head: [int]int;

 

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

@@ -208,165 +210,6 @@ var $Method: [int][int]int;
 

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

 

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

-

-

-

-procedure System.Object.#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.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()

-{

-}

-

-

-

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

-  var local_0: bool;

-

-    x := x$in;

-    y := y$in;

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

-    local_0 := x < y;

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

-    $result := local_0;

-    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 $tmp0: bool;

-

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

-    call $tmp0 := 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.ClassWithArrayTypes: Type;

 

 var RegressionTestInput.ClassWithArrayTypes.s: int;

@@ -380,20 +223,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

-  var $tmp1: int;

+  var $tmp0: int;

   var local_1: int;

-  var $tmp2: int;

+  var $tmp1: int;

 

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

-    call $tmp1 := Alloc();

-    local_0 := $tmp1;

+    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 $tmp2 := Alloc();

-    local_1 := $tmp2;

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

@@ -412,20 +255,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: int;

+  var $tmp2: int;

   var local_0: int;

-  var $tmp4: int;

+  var $tmp3: int;

 

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

-    call $tmp3 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    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 $tmp4 := Alloc();

-    local_0 := $tmp4;

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

@@ -487,6 +330,10 @@ 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);

@@ -518,13 +365,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return
 implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x + 1;

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

-    $result := local_0;

+    $result := x + 1;

     return;

 }

 

@@ -538,13 +382,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 {

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp4: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp4 := x;

+    assert $tmp4 != 0;

+    __temp_1 := 5 / $tmp4;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -612,14 +456,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var local_0: int;

-  var $tmp6: int;

+  var $tmp5: int;

 

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

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

-    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

-    $result := local_0;

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

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

     return;

 }

 

@@ -631,14 +472,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (
 

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

 {

-  var local_0: int;

-

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

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

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

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -650,17 +487,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int
 

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

 {

-  var local_0: 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 44} true;

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -673,17 +506,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i
 implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: 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 50} true;

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -696,13 +526,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr
 implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -715,15 +542,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$i
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

 {

   var y: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp6: int;

 

     y := y$in;

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

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

-    local_0 := $tmp7;

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

-    $result := local_0;

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

+    $result := $tmp6;

     return;

 }

 

@@ -751,3 +575,155 @@ implementation RegressionTestInput.Class0.#cctor()
 }

 

 

+

+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
index 6a9272de..262958c0 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -190,6 +190,8 @@ type Type;
 

 function $DynamicType(ref) : Type;

 

+function $TypeOf(Type) : ref;

+

 var $Head: [int]int;

 

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

@@ -198,165 +200,6 @@ var $Method: [int][int]int;
 

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

 

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

-

-

-

-procedure System.Object.#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.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()

-{

-}

-

-

-

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

-  var local_0: bool;

-

-    x := x$in;

-    y := y$in;

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

-    local_0 := x < y;

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

-    $result := local_0;

-    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 $tmp0: bool;

-

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

-    call $tmp0 := 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.ClassWithArrayTypes: Type;

 

 var RegressionTestInput.ClassWithArrayTypes.s: int;

@@ -370,20 +213,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

-  var $tmp1: int;

+  var $tmp0: int;

   var local_1: int;

-  var $tmp2: int;

+  var $tmp1: int;

 

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

-    call $tmp1 := Alloc();

-    local_0 := $tmp1;

+    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 $tmp2 := Alloc();

-    local_1 := $tmp2;

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

@@ -402,20 +245,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: int;

+  var $tmp2: int;

   var local_0: int;

-  var $tmp4: int;

+  var $tmp3: int;

 

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

-    call $tmp3 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    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 $tmp4 := Alloc();

-    local_0 := $tmp4;

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

@@ -477,6 +320,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

 

 

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

+

+

+

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

 {

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

@@ -508,13 +355,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return
 implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x + 1;

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

-    $result := local_0;

+    $result := x + 1;

     return;

 }

 

@@ -528,13 +372,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 {

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp4: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp4 := x;

+    assert $tmp4 != 0;

+    __temp_1 := 5 / $tmp4;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -602,14 +446,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var local_0: int;

-  var $tmp6: int;

+  var $tmp5: int;

 

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

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

-    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

-    $result := local_0;

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

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

     return;

 }

 

@@ -621,14 +462,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (
 

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

 {

-  var local_0: int;

-

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

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

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

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -640,17 +477,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int
 

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

 {

-  var local_0: 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 44} true;

-    local_0 := x$out;

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

-    $result := local_0;

+    $result := x$out;

     return;

 }

 

@@ -663,17 +496,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i
 implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: 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 50} true;

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -686,13 +516,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr
 implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

 {

   var x: int;

-  var local_0: int;

 

     x := x$in;

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

-    local_0 := x;

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

-    $result := local_0;

+    $result := x;

     return;

 }

 

@@ -705,15 +532,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$i
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

 {

   var y: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp6: int;

 

     y := y$in;

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

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

-    local_0 := $tmp7;

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

-    $result := local_0;

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

+    $result := $tmp6;

     return;

 }

 

@@ -741,3 +565,155 @@ implementation RegressionTestInput.Class0.#cctor()
 }

 

 

+

+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()

+{

+}

+

+