Cleanup of new LHS simplification and replaced the golden output with the

new regression output.

3 files changed, 441 insertions, 394 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 81c25cf1..d1af8142 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -659,24 +659,19 @@ namespace BytecodeTranslator
     public override void Visit(IAssignment assignment) {

       Contract.Assert(TranslatedExpressions.Count == 0);

 

-

-      //var localDeclaration = AssignmentSimplifier_FirstTry.Simplify(this.sink.host, assignment.Target);

-      //if (localDeclaration != null) {

-      //  this.StmtTraverser.Visit(localDeclaration);

-      //}

-

       #region Transform Right Hand Side ...

       this.Visit(assignment.Source);

       Bpl.Expr sourceexp = this.TranslatedExpressions.Pop();

       #endregion

 

+      // Simplify the LHS so that all nested dereferences and method calls are broken

+      // up into separate assignments to locals.

       var blockExpression = AssignmentSimplifier.Simplify(this.sink, assignment.Target);

       foreach (var s in blockExpression.BlockStatement.Statements) {

         this.StmtTraverser.Visit(s);

       }

       var target = blockExpression.Expression as ITargetExpression;

 

-      //var target = assignment.Target;

       var fieldReference = target.Definition as IFieldReference;

 

 

@@ -1212,56 +1207,6 @@ namespace BytecodeTranslator
     #endregion

 

     /// <summary>

-    /// Actually a mutator! It will downcast and whack if/when it finds the right spot in the tree!

-    /// If found, replaces the "right-most object" on the left-hand side of an asignment with a local.

-    /// A local declaration statement is created (and stored in a field of this class) that initializes

-    /// the local to the part of the tree it replaced.

-    /// </summary>

-    private class AssignmentSimplifier_FirstTry : BaseCodeTraverser {

-      IMetadataHost host;

-      private ILocalDeclarationStatement/*?*/ localDeclarationStatement;

-      private AssignmentSimplifier_FirstTry(IMetadataHost host)

-        : base() {

-        this.host = host;

-      }

-      public static ILocalDeclarationStatement/*?*/ Simplify(IMetadataHost host, ITargetExpression targetExpression) {

-        var a = new AssignmentSimplifier_FirstTry(host);

-        a.Visit(targetExpression);

-        return a.localDeclarationStatement;

-      }

-      public override void Visit(IBoundExpression boundExpression) {

-        if (boundExpression.Instance == null) {

-          this.stopTraversal = true;

-          return;

-        }

-        var loc = new LocalDefinition() {

-          Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment

-          Type = boundExpression.Type,

-        };

-        var mutableBoundExpression = (BoundExpression)boundExpression;

-        var init = new LocalDeclarationStatement() {

-          InitialValue = new BoundExpression(){

-            Definition = boundExpression.Definition,

-            Instance = boundExpression.Instance,

-            Type = boundExpression.Type,

-          },

-          LocalVariable = loc,

-          Locations = mutableBoundExpression.Locations,

-        };

-        this.localDeclarationStatement = init;

-        mutableBoundExpression.Instance = null;

-        mutableBoundExpression.Definition = loc;

-        this.stopTraversal = true;

-        return;

-      }

-

-      public override void Visit(ITargetExpression targetExpression) {

-        base.Visit(targetExpression);

-      }

-

-    }

-

-    /// <summary>

     /// This is a rewriter so it must be used on a mutable Code Model!!!

     /// </summary>

     private class AssignmentSimplifier : CodeRewriter {

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 0ff36879..98d25303 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -1,29 +1,21 @@
 // Copyright (c) 2010, Microsoft Corp.

 // Bytecode Translator prelude

 

-const null: ref;

+type Struct = [Field]Box;

 

-type ref = int;

-

-type struct = [Field]box;

-

-type HeapType = [ref,Field]box;

+type HeapType = [Ref,Field]Box;

 

 function IsGoodHeap(HeapType) : bool;

 

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

-

-var $ArrayLength: [int]int;

+var $Alloc: [Ref]bool;

 

-var $Alloc: [ref]bool;

-

-procedure {:inline 1} Alloc() returns (x: ref);

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

   modifies $Alloc;

   free ensures x != null;

 

 

 

-implementation Alloc() returns (x: ref)

+implementation Alloc() returns (x: Ref)

 {

     assume $Alloc[x] == false;

     $Alloc[x] := true;

@@ -41,21 +33,21 @@ axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
 

 axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);

 

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

+procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref);

 

 

 

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

+implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

-  var o: int;

+  var o: Ref;

 

-    if (a == 0)

+    if (a == null)

     {

         c := b;

         return;

     }

-    else if (b == 0)

+    else if (b == null)

     {

         c := a;

         return;

@@ -72,21 +64,21 @@ implementation DelegateAdd(a: int, b: int) returns (c: int)
 

 

 

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

+procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

 

 

 

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

+implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

-  var o: int;

+  var o: Ref;

 

-    if (a == 0)

+    if (a == null)

     {

-        c := 0;

+        c := null;

         return;

     }

-    else if (b == 0)

+    else if (b == null)

     {

         c := a;

         return;

@@ -103,13 +95,13 @@ implementation DelegateRemove(a: int, b: int) returns (c: int)
 

 

 

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

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

 

 

 

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

+implementation GetFirstElement(i: Ref) returns (m: int, o: Ref)

 {

-  var first: int;

+  var first: Ref;

 

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

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

@@ -118,16 +110,16 @@ implementation GetFirstElement(i: int) returns (m: int, o: int)
 

 

 

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

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

 

 

 

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

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

 {

-  var x: int;

-  var h: int;

+  var x: Ref;

+  var h: Ref;

 

-    if (oldi == 0)

+    if (oldi == null)

     {

         call i := Alloc();

         call x := Alloc();

@@ -150,23 +142,23 @@ implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)
 

 

 

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

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

 

 

 

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

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

 {

-  var prev: int;

-  var iter: int;

-  var niter: int;

+  var prev: Ref;

+  var iter: Ref;

+  var niter: Ref;

 

     i := oldi;

-    if (i == 0)

+    if (i == null)

     {

         return;

     }

 

-    prev := 0;

+    prev := null;

     iter := $Head[i];

     while (true)

     {

@@ -184,7 +176,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
         iter := niter;

     }

 

-    if (prev == 0)

+    if (prev == null)

     {

         return;

     }

@@ -192,7 +184,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
     $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

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

     {

-        i := 0;

+        i := null;

     }

 }

 

@@ -200,53 +192,73 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
 

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

 

-function {:inline true} Read(H: HeapType, o: ref, f: Field) : box

+function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Box

 {

   H[o, f]

 }

 

-function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType

+function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Box) : HeapType

 {

   H[o, f := v]

 }

 

+var $ArrayContents: [Ref][int]Box;

+

+var $ArrayLength: [Ref]int;

+

 type Field;

 

-type box;

+type Box;

 

-const unique $DefaultBox: box;

+const unique $DefaultBox: Box;

 

-const unique $DefaultStruct: struct;

+type Ref;

+

+const unique null: Ref;

 

 type Type;

 

-function Box2Int(box) : int;

+const unique $DefaultStruct: Struct;

+

+function Box2Int(Box) : int;

 

-function Box2Bool(box) : bool;

+function Box2Bool(Box) : bool;

 

-function Box2Struct(box) : struct;

+function Box2Struct(Box) : Struct;

 

-function Int2Box(int) : box;

+function Box2Ref(Box) : Ref;

 

-function Bool2Box(bool) : box;

+function Int2Box(int) : Box;

 

-function Struct2Box(struct) : box;

+function Bool2Box(bool) : Box;

 

-function $DynamicType(ref) : Type;

+function Struct2Box(Struct) : Box;

 

-function $TypeOf(Type) : ref;

+function Ref2Box(Ref) : Box;

 

-var $Head: [int]int;

+function Struct2Ref(Struct) : Ref;

 

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

+function Int2Ref(int) : Ref;

 

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

+function Bool2Ref(bool) : Ref;

 

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

+function $DynamicType(Ref) : Type;

+

+function $TypeOf(Type) : Ref;

+

+function $As(Ref, Type) : Ref;

+

+var $Head: [Ref]Ref;

+

+var $Next: [Ref][Ref]Ref;

+

+var $Method: [Ref][Ref]int;

+

+var $Receiver: [Ref][Ref]Ref;

 

 const unique RegressionTestInput.ClassWithArrayTypes: Type;

 

-var RegressionTestInput.ClassWithArrayTypes.s: int;

+var RegressionTestInput.ClassWithArrayTypes.s: Ref;

 

 const unique RegressionTestInput.ClassWithArrayTypes.a: Field;

 

@@ -256,33 +268,37 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

-  var local_0: int;

-  var $tmp0: int;

+  var local_0: Ref;

+  var $tmp0: Ref;

   var $tmp1: int;

-  var local_1: int;

   var $tmp2: int;

-  var $tmp3: int;

+  var local_1: Ref;

+  var $tmp3: Ref;

   var $tmp4: int;

+  var $tmp5: int;

+  var $tmp6: 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]];

+    $tmp1 := Box2Int($ArrayContents[local_0][0]);

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]];

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

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

