Translate AddressOf expressions correctly.

Fixes for problems when translating generic type parameters.

4 files changed, 186 insertions, 122 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index dd65a1f6..59b5d39f 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -318,20 +318,32 @@ namespace BytecodeTranslator
     /// <summary>

     /// If the expression's type is a generic parameter (either method or type),

     /// then this returns a "unboxed" expression, i.e., the value as a ref.

-    /// Otherwise it just translates the expression and skips the address-of

-    /// operation.

+    /// Otherwise it just translates the underlying expression and boxes it.

     /// </summary>

     public override void TraverseChildren(IAddressOf addressOf)

     {

       var t = addressOf.Expression.Type;

+      var boogieT = this.sink.CciTypeToBoogie(t);

+

       if (t is IGenericParameterReference) {

-        // then the expression will be represented by something of type Box

-        // but the address of it must be a ref, so do the conversion

-        this.Traverse(addressOf.Expression);

-        var e = this.TranslatedExpressions.Pop();

-        this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));

+        if (boogieT == this.sink.Heap.BoxType) {

+          // then the expression will be represented by something of type Box

+          // but the address of it must be a ref, so do the conversion

+          this.Traverse(addressOf.Expression);

+          var e = this.TranslatedExpressions.Pop();

+          this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));

+        } else {

+          this.Traverse(addressOf.Expression);

+        }

       } else {

         this.Traverse(addressOf.Expression);

+        var e = this.TranslatedExpressions.Pop();

+

+        Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type);

+        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

+        this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT));

+        this.TranslatedExpressions.Push(Bpl.Expr.Ident(a));

+

       }

     }

     #endregion

@@ -676,6 +688,16 @@ namespace BytecodeTranslator
       #region Create the 'this' argument for the function call

       thisExpr = null;

       if (thisArg != null) {

+

+        // Special case! thisArg is going to be an AddressOf expression if the receiver is a value-type

+        // But if the method's containing type is something that doesn't get translated as a Ref, then

+        // the AddressOf node should be ignored.

+        var addrOf = thisArg as IAddressOf;

+        var boogieType = this.sink.CciTypeToBoogie(methodToCall.ContainingType);

+        if (addrOf != null && boogieType != this.sink.Heap.RefType) {

+          thisArg = addrOf.Expression;

+        }

+

         this.Traverse(thisArg);

 

         var e = this.TranslatedExpressions.Pop();

@@ -700,10 +722,27 @@ namespace BytecodeTranslator
         if (penum.Current == null) {

           throw new TranslationException("More arguments than parameters in method call");

         }

-        this.Traverse(exp);

+

+        var expressionToTraverse = exp;

+        Bpl.Type boogieTypeOfExpression;

+

+        // Special case! exp can be an AddressOf expression if it is a value type being passed by reference.

+        // But since we pass reference parameters by in-out value passing, need to short-circuit the

+        // AddressOf node if the underlying type is not a Ref.

+        var addrOf = exp as IAddressOf;

+        if (addrOf != null) {

+          boogieTypeOfExpression = this.sink.CciTypeToBoogie(addrOf.Expression.Type);

+          if (boogieTypeOfExpression != this.sink.Heap.RefType) {

+            expressionToTraverse = addrOf.Expression;

+          }

+        }

+

+        boogieTypeOfExpression = this.sink.CciTypeToBoogie(expressionToTraverse.Type);

+        this.Traverse(expressionToTraverse);

+

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

-        if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter)

-          inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(exp.Type), e));

+        if (penum.Current.Type is IGenericParameterReference && this.sink.CciTypeToBoogie(penum.Current.Type) == this.sink.Heap.BoxType)

