Automated merge with https://hg01.codeplex.com/boogie

7 files changed, 259 insertions, 165 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index aa4141e2..a9e1f9b0 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -326,27 +326,18 @@ namespace BytecodeTranslator
       var boogieT = this.sink.CciTypeToBoogie(t);

 

       if (t is IGenericParameterReference) {

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

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

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

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

         } else {

           this.Traverse(addressOf.Expression);

         }

       } else {

         this.Traverse(addressOf.Expression);

         return;

-        // TODO: Sometimes the value must still be boxed: for anythign that is not going to be represented as a Ref in Boogie!

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

@@ -481,8 +472,8 @@ namespace BytecodeTranslator
         e = lit;

       } else if (bplType == this.sink.Heap.RefType) {

         e = Bpl.Expr.Ident(this.sink.Heap.NullRef);

-      } else if (bplType == this.sink.Heap.BoxType) {

-        e = Bpl.Expr.Ident(this.sink.Heap.DefaultBox);

+      } else if (bplType == this.sink.Heap.UnionType) {

+        e = Bpl.Expr.Ident(this.sink.Heap.DefaultHeapValue);

       } else if (bplType == this.sink.Heap.RealType) {

         e = Bpl.Expr.Ident(this.sink.Heap.DefaultReal);

       } else {

@@ -554,7 +545,7 @@ namespace BytecodeTranslator
       List<Bpl.Expr> inexpr;

       List<Bpl.IdentifierExpr> outvars;

       Bpl.IdentifierExpr thisExpr;

-      Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+      Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

       var proc = TranslateArgumentsAndReturnProcedure(methodCallToken, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);

       string methodname = proc.Name;

       var translateAsFunctionCall = proc is Bpl.Function;

@@ -596,6 +587,7 @@ namespace BytecodeTranslator
             this.TranslatedExpressions.Push(callFunction);

             return;

           } else {

+            EmitLineDirective(methodCallToken);

             if (attrib != null)

               call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib);

             else

@@ -604,8 +596,20 @@ namespace BytecodeTranslator
           }

         }

 

-        foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

-          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+        foreach (KeyValuePair<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> kv in toBoxed) {

+          var lhs = kv.Key;

+          var tuple = kv.Value;

+          var rhs = tuple.Item1;

+          Bpl.Expr fromUnion;

+          if (tuple.Item2) {

+            // Since both structs and objects are represented by "Ref", need to make a distinction here.

+            // Review: Introduce an explicit type "Struct"?

+            fromUnion = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Struct), new Bpl.ExprSeq(rhs));

+          } else {

+            fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs);

+            //this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs)));

+          }

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));

         }

 

         Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

@@ -630,6 +634,17 @@ namespace BytecodeTranslator
       }

     }

 

+    private void EmitLineDirective(Bpl.IToken methodCallToken) {

+      var sloc = this.StmtTraverser.lastSourceLocation;

+      if (sloc != null) {

+        var fileName = sloc.Document.Location;

+        var lineNumber = sloc.StartLine;

+        var attrib = new Bpl.QKeyValue(methodCallToken, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);

+        attrib = new Bpl.QKeyValue(methodCallToken, "sourceFile", new List<object> { fileName }, attrib);

+        this.StmtTraverser.StmtBuilder.Add(new Bpl.AssertCmd(methodCallToken, Bpl.Expr.True, attrib));

+      }

+    }

+

     private Bpl.CallCmd translateAddRemoveCall(IMethodCall methodCall, IMethodDefinition resolvedMethod, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, bool isEventAdd) {

       Bpl.CallCmd call;

       var mName = resolvedMethod.Name.Value;

@@ -670,6 +685,7 @@ namespace BytecodeTranslator
       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));

 

       // Second, generate the call to the appropriate ctor

+      EmitLineDirective(methodCallToken);

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));

 

       // Generate an assumption about the dynamic type of the just allocated object

@@ -684,7 +700,7 @@ namespace BytecodeTranslator
     }

 

     // REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression?