-    assert $tmp1 == 2;

+    $tmp2 := Box2Int($ArrayContents[local_0][0]);

+    assert $tmp2 == 2;

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

-    call $tmp2 := Alloc();

-    local_1 := $tmp2;

+    call $tmp3 := Alloc();

+    local_1 := $tmp3;

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

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

+    $tmp4 := Box2Int($ArrayContents[local_1][0]);

+    $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]];

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

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

-    assert $tmp3 == 1;

+    $tmp5 := Box2Int($ArrayContents[local_1][0]);

+    assert $tmp5 == 1;

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

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

-    assert $tmp4 == 2;

+    $tmp6 := Box2Int($ArrayContents[local_0][0]);

+    assert $tmp6 == 2;

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

     return;

 }

@@ -295,78 +311,104 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp5: int;

-  var $tmp6: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp7: Ref;

   var $tmp8: int;

   var $tmp9: int;

+  var local_0: Ref;

+  var $tmp10: Ref;

+  var $tmp11: int;

+  var $tmp12: int;

+  var $tmp13: int;

 

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

-    call $tmp5 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp5;

+    call $tmp7 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp7;

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

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

+    $tmp8 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];

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

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

-    assert $tmp6 == 2;

+    $tmp9 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);

+    assert $tmp9 == 2;

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