+          inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e));

         else

           inexpr.Add(e);

         if (penum.Current.IsByReference) {

@@ -711,7 +750,7 @@ namespace BytecodeTranslator
           if (unboxed == null) {

             throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");

           }

-          if (penum.Current.Type is IGenericParameter) {

+          if (penum.Current.Type is IGenericParameterReference) {

             var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);

             if (boogieType == this.sink.Heap.BoxType) {

               Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

@@ -747,8 +786,8 @@ namespace BytecodeTranslator
         if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

           Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);

-          if (resolvedMethod.Type is IGenericParameter) {

-            var boogieType = this.sink.CciTypeToBoogie(methodToCall.Type);

+          if (resolvedMethod.Type is IGenericParameterReference) {

+            var boogieType = this.sink.CciTypeToBoogie(resolvedMethod.Type);

             if (boogieType == this.sink.Heap.BoxType) {

               Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

               toBoxed[unboxed] = boxed;

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index bcf3ce0b..612854d9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -133,11 +133,12 @@ namespace BytecodeTranslator {
         return heap.RefType; // structs are kept on the heap with special rules about assignment

       else if (type.IsEnum)

         return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer

-      else if (type is IGenericParameter) {

-        var gp = type as IGenericParameter;

-        if (gp.MustBeReferenceType || gp.MustBeValueType)

+      else if (type is IGenericParameterReference) {

+        var gp = type.ResolvedType as IGenericParameter;

+        if (gp.MustBeReferenceType)// || gp.MustBeValueType)

           return heap.RefType;

-        foreach (var c in gp.Constraints){

+        foreach (var c in gp.Constraints) {

+          if (TypeHelper.TypesAreEquivalent(c, type.PlatformType.SystemValueType)) continue;

           return CciTypeToBoogie(c);

         }

         return heap.BoxType;

@@ -214,7 +215,7 @@ namespace BytecodeTranslator {
       typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

       var mangledName = String.Format("{0}_{1}", name, typeName);

       if (!localVarMap.TryGetValue(mangledName, out v)) {

-        v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));

+        v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, mangledName, t));

         localVarMap.Add(mangledName, v);

       }

       return v;

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 3284f217..f68465d1 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -499,38 +499,38 @@ const unique $real_literal_4_0: Real;
 

 implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)

 {

-  var d: Real;

-  var d2: Real;

+  var d_Real: Real;

+  var d2_Real: Real;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;

-    d := $real_literal_3_0;

+    d_Real := $real_literal_3_0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;

-    d2 := $real_literal_4_0;

+    d2_Real := $real_literal_4_0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

@@ -667,27 +667,33 @@ const unique F$RegressionTestInput.S.b: Field;
 

 implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

 {

-  var s: Ref;

+  var s_Ref: Ref;

   var $tmp0: Ref;

   var $tmp1: Ref;

+  var $tmp2: Ref;

+  var $tmp3: Ref;

   var $localExc: Ref;

   var $label: int;

 

     call $tmp0 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp0);

     assume $DynamicType($tmp0) == T$RegressionTestInput.S();

-    s := $tmp0;

+    s_Ref := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp1 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp1);

     assume $DynamicType($tmp1) == T$RegressionTestInput.S();

-    s := $tmp1;

+    s_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

-    assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;

+    call $tmp2 := Alloc();

+    $Heap := Write($Heap, $tmp2, $BoxField, Ref2Box(s_Ref));

+    assert Box2Int(Read($Heap, $tmp2, F$RegressionTestInput.S.x)) == 0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

-    assert !Box2Bool(Read($Heap, s, F$RegressionTestInput.S.b));

+    call $tmp3 := Alloc();

+    $Heap := Write($Heap, $tmp3, $BoxField, Ref2Box(s_Ref));

+    assert !Box2Bool(Read($Heap, $tmp3, F$RegressionTestInput.S.b));

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;

-    $result := s;

+    $result := s_Ref;

     return;

 }

 

@@ -700,14 +706,20 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu
 implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref)

 {

   var s: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     s := s$in;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;

-    $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));

+    call $tmp0 := Alloc();

+    $Heap := Write($Heap, $tmp0, $BoxField, Ref2Box(s));

+    $Heap := Write($Heap, $tmp0, F$RegressionTestInput.S.x, Int2Box(3));

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;

-    assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;

+    call $tmp1 := Alloc();

+    $Heap := Write($Heap, $tmp1, $BoxField, Ref2Box(s));

+    assert Box2Int(Read($Heap, $tmp1, F$RegressionTestInput.S.x)) == 3;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;

     $result := s;

     return;

@@ -761,9 +773,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

-  var s: Ref;

+  var s_Ref: Ref;

   var $tmp0: Ref;

-  var t: Ref;

+  var t_Ref: Ref;

   var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

@@ -771,21 +783,21 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;

     call $tmp0 := Alloc();

     assume $ArrayLength($tmp0) == 1 * 5;

-    s := $tmp0;

+    s_Ref := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;

-    $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

-    assert Box2Int($ArrayContents[s][0]) == 2;

+    assert Box2Int($ArrayContents[s_Ref][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

-    t := $tmp1;

+    t_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;

-    $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

-    assert Box2Int($ArrayContents[t][0]) == 1;

+    assert Box2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;

-    assert Box2Int($ArrayContents[s][0]) == 2;

+    assert Box2Int($ArrayContents[s_Ref][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;

     return;

 }

@@ -799,7 +811,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

   var $tmp0: Ref;

-  var t: Ref;

+  var t_Ref: Ref;

   var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

@@ -815,11 +827,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

-    t := $tmp1;

+    t_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;

-    $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

-    assert Box2Int($ArrayContents[t][0]) == 1;

+    assert Box2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;

     assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;

@@ -835,8 +847,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref,
 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var _loc0: Ref;

-  var _loc1: Ref;

+  var _loc0_Ref: Ref;

+  var _loc1_Ref: Ref;

   var $localExc: Ref;

   var $label: int;

 

@@ -846,9 +858,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;

-    _loc0 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

-    _loc1 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));

-    assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;

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

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

+    assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;

     return;

 }

@@ -1246,13 +1258,13 @@ procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result
 implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var CS$0$0000: Box;

+  var CS$0$0000_Box: Box;

   var $tmp0: Ref;

-  var __temp_2: Box;

-  var __temp_3: Box;

+  var __temp_2_Box: Box;

+  var __temp_3_Box: Box;

   var $tmp1: Box;

   var $tmp2: Box;

-  var y: Box;

+  var y_Box: Box;

   var $localExc: Ref;

   var $label: int;

 

@@ -1265,13 +1277,13 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;

-    CS$0$0000 := $DefaultBox;

+    CS$0$0000_Box := $DefaultBox;

     call $tmp0 := Alloc();

-    $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000));