-    protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {

+    protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toUnioned) {

       inexpr = new List<Bpl.Expr>();

       outvars = new List<Bpl.IdentifierExpr>();

 

@@ -718,7 +734,7 @@ namespace BytecodeTranslator
       }

       #endregion

 

-      toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();

+      toUnioned = new Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>>();

       IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

       foreach (IExpression exp in arguments) {

@@ -755,9 +771,16 @@ namespace BytecodeTranslator
           e = bplLocal;

         }

 

-        if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.BoxType)

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

-        else {

+        if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.UnionType) {

+          if (TranslationHelper.IsStruct(expressionToTraverse.Type)) {

+            // Since both structs and objects are represented by "Ref", need to make a distinction here.

+            // Review: Introduce an explicit type "Struct"?

+            var toUnion = new Bpl.NAryExpr(token, new Bpl.FunctionCall(this.sink.Heap.Struct2Union), new Bpl.ExprSeq(e));

+            inexpr.Add(toUnion);

+          } else {

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

+          }

+        } else {

           inexpr.Add(e);

         }

         if (penum.Current.IsByReference) {

@@ -767,9 +790,9 @@ namespace BytecodeTranslator
           }

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

-              toBoxed[unboxed] = boxed;

+            if (boogieType == this.sink.Heap.UnionType) {

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

+              toUnioned[unboxed] = Tuple.Create(boxed,false);

               outvars.Add(boxed);

             } else {

               outvars.Add(unboxed);

@@ -800,20 +823,20 @@ namespace BytecodeTranslator
       if (!translateAsFunctionCall) {

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

+          Bpl.IdentifierExpr unUnioned = new Bpl.IdentifierExpr(token, v);

           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;

-              outvars.Add(boxed);

+            if (boogieType == this.sink.Heap.UnionType) {

+              Bpl.IdentifierExpr unioned = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.UnionType));

+              toUnioned[unUnioned] = Tuple.Create(unioned, TranslationHelper.IsStruct(methodToCall.ResolvedMethod.Type.ResolvedType));

+              outvars.Add(unioned);

             } else {

-              outvars.Add(unboxed);

+              outvars.Add(unUnioned);

             }

           } else {

-            outvars.Add(unboxed);

+            outvars.Add(unUnioned);

           }

-          TranslatedExpressions.Push(unboxed);

+          TranslatedExpressions.Push(unUnioned);

         }

       }

 

@@ -882,6 +905,8 @@ namespace BytecodeTranslator
       }

       Bpl.Cmd cmd;

 

+      EmitLineDirective(tok);

+

       var/*?*/ local = container as ILocalDefinition;

       if (local != null) {

         Contract.Assume(instance == null);

@@ -1025,9 +1050,12 @@ namespace BytecodeTranslator
         List<Bpl.Expr> inexpr;

         List<Bpl.IdentifierExpr> outvars;

         Bpl.IdentifierExpr thisExpr;

-        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+        Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

         var proc = TranslateArgumentsAndReturnProcedure(token, ctor, resolvedMethod, null, createObjectInstance.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);

         inexpr.Insert(0, Bpl.Expr.Ident(a));

+

+        EmitLineDirective(token);

+

         this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc.Name, inexpr, outvars));

 

         // Generate an assumption about the dynamic type of the just allocated object

@@ -1574,7 +1602,8 @@ namespace BytecodeTranslator
       this.Traverse(conversion.ValueToConvert);

       var boogieTypeOfValue = this.sink.CciTypeToBoogie(conversion.ValueToConvert.Type);

       var boogieTypeToBeConvertedTo = this.sink.CciTypeToBoogie(conversion.TypeAfterConversion);

-      if (boogieTypeOfValue == boogieTypeToBeConvertedTo) {

+      if (boogieTypeOfValue == boogieTypeToBeConvertedTo && !TranslationHelper.IsStruct(conversion.ValueToConvert.Type)

+        && !TranslationHelper.IsStruct(conversion.TypeAfterConversion)) {

         // then this conversion is a nop, just ignore it

         return;

       }

@@ -1584,20 +1613,44 @@ namespace BytecodeTranslator
 

       var exp = TranslatedExpressions.Pop();

 

+      if (boogieTypeOfValue == this.sink.Heap.UnionType && boogieTypeToBeConvertedTo != this.sink.Heap.RefType) {

+        var e = this.sink.Heap.FromUnion(tok, boogieTypeToBeConvertedTo, exp);

+        TranslatedExpressions.Push(e);

+        return;

+      }

+      if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) {

+        Bpl.Expr e;

+        if (boogieTypeOfValue == this.sink.Heap.RefType)

+          e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Union), new Bpl.ExprSeq(exp));