-    call $tmp7 := Alloc();

-    local_0 := $tmp7;

+    call $tmp10 := Alloc();

+    local_0 := $tmp10;

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

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

+    $tmp11 := Box2Int($ArrayContents[local_0][0]);

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]];

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

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

-    assert $tmp8 == 1;

+    $tmp12 := Box2Int($ArrayContents[local_0][0]);

+    assert $tmp12 == 1;

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

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

-    assert $tmp9 == 2;

+    $tmp13 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]);

+    assert $tmp13 == 2;

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

-  var $tmp10: int;

-  var $tmp11: int;

+  var _loc0: Ref;

+  var $tmp14: Ref;

+  var $tmp15: int;

+  var _loc1: Ref;

+  var $tmp16: Ref;

+  var $tmp17: int;

+  var $tmp18: Ref;

+  var $tmp19: int;

+  var $tmp20: Ref;

+  var $tmp21: int;

 

     x := x$in;

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

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

+    $tmp14 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));

+    _loc0 := $tmp14;

+    $tmp15 := Box2Int($ArrayContents[_loc0][x]);

+    $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := Int2Box(42)]];

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

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

+    $tmp16 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));

+    _loc1 := $tmp16;

+    $tmp17 := Box2Int($ArrayContents[_loc1][x + 1]);

+    $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := Int2Box(43)]];

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

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

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

-    assert $tmp10 == $tmp11 + 1;