+    $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000_Box));

     if ($tmp0 != null)

     {

-        CS$0$0000 := $DefaultBox;

-        __temp_2 := CS$0$0000;

+        CS$0$0000_Box := $DefaultBox;

+        __temp_2_Box := CS$0$0000_Box;

     }

     else

     {

@@ -1282,11 +1294,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
             return;

         }

 

-        __temp_3 := $tmp1;

-        __temp_2 := __temp_3;

+        __temp_3_Box := $tmp1;

+        __temp_2_Box := __temp_3_Box;

     }

 

-    y := __temp_2;

+    y_Box := __temp_2_Box;

     return;

 }

 

@@ -1414,15 +1426,15 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);
 implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var __temp_1: int;

-  var y: int;

+  var __temp_1_int: int;

+  var y_int: int;

   var $localExc: Ref;

   var $label: int;

 

     x := x$in;

-    __temp_1 := 5 / x;

+    __temp_1_int := 5 / x;

     x := 3;

-    y := __temp_1 + 3;

+    y_int := __temp_1_int + 3;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;

     if (x == 3)

     {

@@ -1431,11 +1443,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
     {

     }

 

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

+    assert (if x == 3 then y_int <= 8 else false);

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;

-    F$RegressionTestInput.Class0.StaticInt := y;

+    F$RegressionTestInput.Class0.StaticInt := y_int;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;

-    assert y == F$RegressionTestInput.Class0.StaticInt;

+    assert y_int == F$RegressionTestInput.Class0.StaticInt;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;

     return;

 }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 83cc1869..9484ee38 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -485,38 +485,38 @@ const unique $real_literal_4_0: Real;
 

 implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)

 {

-  var d: Real;

-  var d2: Real;

+  var d_Real: Real;

+  var d2_Real: Real;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;

-    d := $real_literal_3_0;

+    d_Real := $real_literal_3_0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;

-    d2 := $real_literal_4_0;

+    d2_Real := $real_literal_4_0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));

     if ($Exception != null)

     {

         return;

@@ -653,27 +653,33 @@ var F$RegressionTestInput.S.b: [Ref]bool;
 

 implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

 {

-  var s: Ref;

+  var s_Ref: Ref;

   var $tmp0: Ref;

   var $tmp1: Ref;

+  var $tmp2: Ref;

+  var $tmp3: Ref;

   var $localExc: Ref;

   var $label: int;

 

     call $tmp0 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp0);

     assume $DynamicType($tmp0) == T$RegressionTestInput.S();

-    s := $tmp0;

+    s_Ref := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp1 := Alloc();

     call RegressionTestInput.S.#default_ctor($tmp1);

     assume $DynamicType($tmp1) == T$RegressionTestInput.S();

-    s := $tmp1;

+    s_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

-    assert F$RegressionTestInput.S.x[s] == 0;

+    call $tmp2 := Alloc();

+    $BoxField[$tmp2] := Ref2Box(s_Ref);

+    assert F$RegressionTestInput.S.x[$tmp2] == 0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

-    assert !F$RegressionTestInput.S.b[s];

+    call $tmp3 := Alloc();

+    $BoxField[$tmp3] := Ref2Box(s_Ref);

+    assert !F$RegressionTestInput.S.b[$tmp3];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;

-    $result := s;

+    $result := s_Ref;

     return;

 }

 