+        else

+          e = this.sink.Heap.ToUnion(tok, boogieTypeOfValue, exp);

+        TranslatedExpressions.Push(e);

+        return;

+      }

+

+      if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType &&

+        TranslationHelper.IsStruct(conversion.TypeAfterConversion) &&

+        boogieTypeOfValue == this.sink.Heap.RefType) {

+        // REVIEW: This also applies to conversions from one struct type to another!

+        var e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Struct), new Bpl.ExprSeq(exp));

+        TranslatedExpressions.Push(e);

+        return;

+      }

+

       if (boogieTypeToBeConvertedTo == Bpl.Type.Bool) {

         Bpl.Expr expr;

         if (boogieTypeOfValue == Bpl.Type.Int) {

           expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0));

         }

         else if (boogieTypeOfValue == this.sink.Heap.RefType) {

-          expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Bool), new Bpl.ExprSeq(exp));

         }

         else if (boogieTypeOfValue == this.sink.Heap.RealType) {

           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp));

           expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, expr, Bpl.Expr.Literal(0));

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Bool), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = this.sink.Heap.FromUnion(tok, Bpl.Type.Bool, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1612,13 +1665,13 @@ namespace BytecodeTranslator
           expr = new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(exp, Bpl.Expr.Literal(1), Bpl.Expr.Literal(0)));

         }

         else if (boogieTypeOfValue == this.sink.Heap.RefType) {

-          expr = this.sink.Heap.ReadHeap(exp, Bpl.Expr.Ident(this.sink.Heap.BoxField), AccessType.Heap, Bpl.Type.Int);

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Int), new Bpl.ExprSeq(exp));

         }

         else if (boogieTypeOfValue == this.sink.Heap.RealType) {

           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp));

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Int), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = this.sink.Heap.FromUnion(Bpl.Token.NoToken, Bpl.Type.Int, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1628,9 +1681,32 @@ namespace BytecodeTranslator
       }

 

       if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType) {

+        // var a = BoxFromXXX(exp);

         Bpl.Variable a = this.sink.CreateFreshLocal(conversion.TypeAfterConversion);

-        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), exp, AccessType.Heap, boogieTypeOfValue));

+        Bpl.Procedure boxOperator;

+        if (boogieTypeOfValue == Bpl.Type.Bool)

+          boxOperator = this.sink.Heap.BoxFromBool;

+        else if (boogieTypeOfValue == Bpl.Type.Int)

+          boxOperator = this.sink.Heap.BoxFromInt;

+        else if (boogieTypeOfValue == this.sink.Heap.RealType)

+          boxOperator = this.sink.Heap.BoxFromReal;

+        else if (TranslationHelper.IsStruct(conversion.ValueToConvert.Type)) {

+          // Boxing a struct implicitly makes a copy of the struct

+          var typeOfValue = conversion.ValueToConvert.Type;

+          var proc = this.sink.FindOrCreateProcedureForStructCopy(typeOfValue);

+          var bplLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(typeOfValue));

+          var cmd = new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { exp, }, new List<Bpl.IdentifierExpr> { bplLocal, });

+          this.StmtTraverser.StmtBuilder.Add(cmd);

+          exp = bplLocal;

+          boxOperator = this.sink.Heap.BoxFromStruct;

+        }  else {

+          if (boogieTypeOfValue != this.sink.Heap.UnionType)

+            throw new NotImplementedException(msg);

+          boxOperator = this.sink.Heap.BoxFromUnion;

+        }

+        var name = boxOperator.Name;

+

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

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

         return;

       }