+    $tmp18 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));

+    $tmp19 := Box2Int($ArrayContents[$tmp18][x + 1]);

+    $tmp20 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));

+    $tmp21 := Box2Int($ArrayContents[$tmp20][x]);

+    assert $tmp19 == $tmp21 + 1;

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

     return;

 }

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref)

 {

-  var xs: int;

-  var $tmp12: int;

+  var xs: Ref;

+  var $tmp22: int;

+  var _loc0: Ref;

+  var $tmp23: Ref;

+  var $tmp24: int;

 

     xs := xs$in;

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

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

     {

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

-        $tmp12 := $ArrayContents[xs][0];

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

+        $tmp22 := Box2Int($ArrayContents[xs][0]);

+        $tmp23 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a));

+        _loc0 := $tmp23;

+        $tmp24 := Box2Int($ArrayContents[_loc0][0]);

+        $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := Int2Box($tmp22)]];

     }

     else

     {

@@ -378,17 +420,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
 

 

 

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

+procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref);

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref)

 {

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

+    $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));

     call System.Object.#ctor(this);

     return;

 }

@@ -401,7 +443,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
 

 implementation RegressionTestInput.ClassWithArrayTypes.#cctor()

 {

-    RegressionTestInput.ClassWithArrayTypes.s := 0;

+    RegressionTestInput.ClassWithArrayTypes.s := null;

 }

 

 

@@ -423,11 +465,11 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 

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

+procedure RegressionTestInput.RefParameters.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.RefParameters.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;

@@ -465,21 +507,21 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

   var __temp_1: int;

-  var $tmp13: int;

+  var $tmp25: int;

   var local_0: int;

 

     x := x$in;

-    $tmp13 := x;

-    assert $tmp13 != 0;

-    __temp_1 := 5 / $tmp13;

+    $tmp25 := x;

+    assert $tmp25 != 0;

+    __temp_1 := 5 / $tmp25;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -494,11 +536,11 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

   var y: int;

@@ -511,11 +553,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int,
 

 

 

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

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

 

 

 

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

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

 {

   var b: bool;

 

@@ -526,13 +568,13 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool
 

 

 

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

+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref);

 

 

 

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

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref)

 {

-  var c: int;

+  var c: Ref;

 

     c := c$in;

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

@@ -541,27 +583,27 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int
 

 

 

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

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

 

 

 

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

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

 {

-  var $tmp14: int;

+  var $tmp26: int;

 

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

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

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

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

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

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

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

@@ -572,11 +614,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) retu
 

 

 

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

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, 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)

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

 {

     x$out := x$in;

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

@@ -590,11 +632,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

 

@@ -610,11 +652,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

 

@@ -626,29 +668,29 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 

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

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

 

 

 

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

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

 {

   var y: int;

-  var $tmp15: int;

+  var $tmp27: int;

 

     y := y$in;

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

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

-    $result := $tmp15;

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

+    $result := $tmp27;

     return;

 }

 

 

 

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

+procedure RegressionTestInput.Class0.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.Class0.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;

@@ -673,25 +715,28 @@ const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
 

 const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

 

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

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

 

 

 

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

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

 {

+  var $tmp28: int;

+

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

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

+    $tmp28 := Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x));

+    $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box($tmp28));

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

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

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

@@ -735,11 +780,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 

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

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

 

 

 

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

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

 {

   var z: bool;

 

@@ -770,10 +815,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp16: bool;

+  var $tmp29: bool;

 

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

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

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

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

     return;

 }

@@ -799,15 +844,15 @@ const unique RegressionTestInput.S.b: Field;
 

 const unique RegressionTestInput.AsyncAttribute: Type;

 

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

+procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);

 

 

 

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

+procedure System.Attribute.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)

 {

     call System.Attribute.#ctor(this);

     return;

@@ -827,20 +872,24 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 

 const unique RegressionTestInput.CreateStruct: Type;

 

-procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box);

+procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);

 

 

 

-implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box)

+implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)

 {

-  var local_0: [Field]box;

+  var local_0: [Field]Box;

+  var $tmp30: int;

+  var $tmp31: bool;

 

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

     local_0 := $DefaultStruct;

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

-    assert Box2Int(local_0[RegressionTestInput.S.x]) == 0;

+    $tmp30 := Box2Int(local_0[RegressionTestInput.S.x]);

+    assert $tmp30 == 0;

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

-    assert !Box2Bool(local_0[RegressionTestInput.S.b]);

+    $tmp31 := Box2Bool(local_0[RegressionTestInput.S.b]);

+    assert !$tmp31;

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

     $result := local_0;

     return;

@@ -848,19 +897,21 @@ implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($resu
 

 

 

-procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box);

+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);

 

 

 

-implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box)

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)

 {

-  var s: [Field]box;

+  var s: [Field]Box;

+  var $tmp32: int;

 

     s := s$in;

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

     s := s[RegressionTestInput.S.x := Int2Box(3)];

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

-    assert Box2Int(s[RegressionTestInput.S.x]) == 3;

+    $tmp32 := Box2Int(s[RegressionTestInput.S.x]);

+    assert $tmp32 == 3;

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

     $result := s;

     return;

@@ -868,11 +919,11 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 

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

+procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 53e9a8c3..6e450f38 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -1,31 +1,23 @@
 // Copyright (c) 2010, Microsoft Corp.

 // Bytecode Translator prelude

 

-const null: int;

+type Struct = [Field]Box;

 

-type ref = int;

-

-type struct = [Field]box;

-

-type HeapType = [int,int]int;

+type HeapType = [Ref,Field]Box;

 

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

 

 function IsGoodHeap(HeapType) : bool;

 

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

-

-var $ArrayLength: [int]int;

+var $Alloc: [Ref]bool;

 

-var $Alloc: [int]bool;

-

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

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

   modifies $Alloc;

-  free ensures x != 0;

+  free ensures x != null;

 

 

 

-implementation Alloc() returns (x: int)

+implementation Alloc() returns (x: Ref)

 {

     assume $Alloc[x] == false;

     $Alloc[x] := true;

@@ -43,21 +35,21 @@ axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
 

 axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);

 

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

+procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref);

 

 

 

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

+implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

-  var o: int;

+  var o: Ref;

 

-    if (a == 0)

+    if (a == null)

     {

         c := b;

         return;

     }

-    else if (b == 0)