@@ -686,14 +692,20 @@ procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInpu
 implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref)

 {

   var s: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     s := s$in;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;

-    F$RegressionTestInput.S.x[s] := 3;

+    call $tmp0 := Alloc();

+    $BoxField[$tmp0] := Ref2Box(s);

+    F$RegressionTestInput.S.x[$tmp0] := 3;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;

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

+    call $tmp1 := Alloc();

+    $BoxField[$tmp1] := Ref2Box(s);

+    assert F$RegressionTestInput.S.x[$tmp1] == 3;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;

     $result := s;

     return;

@@ -747,9 +759,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

-  var s: Ref;

+  var s_Ref: Ref;

   var $tmp0: Ref;

-  var t: Ref;

+  var t_Ref: Ref;

   var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

@@ -757,21 +769,21 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;

     call $tmp0 := Alloc();

     assume $ArrayLength($tmp0) == 1 * 5;

-    s := $tmp0;

+    s_Ref := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;

-    $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

-    assert Box2Int($ArrayContents[s][0]) == 2;

+    assert Box2Int($ArrayContents[s_Ref][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

-    t := $tmp1;

+    t_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;

-    $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

-    assert Box2Int($ArrayContents[t][0]) == 1;

+    assert Box2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;

-    assert Box2Int($ArrayContents[s][0]) == 2;

+    assert Box2Int($ArrayContents[s_Ref][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;

     return;

 }

@@ -785,7 +797,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

   var $tmp0: Ref;

-  var t: Ref;

+  var t_Ref: Ref;

   var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

@@ -801,11 +813,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;

     call $tmp1 := Alloc();

     assume $ArrayLength($tmp1) == 1 * 4;

-    t := $tmp1;

+    t_Ref := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;

-    $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

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

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

-    assert Box2Int($ArrayContents[t][0]) == 1;

+    assert Box2Int($ArrayContents[t_Ref][0]) == 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;

     assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;

@@ -821,8 +833,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref,
 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var _loc0: Ref;

-  var _loc1: Ref;

+  var _loc0_Ref: Ref;

+  var _loc1_Ref: Ref;

   var $localExc: Ref;

   var $label: int;

 

@@ -832,9 +844,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Box(43)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;

-    _loc0 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

-    _loc1 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];

-    assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;

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

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

+    assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;

     return;

 }

@@ -1232,13 +1244,13 @@ procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result
 implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var CS$0$0000: Box;

+  var CS$0$0000_Box: Box;

   var $tmp0: Ref;

-  var __temp_2: Box;

-  var __temp_3: Box;

+  var __temp_2_Box: Box;

+  var __temp_3_Box: Box;

   var $tmp1: Box;

   var $tmp2: Box;

-  var y: Box;

+  var y_Box: Box;

   var $localExc: Ref;

   var $label: int;

 

@@ -1251,13 +1263,13 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;

-    CS$0$0000 := $DefaultBox;

+    CS$0$0000_Box := $DefaultBox;

     call $tmp0 := Alloc();

-    $BoxField[$tmp0] := Box2Box(CS$0$0000);

+    $BoxField[$tmp0] := Box2Box(CS$0$0000_Box);

     if ($tmp0 != null)

     {

-        CS$0$0000 := $DefaultBox;

-        __temp_2 := CS$0$0000;

+        CS$0$0000_Box := $DefaultBox;

+        __temp_2_Box := CS$0$0000_Box;

     }

     else

     {

@@ -1268,11 +1280,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
             return;

         }

 

-        __temp_3 := $tmp1;

-        __temp_2 := __temp_3;

+        __temp_3_Box := $tmp1;

+        __temp_2_Box := __temp_3_Box;

     }

 

-    y := __temp_2;

+    y_Box := __temp_2_Box;

     return;

 }

 

@@ -1400,15 +1412,15 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);
 implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)

 {

   var x: int;

-  var __temp_1: int;

-  var y: int;

+  var __temp_1_int: int;

+  var y_int: int;

   var $localExc: Ref;

   var $label: int;

 

     x := x$in;

-    __temp_1 := 5 / x;

+    __temp_1_int := 5 / x;

     x := 3;

-    y := __temp_1 + 3;

+    y_int := __temp_1_int + 3;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;

     if (x == 3)

     {

@@ -1417,11 +1429,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
     {

     }

 

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

+    assert (if x == 3 then y_int <= 8 else false);

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;

-    F$RegressionTestInput.Class0.StaticInt := y;

+    F$RegressionTestInput.Class0.StaticInt := y_int;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;

-    assert y == F$RegressionTestInput.Class0.StaticInt;

+    assert y_int == F$RegressionTestInput.Class0.StaticInt;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;

     return;

 }