@@ -1645,10 +1721,10 @@ namespace BytecodeTranslator
           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Int2Real), new Bpl.ExprSeq(exp));

         }

         else if (boogieTypeOfValue == this.sink.Heap.RefType) {

-          expr = this.sink.Heap.ReadHeap(exp, Bpl.Expr.Ident(this.sink.Heap.BoxField), AccessType.Heap, this.sink.Heap.RealType);

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Real), new Bpl.ExprSeq(exp));

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Real), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = this.sink.Heap.FromUnion(tok, this.sink.Heap.RealType, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1657,27 +1733,27 @@ namespace BytecodeTranslator
         return;

       }

       

-      if (boogieTypeToBeConvertedTo == this.sink.Heap.BoxType) {

-        Bpl.Function func;

-        if (boogieTypeOfValue == Bpl.Type.Bool) {

-          func = this.sink.Heap.Bool2Box;

-        }

-        else if (boogieTypeOfValue == Bpl.Type.Int) {

-          func = this.sink.Heap.Int2Box;

-        }

-        else if (boogieTypeOfValue == this.sink.Heap.RefType) {

-          func = this.sink.Heap.Ref2Box;

-        }

-        else if (boogieTypeOfValue == this.sink.Heap.RealType) {

-          func = this.sink.Heap.Real2Box;

-        }

-        else {

-          throw new NotImplementedException(msg);

-        }

-        var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp));

-        TranslatedExpressions.Push(boxExpr);

-        return;

-      }

+      //if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) {

+      //  Bpl.Function func;

+      //  if (boogieTypeOfValue == Bpl.Type.Bool) {

+      //    func = this.sink.Heap.Bool2Union;

+      //  }

+      //  else if (boogieTypeOfValue == Bpl.Type.Int) {

+      //    func = this.sink.Heap.Int2Union;

+      //  }

+      //  else if (boogieTypeOfValue == this.sink.Heap.RefType) {

+      //    func = this.sink.Heap.Ref2Union;

+      //  }

+      //  else if (boogieTypeOfValue == this.sink.Heap.RealType) {

+      //    func = this.sink.Heap.Real2Union;

+      //  }

+      //  else {

+      //    throw new NotImplementedException(msg);

+      //  }

+      //  var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp));

+      //  TranslatedExpressions.Push(boxExpr);

+      //  return;

+      //}

     }

 

     public override void TraverseChildren(IOnesComplement onesComplement) {

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index abc3068d..aaed79e4 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -29,15 +29,6 @@ namespace BytecodeTranslator {
   /// </summary>

   public class SplitFieldsHeap : Heap {

 

-    #region "Boxing" as done in the CLR

-    /// <summary>

-    /// Used to represent "boxing" as it is done in the CLR.

-    /// </summary>

-    [RepresentationFor("$BoxField", "var $BoxField: [Ref]Box;")]

-    private Bpl.GlobalVariable boxField = null;

-    public override Bpl.Variable BoxField { get { return boxField; } }

-    #endregion

-

     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

@@ -52,7 +43,7 @@ namespace BytecodeTranslator {
       string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

-        this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

+        this.UnionType = new Bpl.CtorType(this.UnionTypeDecl.tok, this.UnionTypeDecl, new Bpl.TypeSeq());

         this.DelegateType = new Bpl.CtorType(this.DelegateTypeDecl.tok, this.DelegateTypeDecl, new Bpl.TypeSeq());

         this.DelegateMultisetType = new Bpl.TypeSynonymAnnotation(this.DelegateMultisetTypeDecl.tok, this.DelegateMultisetTypeDecl, new Bpl.TypeSeq());

         this.FieldType = new Bpl.CtorType(this.FieldTypeDecl.tok, this.FieldTypeDecl, new Bpl.TypeSeq());

@@ -122,13 +113,10 @@ namespace BytecodeTranslator {
       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr;

         Debug.Assert(field != null);

-        if (field.Decl == this.BoxField)

-          return Unbox(f.tok, unboxType, Bpl.Expr.Select(field, o));

-        else

-          return Bpl.Expr.Select(field, o);

+        return Bpl.Expr.Select(field, o);

       }

       else

-        return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));

+        return FromUnion(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));

     }

 

     /// <summary>