+    else if (b == null)

     {

         c := a;

         return;

@@ -74,21 +66,21 @@ implementation DelegateAdd(a: int, b: int) returns (c: int)
 

 

 

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

+procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

 

 

 

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

+implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

-  var o: int;

+  var o: Ref;

 

-    if (a == 0)

+    if (a == null)

     {

-        c := 0;

+        c := null;

         return;

     }

-    else if (b == 0)

+    else if (b == null)

     {

         c := a;

         return;

@@ -105,13 +97,13 @@ implementation DelegateRemove(a: int, b: int) returns (c: int)
 

 

 

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

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

 

 

 

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

+implementation GetFirstElement(i: Ref) returns (m: int, o: Ref)

 {

-  var first: int;

+  var first: Ref;

 

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

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

@@ -120,16 +112,16 @@ implementation GetFirstElement(i: int) returns (m: int, o: int)
 

 

 

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

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

 

 

 

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

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

 {

-  var x: int;

-  var h: int;

+  var x: Ref;

+  var h: Ref;

 

-    if (oldi == 0)

+    if (oldi == null)

     {

         call i := Alloc();

         call x := Alloc();

@@ -152,23 +144,23 @@ implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)
 

 

 

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

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

 

 

 

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

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

 {

-  var prev: int;

-  var iter: int;

-  var niter: int;

+  var prev: Ref;

+  var iter: Ref;

+  var niter: Ref;

 

     i := oldi;

-    if (i == 0)

+    if (i == null)

     {

         return;

     }

 

-    prev := 0;

+    prev := null;

     iter := $Head[i];

     while (true)

     {

@@ -186,7 +178,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
         iter := niter;

     }

 

-    if (prev == 0)

+    if (prev == null)

     {

         return;

     }

@@ -194,51 +186,71 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
     $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

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

     {

-        i := 0;

+        i := null;

     }

 }

 

 

 

+var $ArrayContents: [Ref][int]Box;

+

+var $ArrayLength: [Ref]int;

+

 type Field;

 

-type box;

+type Box;

+

+const unique $DefaultBox: Box;

 

-const unique $DefaultBox: box;

+type Ref;

 

-const unique $DefaultStruct: struct;

+const unique null: Ref;

 

 type Type;

 

-function Box2Int(box) : int;

+const unique $DefaultStruct: Struct;

+

+function Box2Int(Box) : int;

+

+function Box2Bool(Box) : bool;

 

-function Box2Bool(box) : bool;

+function Box2Struct(Box) : Struct;

 

-function Box2Struct(box) : struct;

+function Box2Ref(Box) : Ref;

 

-function Int2Box(int) : box;

+function Int2Box(int) : Box;

 

-function Bool2Box(bool) : box;

+function Bool2Box(bool) : Box;

 

-function Struct2Box(struct) : box;

+function Struct2Box(Struct) : Box;

 

-function $DynamicType(ref) : Type;

+function Ref2Box(Ref) : Box;

 

-function $TypeOf(Type) : ref;

+function Struct2Ref(Struct) : Ref;

 

-var $Head: [int]int;

+function Int2Ref(int) : Ref;

 

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

+function Bool2Ref(bool) : Ref;

 

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

+function $DynamicType(Ref) : Type;

 

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

+function $TypeOf(Type) : Ref;

+

+function $As(Ref, Type) : Ref;

+

+var $Head: [Ref]Ref;

+

+var $Next: [Ref][Ref]Ref;

+

+var $Method: [Ref][Ref]int;

+

+var $Receiver: [Ref][Ref]Ref;

 

 const unique RegressionTestInput.ClassWithArrayTypes: Type;

 

-var RegressionTestInput.ClassWithArrayTypes.s: int;

+var RegressionTestInput.ClassWithArrayTypes.s: Ref;

 

-var RegressionTestInput.ClassWithArrayTypes.a: [int]int;

+var RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref;

 

 procedure RegressionTestInput.ClassWithArrayTypes.Main1();

 

@@ -246,33 +258,37 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

-  var local_0: int;

-  var $tmp0: int;

+  var local_0: Ref;

+  var $tmp0: Ref;

   var $tmp1: int;

-  var local_1: int;

   var $tmp2: int;

-  var $tmp3: int;

+  var local_1: Ref;

+  var $tmp3: Ref;

   var $tmp4: int;

+  var $tmp5: int;

+  var $tmp6: int;

 

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

     call $tmp0 := Alloc();

     local_0 := $tmp0;

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

+    $tmp1 := $ArrayContents[local_0][0];

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

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

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

-    assert $tmp1 == 2;

+    $tmp2 := $ArrayContents[local_0][0];

+    assert $tmp2 == 2;

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

-    call $tmp2 := Alloc();

-    local_1 := $tmp2;

+    call $tmp3 := Alloc();

+    local_1 := $tmp3;

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

+    $tmp4 := $ArrayContents[local_1][0];

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

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

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

-    assert $tmp3 == 1;

+    $tmp5 := $ArrayContents[local_1][0];

+    assert $tmp5 == 1;

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

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

-    assert $tmp4 == 2;

+    $tmp6 := $ArrayContents[local_0][0];

+    assert $tmp6 == 2;

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

     return;

 }

@@ -285,78 +301,104 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp5: int;

-  var $tmp6: int;

-  var local_0: int;

-  var $tmp7: int;

+  var $tmp7: Ref;

   var $tmp8: int;

   var $tmp9: int;

+  var local_0: Ref;

+  var $tmp10: Ref;

+  var $tmp11: int;

+  var $tmp12: int;

+  var $tmp13: int;

 

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

-    call $tmp5 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp5;

+    call $tmp7 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp7;

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

+    $tmp8 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];

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

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

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

-    assert $tmp6 == 2;

+    $tmp9 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];

+    assert $tmp9 == 2;

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

-    call $tmp7 := Alloc();

-    local_0 := $tmp7;

+    call $tmp10 := Alloc();

+    local_0 := $tmp10;

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

+    $tmp11 := $ArrayContents[local_0][0];

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

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

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

-    assert $tmp8 == 1;

+    $tmp12 := $ArrayContents[local_0][0];

+    assert $tmp12 == 1;

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

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

-    assert $tmp9 == 2;

+    $tmp13 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0];

+    assert $tmp13 == 2;

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

-  var $tmp10: int;

-  var $tmp11: int;

+  var _loc0: Ref;

+  var $tmp14: Ref;

+  var $tmp15: int;

+  var _loc1: Ref;

+  var $tmp16: Ref;

+  var $tmp17: int;

+  var $tmp18: Ref;

+  var $tmp19: int;

+  var $tmp20: Ref;

+  var $tmp21: int;

 

     x := x$in;

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

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

+    $tmp14 := RegressionTestInput.ClassWithArrayTypes.a[this];

+    _loc0 := $tmp14;

+    $tmp15 := $ArrayContents[_loc0][x];

+    $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := 42]];

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

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

+    $tmp16 := RegressionTestInput.ClassWithArrayTypes.a[this];

+    _loc1 := $tmp16;

+    $tmp17 := $ArrayContents[_loc1][x + 1];

+    $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := 43]];

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

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

-    $tmp11 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x];

-    assert $tmp10 == $tmp11 + 1;

+    $tmp18 := RegressionTestInput.ClassWithArrayTypes.a[this];

+    $tmp19 := $ArrayContents[$tmp18][x + 1];

+    $tmp20 := RegressionTestInput.ClassWithArrayTypes.a[this];

+    $tmp21 := $ArrayContents[$tmp20][x];

+    assert $tmp19 == $tmp21 + 1;

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

     return;

 }

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref)

 {

-  var xs: int;

-  var $tmp12: int;

+  var xs: Ref;

+  var $tmp22: int;

+  var _loc0: Ref;

+  var $tmp23: Ref;

+  var $tmp24: int;

 

     xs := xs$in;

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

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

     {

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

-        $tmp12 := $ArrayContents[xs][0];

-        $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][0 := $tmp12]];

+        $tmp22 := $ArrayContents[xs][0];

+        $tmp23 := RegressionTestInput.ClassWithArrayTypes.a[this];

+        _loc0 := $tmp23;

+        $tmp24 := $ArrayContents[_loc0][0];

+        $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := $tmp22]];

     }

     else

     {

@@ -368,17 +410,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
 

 

 

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

+procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref);

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref)

 {

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

+    RegressionTestInput.ClassWithArrayTypes.a[this] := null;

     call System.Object.#ctor(this);

     return;

 }

@@ -391,7 +433,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
 

 implementation RegressionTestInput.ClassWithArrayTypes.#cctor()

 {

-    RegressionTestInput.ClassWithArrayTypes.s := 0;

+    RegressionTestInput.ClassWithArrayTypes.s := null;

 }

 

 

@@ -413,11 +455,11 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 

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

+procedure RegressionTestInput.RefParameters.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.RefParameters.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;

@@ -455,21 +497,21 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

   var __temp_1: int;

-  var $tmp13: int;

+  var $tmp25: int;

   var local_0: int;

 

     x := x$in;

-    $tmp13 := x;

-    assert $tmp13 != 0;

-    __temp_1 := 5 / $tmp13;

+    $tmp25 := x;

+    assert $tmp25 != 0;

+    __temp_1 := 5 / $tmp25;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -484,11 +526,11 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

   var y: int;