@@ -140,13 +128,10 @@ namespace BytecodeTranslator {
       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr;

         Debug.Assert(field != null);

-        if (field.Decl == this.BoxField)

-          return Bpl.Cmd.MapAssign(tok, field, o, Box(tok, boxType, value));

-        else

-          return Bpl.Cmd.MapAssign(tok, field, o, value);

+        return Bpl.Cmd.MapAssign(tok, field, o, value);

       }

       else {

-        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value))));

+        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, ToUnion(f.tok, boxType, value))));

       }

     }

 

@@ -159,31 +144,22 @@ namespace BytecodeTranslator {
   /// </summary>

   public class GeneralHeap : Heap {

 

-    #region "Boxing" as done in the CLR

-    /// <summary>

-    /// Used to represent "boxing" as it is done in the CLR.

-    /// </summary>

-    [RepresentationFor("$BoxField", "const unique $BoxField: Field;")]

-    private Bpl.Constant boxField = null;

-    public override Bpl.Variable BoxField { get { return boxField; } }

-    #endregion

-

     #region Fields

 

     [RepresentationFor("$Heap", "var $Heap: HeapType;", true)]

     private Bpl.Variable HeapVariable = null;

     

-    [RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:Ref, f:Field): Box { H[o][f] }")]

+    [RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:Ref, f:Field): Union { H[o][f] }")]

     private Bpl.Function Read = null;

 

-    [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:Ref, f:Field, v:Box): HeapType { H[o := H[o][f := v]] }")]

+    [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:Ref, f:Field, v:Union): HeapType { H[o := H[o][f := v]] }")]

     private Bpl.Function Write = null;

 

     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

     private readonly string InitialPreludeText =

-      @"type HeapType = [Ref][Field]Box;

+      @"type HeapType = [Ref][Field]Union;

 

 ";

     private Sink sink;

@@ -197,7 +173,7 @@ namespace BytecodeTranslator {
       string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

-        this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

+        this.UnionType = new Bpl.CtorType(this.UnionTypeDecl.tok, this.UnionTypeDecl, new Bpl.TypeSeq());

         this.DelegateType = new Bpl.CtorType(this.DelegateTypeDecl.tok, this.DelegateTypeDecl, new Bpl.TypeSeq());

         this.DelegateMultisetType = new Bpl.TypeSynonymAnnotation(this.DelegateMultisetTypeDecl.tok, this.DelegateMultisetTypeDecl, new Bpl.TypeSeq());

         this.FieldType = new Bpl.CtorType(this.FieldTypeDecl.tok, this.FieldTypeDecl, new Bpl.TypeSeq());

@@ -268,7 +244,7 @@ namespace BytecodeTranslator {
         callRead = Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f);

 

       // wrap it in the right conversion function

-      var callExpr = Unbox(f.tok, unboxType, callRead);

+      var callExpr = FromUnion(f.tok, unboxType, callRead);

       return callExpr;

     }

 

@@ -281,7 +257,7 @@ namespace BytecodeTranslator {
 

       Bpl.IdentifierExpr h;

       Bpl.NAryExpr callWrite;

-      var callConversion = Box(f.tok, boxType, value);

+      var callConversion = ToUnion(f.tok, boxType, value);

 

       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         h = Bpl.Expr.Ident(HeapVariable);

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 6553efba..f4a04b37 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -66,15 +66,13 @@ namespace BytecodeTranslator {
 

   public abstract class Heap : HeapFactory, IHeap

   {

-    [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]

+    [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Union;")]

     public Bpl.Variable ArrayContentsVariable = null;

     [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]

     public Bpl.Function ArrayLengthFunction = null;

 

     public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);

 

-    public abstract Bpl.Variable BoxField { get; }

-

     #region Boogie Types

 

     [RepresentationFor("Delegate", "type {:datatype} Delegate;")]

@@ -101,12 +99,12 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl FieldTypeDecl = null;

     public Bpl.CtorType FieldType;

 

-    [RepresentationFor("Box", "type Box;")]

-    public Bpl.TypeCtorDecl BoxTypeDecl = null;

-    public Bpl.CtorType BoxType;

+    [RepresentationFor("Union", "type {:datatype} Union;")]

+    public Bpl.TypeCtorDecl UnionTypeDecl = null;

+    public Bpl.CtorType UnionType;

 

-    [RepresentationFor("$DefaultBox", "const unique $DefaultBox : Box;")]

-    public Bpl.Constant DefaultBox;

+    [RepresentationFor("$DefaultHeapValue", "const unique $DefaultHeapValue : Union;")]

+    public Bpl.Constant DefaultHeapValue;

 

     [RepresentationFor("Ref", "type Ref;")]

     public Bpl.TypeCtorDecl RefTypeDecl = null;

@@ -126,49 +124,92 @@ namespace BytecodeTranslator {
 

     #endregion

 

+    #region CLR Boxing

+

+    [RepresentationFor("$BoxFromBool", "procedure $BoxFromBool(b: bool) returns (r: Ref) free ensures $BoxedValue(r) == Bool2Union(b); { call r := Alloc(); assume $BoxedValue(r) == Bool2Union(b); }")]

+    public Bpl.Procedure BoxFromBool = null;

+

+    [RepresentationFor("$BoxFromInt", "procedure $BoxFromInt(i: int) returns (r: Ref) free ensures $BoxedValue(r) == Int2Union(i); { call r := Alloc(); assume $BoxedValue(r) == Int2Union(i); }")]

+    public Bpl.Procedure BoxFromInt = null;

+

+    [RepresentationFor("$BoxFromReal", "procedure $BoxFromReal(r: Real) returns (rf: Ref) free ensures $BoxedValue(rf) == Real2Union(r); { call rf := Alloc(); assume $BoxedValue(rf) == Real2Union(r); }")]

+    public Bpl.Procedure BoxFromReal = null;

+

+    [RepresentationFor("$BoxFromStruct", "procedure $BoxFromStruct(s: Ref) returns (r: Ref) free ensures $BoxedValue(r) == Struct2Union(s); { call r := Alloc(); assume $BoxedValue(r) == Struct2Union(s); }")]

+    public Bpl.Procedure BoxFromStruct = null;

+

+    [RepresentationFor("$BoxFromUnion", "procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) { if (is#Ref2Union(u)) { r := refValue#Ref2Union(u); } else { call r := Alloc(); assume $BoxedValue(r) == u; } }")]

+    public Bpl.Procedure BoxFromUnion = null;

+

+    [RepresentationFor("$BoxedValue", "function $BoxedValue(r: Ref): Union;")]

+    public Bpl.Function BoxedValue = null;

+

+    [RepresentationFor("$Unbox2Bool", "function $Unbox2Bool(r: Ref): (bool) { boolValue#Bool2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Bool = null;

+

+    [RepresentationFor("$Unbox2Int", "function $Unbox2Int(r: Ref): (int) { intValue#Int2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Int = null;

+

+    [RepresentationFor("$Unbox2Real", "function $Unbox2Real(r: Ref): (Real) { realValue#Real2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Real = null;

+

+    [RepresentationFor("$Unbox2Struct", "function $Unbox2Struct(r: Ref): (Ref) { structValue#Struct2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Struct = null;

+

+    [RepresentationFor("$Unbox2Union", "function $Unbox2Union(r: Ref): (Union) { $BoxedValue(r) }")]

+    public Bpl.Function Unbox2Union = null;

+

+    #endregion

+

     #region Conversions

 

     #region Heap values

 

-    [RepresentationFor("Box2Bool", "function Box2Bool(Box): bool;")]

-    public Bpl.Function Box2Bool = null;

+    [RepresentationFor("Union2Bool", "function Union2Bool(u: Union): (bool) { boolValue#Bool2Union(u) }")]

+    public Bpl.Function Union2Bool = null;

     

-    [RepresentationFor("Box2Int", "function Box2Int(Box): int;")]

-    public Bpl.Function Box2Int = null;

+    [RepresentationFor("Union2Int", "function Union2Int(u: Union): (int) { intValue#Int2Union(u) }")]

+    public Bpl.Function Union2Int = null;

     

-    [RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]

-    public Bpl.Function Box2Ref = null;

+    [RepresentationFor("Union2Ref", "function Union2Ref(u: Union): (Ref) { refValue#Ref2Union(u) }")]

+    public Bpl.Function Union2Ref = null;

+

+    [RepresentationFor("Union2Real", "function Union2Real(u: Union): (Real) { realValue#Real2Union(u) }")]

+    public Bpl.Function Union2Real = null;

 

-    [RepresentationFor("Box2Real", "function Box2Real(Box): Real;")]

-    public Bpl.Function Box2Real = null;

+    [RepresentationFor("Union2Struct", "function Union2Struct(u: Union): (Ref) { structValue#Struct2Union(u) }")]

+    public Bpl.Function Union2Struct = null;

 

-    [RepresentationFor("Bool2Box", "function Bool2Box(bool): Box;")]

-    public Bpl.Function Bool2Box = null;

+    [RepresentationFor("Bool2Union", "function {:constructor} Bool2Union(boolValue: bool): Union;")]

+    public Bpl.Function Bool2Union = null;

 

-    [RepresentationFor("Int2Box", "function Int2Box(int): Box;")]

-    public Bpl.Function Int2Box = null;

+    [RepresentationFor("Int2Union", "function {:constructor} Int2Union(intValue: int): Union;")]

+    public Bpl.Function Int2Union = null;

 

-    [RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]

-    public Bpl.Function Ref2Box = null;

+    [RepresentationFor("Ref2Union", "function {:constructor} Ref2Union(refValue: Ref): Union;")]

+    public Bpl.Function Ref2Union = null;

 

-    [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]

-    public Bpl.Function Real2Box = null;

+    [RepresentationFor("Real2Union", "function {:constructor} Real2Union(realValue: Real): Union;")]

+    public Bpl.Function Real2Union = null;

 

-    [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]

-    public Bpl.Function Box2Box = null;

+    [RepresentationFor("Struct2Union", "function {:constructor} Struct2Union(structValue: Ref): Union;")]

+    public Bpl.Function Struct2Union = null;

 

-    public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

+    [RepresentationFor("Union2Union", "function {:inline true} Union2Union(u: Union): Union { u }")]

+    public Bpl.Function Union2Union = null;

+

+    public Bpl.Expr ToUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

-        conversion = this.Bool2Box;

+        conversion = this.Bool2Union;

       else if (boogieType == Bpl.Type.Int)

-        conversion = this.Int2Box;

+        conversion = this.Int2Union;

       else if (boogieType == RefType)

-        conversion = this.Ref2Box;

+        conversion = this.Ref2Union;

       else if (boogieType == RealType)

-        conversion = this.Real2Box;

-      else if (boogieType == BoxType)

-        conversion = this.Box2Box;

+        conversion = this.Real2Union;

+      else if (boogieType == UnionType)

+        conversion = this.Union2Union;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

@@ -180,18 +221,18 @@ namespace BytecodeTranslator {
       return callConversion;

     }

 

-    public Bpl.Expr Unbox(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

+    public Bpl.Expr FromUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion = null;

       if (boogieType == Bpl.Type.Bool)

-        conversion = this.Box2Bool;

+        conversion = this.Union2Bool;

       else if (boogieType == Bpl.Type.Int)

-        conversion = this.Box2Int;

+        conversion = this.Union2Int;

       else if (boogieType == RefType)

-        conversion = this.Box2Ref;

+        conversion = this.Union2Ref;

       else if (boogieType == RealType)

-        conversion = this.Box2Real;

-      else if (boogieType == BoxType)

-        conversion = this.Box2Box;

+        conversion = this.Union2Real;

+      else if (boogieType == UnionType)

+        conversion = this.Union2Union;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

@@ -380,13 +421,9 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
   $result := $TypeOf($DynamicType(this));

 }

 

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

-

-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

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

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

+axiom Union2Int($DefaultHeapValue) == 0;

+axiom Union2Bool($DefaultHeapValue) == false;

+axiom Union2Ref($DefaultHeapValue) == null;

 

 function $ThreadDelegate(Ref) : Ref;

 

@@ -492,14 +529,14 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
   var enabledness: bool;

   $Exception:=null;

   enabledness := isControlEnabled[$this];

-  $result := Box2Ref(Bool2Box(enabledness));

+  $result := Union2Ref(Bool2Union(enabledness));

 }

 

 procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

 implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {

   var check: bool;

   $Exception:=null;

-  check := Box2Bool(Ref2Box(value$in));

+  check := Union2Bool(Ref2Union(value$in));

   isControlChecked[$this] := check;

 }

 

@@ -508,7 +545,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th
   var isChecked: bool;

   $Exception:=null;

   isChecked := isControlChecked[$this];

-  $result := Box2Ref(Bool2Box(isChecked));

+  $result := Union2Ref(Bool2Union(isChecked));

 }

 

 ";

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 761ecf7b..ff4a567b 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -565,11 +565,11 @@ namespace BytecodeTranslator {
         Bpl.Expr rexpr = Bpl.Expr.Ident(rvar);

         if (rtype == ltype) {

           // do nothing

-        } else if (ltype == sink.Heap.BoxType) {

-          rexpr = sink.Heap.Box(Bpl.Token.NoToken, rtype, rexpr);

+        } else if (ltype == sink.Heap.UnionType) {

+          rexpr = sink.Heap.ToUnion(Bpl.Token.NoToken, rtype, rexpr);

         }

-        else if (rtype == sink.Heap.BoxType) {

-          rexpr = sink.Heap.Unbox(Bpl.Token.NoToken, ltype, rexpr);

+        else if (rtype == sink.Heap.UnionType) {

+          rexpr = sink.Heap.FromUnion(Bpl.Token.NoToken, ltype, rexpr);

         }

         else {

           System.Diagnostics.Debug.Assert(false);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4499f11e..bc4e7524 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -144,7 +144,7 @@ namespace BytecodeTranslator {
           if (TypeHelper.TypesAreEquivalent(c, type.PlatformType.SystemValueType)) continue;

           return CciTypeToBoogie(c);

         }

-        return heap.BoxType;

+        return heap.UnionType;

       } else

         return heap.RefType;

     }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index aed72ccd..60fb8567 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -122,6 +122,8 @@ namespace BytecodeTranslator
           foreach (var sloc in slocs) {

             fileName = sloc.Document.Location;

             lineNumber = sloc.StartLine;

+

+            this.parent.lastSourceLocation = sloc;

             break;

           }

           if (fileName != null) {

@@ -237,6 +239,7 @@ namespace BytecodeTranslator
     }

 

     private static int counter = 0;

+    public IPrimarySourceLocation lastSourceLocation;

     internal int NextUniqueNumber() {

       return counter++;

     }

@@ -336,14 +339,16 @@ namespace BytecodeTranslator
       // then a struct value of type S is being assigned: "lhs := s"

       // model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying

       if (isStruct) {

-        var defaultValue = new DefaultValue() {

-          DefaultValueType = typ,

-          Locations = new List<ILocation>(localDeclarationStatement.Locations),

-          Type = typ,

-        };

-        var e2 = ExpressionFor(defaultValue);

-        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

-        if (structCopy) {

+        if (!structCopy) {

+          var defaultValue = new DefaultValue() {

+            DefaultValueType = typ,

+            Locations = new List<ILocation>(localDeclarationStatement.Locations),

+            Type = typ,

+          };

+          var e2 = ExpressionFor(defaultValue);

+          StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

+        } else 

+        /*if (structCopy) */{

           var proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

           e = ExpressionFor(initVal);

           StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, }, new List<Bpl.IdentifierExpr>{ boogieLocalExpr, }));

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index bd297451..73e882e0 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -140,7 +140,7 @@ namespace BytecodeTranslator {
         List<Bpl.Expr> inexpr;

         List<Bpl.IdentifierExpr> outvars;

         Bpl.IdentifierExpr thisExpr;

-        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+        Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

         var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);