@@ -501,11 +543,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int,
 

 

 

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

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

 

 

 

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

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

 {

   var b: bool;

 

@@ -516,13 +558,13 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool
 

 

 

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

+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref);

 

 

 

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

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref)

 {

-  var c: int;

+  var c: Ref;

 

     c := c$in;

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

@@ -531,27 +573,27 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int
 

 

 

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

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

 

 

 

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

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

 {

-  var $tmp14: int;

+  var $tmp26: int;

 

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

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

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

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

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

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

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

@@ -562,11 +604,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) retu
 

 

 

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

+procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, 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)

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

 {

     x$out := x$in;

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

@@ -580,11 +622,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

 

@@ -600,11 +642,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int
 

 

 

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

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

 

 

 

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

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

 {

   var x: int;

 

@@ -616,29 +658,29 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 

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

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

 

 

 

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

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

 {

   var y: int;

-  var $tmp15: int;

+  var $tmp27: int;

 

     y := y$in;

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

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

-    $result := $tmp15;

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

+    $result := $tmp27;

     return;

 }

 

 

 

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

+procedure RegressionTestInput.Class0.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.Class0.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;

@@ -659,29 +701,32 @@ implementation RegressionTestInput.Class0.#cctor()
 

 const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

 

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

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

 

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

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

 

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

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

 

 

 

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

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

 {

+  var $tmp28: int;

+

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

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

+    $tmp28 := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];

+    RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := $tmp28;

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

     return;

 }

 

 

 

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

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

 

 

 

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

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

 {

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

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

@@ -705,7 +750,7 @@ const unique RegressionTestInput.ClassWithBoolTypes: Type;
 

 var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

 

-var RegressionTestInput.ClassWithBoolTypes.b: [int]bool;

+var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;

 

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

 

@@ -725,11 +770,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 

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

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

 

 

 

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

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

 {

   var z: bool;

 

@@ -760,10 +805,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp16: bool;

+  var $tmp29: bool;

 

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

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

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

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

     return;

 }

@@ -783,21 +828,21 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
 

 const unique RegressionTestInput.S: Type;

 

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

+var RegressionTestInput.S.x: [Ref]int;

 

-var RegressionTestInput.S.b: [int]bool;

+var RegressionTestInput.S.b: [Ref]bool;

 

 const unique RegressionTestInput.AsyncAttribute: Type;

 

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

+procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);

 

 

 

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

+procedure System.Attribute.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref)

 {

     call System.Attribute.#ctor(this);

     return;

@@ -817,20 +862,24 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 

 const unique RegressionTestInput.CreateStruct: Type;

 

-procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box);

+procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box);

 

 

 

-implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box)

+implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box)

 {

-  var local_0: [Field]box;

+  var local_0: [Field]Box;

+  var $tmp30: int;

+  var $tmp31: bool;

 

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

     local_0 := $DefaultStruct;

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

-    assert local_0[RegressionTestInput.S.x] == 0;

+    $tmp30 := local_0[RegressionTestInput.S.x];

+    assert $tmp30 == 0;

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

-    assert !local_0[RegressionTestInput.S.b];

+    $tmp31 := local_0[RegressionTestInput.S.b];

+    assert !$tmp31;

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

     $result := local_0;

     return;

@@ -838,19 +887,21 @@ implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($resu
 

 

 

-procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box);

+procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box);

 

 

 

-implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box)

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box)

 {

-  var s: [Field]box;

+  var s: [Field]Box;

+  var $tmp32: int;

 

     s := s$in;

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

     s[RegressionTestInput.S.x] := 3;

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

-    assert s[RegressionTestInput.S.x] == 3;

+    $tmp32 := s[RegressionTestInput.S.x];

+    assert $tmp32 == 3;

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

     $result := s;

     return;

@@ -858,11 +909,11 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 

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

+procedure RegressionTestInput.CreateStruct.#ctor(this: Ref);

 

 

 

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

+implementation RegressionTestInput.CreateStruct.#ctor(this: Ref)

 {

     call System.Object.#ctor(this);

     return;