whole bunch of bug fixes

5 files changed, 157 insertions, 247 deletions

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index e08da536..55f0cd46 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -29,28 +29,7 @@ namespace BytecodeTranslator {
 

       public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext)

         : base(sink, statementTraverser, contractContext) { }

-

-      /*

-      public override void Visit(IDivision division) {

-        this.Visit(division.LeftOperand);

-        this.Visit(division.RightOperand);

-        Bpl.Expr rexp = TranslatedExpressions.Pop();

-        Bpl.Expr lexp = TranslatedExpressions.Pop();

-

-        var tok = division.Token();

-

-        var loc = this.sink.CreateFreshLocal(division.RightOperand.Type);

-        var locExpr = Bpl.Expr.Ident(loc);

-        var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);

-        this.StmtTraverser.StmtBuilder.Add(storeLocal);

-

-//        Assertion fails if denominator is Real or something else than int

-//        var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, locExpr, Bpl.Expr.Literal(0)));

-//        this.StmtTraverser.StmtBuilder.Add(a);

-

-        TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, locExpr));

-      }

-       * */

+      

     }

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 23736b36..7edd62bf 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -591,7 +591,7 @@ namespace BytecodeTranslator
         }

         this.Visit(exp);

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

-        if (penum.Current.Type is IGenericTypeParameter)

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

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

         else

           inexpr.Add(e);

@@ -600,7 +600,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 IGenericTypeParameter) {

+          if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter) {

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

             toBoxed[unboxed] = boxed;

             outvars.Add(boxed);

@@ -631,7 +631,7 @@ 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 IGenericTypeParameter) {

+          if (resolvedMethod.Type is IGenericTypeParameter || resolvedMethod.Type is IGenericMethodParameter) {

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

             toBoxed[unboxed] = boxed;

             outvars.Add(boxed);

@@ -803,29 +803,40 @@ namespace BytecodeTranslator
 

       var a = this.sink.CreateFreshLocal(createObjectInstance.Type);

 

-      // First generate an Alloc() call

-      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

+      if (createObjectInstance.Type.TypeCode == PrimitiveTypeCode.IntPtr ||

+          createObjectInstance.Type.TypeCode == PrimitiveTypeCode.UIntPtr) {

+        List<Bpl.Expr> args = new List<Bpl.Expr>();

+        foreach (IExpression e in createObjectInstance.Arguments) {

+          this.Visit(e);

+          args.Add(TranslatedExpressions.Pop());

+        }

+        System.Diagnostics.Debug.Assert(args.Count == 1);

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(a), args[0]));

+      }

+      else {

+        // First generate an Alloc() call

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

 

-      // Second, generate the call to the appropriate ctor

+        // Second, generate the call to the appropriate ctor

 

-      List<Bpl.Expr> inexpr;

-      List<Bpl.IdentifierExpr> outvars;

-      Bpl.IdentifierExpr thisExpr;

-      Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> 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));

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

-

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

-      this.StmtTraverser.StmtBuilder.Add(

-          new Bpl.AssumeCmd(token,

-            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

-            this.sink.Heap.DynamicType(Bpl.Expr.Ident(a)),

-            this.sink.FindOrCreateType(createObjectInstance.Type)

-            )

-            )

-          );

-      

+        List<Bpl.Expr> inexpr;

+        List<Bpl.IdentifierExpr> outvars;

+        Bpl.IdentifierExpr thisExpr;

+        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> 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));

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

+

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

+        this.StmtTraverser.StmtBuilder.Add(

+            new Bpl.AssumeCmd(token,

+              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+              this.sink.Heap.DynamicType(Bpl.Expr.Ident(a)),

+              this.sink.FindOrCreateType(createObjectInstance.Type)

+              )

+              )

+            );

+      }

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

     }

 

@@ -906,11 +917,17 @@ namespace BytecodeTranslator
       base.Visit(bitwiseAnd);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      var e = new Bpl.NAryExpr(

-        bitwiseAnd.Token(),

-        new Bpl.FunctionCall(this.sink.Heap.BitwiseAnd),

-        new Bpl.ExprSeq(lexp, rexp)

-        );

+      Bpl.Expr e;

+      if (bitwiseAnd.Type.TypeCode == PrimitiveTypeCode.Boolean) {

+        e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, lexp, rexp);

+      }

+      else {

+        e = new Bpl.NAryExpr(

+          bitwiseAnd.Token(),

+          new Bpl.FunctionCall(this.sink.Heap.BitwiseAnd),

+          new Bpl.ExprSeq(lexp, rexp)

+          );

+      }

       TranslatedExpressions.Push(e);

     }

 

@@ -918,11 +935,17 @@ namespace BytecodeTranslator
       base.Visit(bitwiseOr);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      var e = new Bpl.NAryExpr(

-        bitwiseOr.Token(),

-        new Bpl.FunctionCall(this.sink.Heap.BitwiseOr),

-        new Bpl.ExprSeq(lexp, rexp)

-        );

+      Bpl.Expr e;

+      if (bitwiseOr.Type.TypeCode == PrimitiveTypeCode.Boolean) {

+        e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, lexp, rexp);

+      }

+      else {

+        e = new Bpl.NAryExpr(

+          bitwiseOr.Token(),

+          new Bpl.FunctionCall(this.sink.Heap.BitwiseOr),

+          new Bpl.ExprSeq(lexp, rexp)

+          );

+      }

       TranslatedExpressions.Push(e);

     }

 

@@ -1265,189 +1288,100 @@ namespace BytecodeTranslator
 

       var exp = TranslatedExpressions.Pop();

 

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

-

-          break;

-

-        case Bpl.Type.Int:

-

-          break;

-

-        case this.sink.Heap.RefType:

-

-          break;

-

-        case this.sink.Heap.RealType:

-

-          break;

-

-        case this.sink.Heap.BoxType:

-

-          break;

-

-        default:

-          throw NotImplementedException(msg);

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

+        }

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

+          throw new NotImplementedException(msg);

+        }

+        TranslatedExpressions.Push(expr);

+        return;

       }

 

+      if (boogieTypeToBeConvertedTo == Bpl.Type.Int) {

+        Bpl.Expr expr;

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

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

+        }

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

+          throw new NotImplementedException(msg);

+        }

+        TranslatedExpressions.Push(expr);

+        return;

+      }

 

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

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

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

+        return;

+      }

 

-      if (conversion.TypeAfterConversion.IsEnum) {

-

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

+        Bpl.Expr expr;

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

+          expr = new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(exp, Bpl.Expr.Literal(1), Bpl.Expr.Literal(0)));

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

+        }

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

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

+        }

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

+          throw new NotImplementedException(msg);

+        }

+        TranslatedExpressions.Push(expr);

+        return;

       }

-      if (conversion.TypeAfterConversion is IGenericTypeParameter || conversion.TypeAfterConversion is IGenericMethodParameter) {

+      

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

         Bpl.Function func;

-        if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Boolean) {

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

           func = this.sink.Heap.Bool2Box;

         }

-        else if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {

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

           func = this.sink.Heap.Int2Box;

         }

-        else if (conversion.ValueToConvert.Type.IsEnum) {

-          func = this.sink.Heap.Int2Box;

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

+          func = this.sink.Heap.Ref2Box;

         }

-        else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float32 ||

-                 conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float64) {

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

           func = this.sink.Heap.Real2Box;

         }

-        else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.NotPrimitive) {

-          func = this.sink.Heap.Ref2Box;

-        } else {

+        else {

           throw new NotImplementedException(msg);

         }

-        var boxExpr = new Bpl.NAryExpr(

-          conversion.Token(),

-          new Bpl.FunctionCall(func),

-          new Bpl.ExprSeq(exp)

-          );

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

         TranslatedExpressions.Push(boxExpr);

         return;

       }

-

-      switch (conversion.TypeAfterConversion.TypeCode) {

-        case PrimitiveTypeCode.Int16:

-        case PrimitiveTypeCode.Int32:

-        case PrimitiveTypeCode.Int64:

-        case PrimitiveTypeCode.Int8:

-        case PrimitiveTypeCode.UInt16:

-        case PrimitiveTypeCode.UInt32:

-        case PrimitiveTypeCode.UInt64:

-        case PrimitiveTypeCode.UInt8:

-          switch (conversion.ValueToConvert.Type.TypeCode) {

-            case PrimitiveTypeCode.Boolean:

-              TranslatedExpressions.Push(

-                new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(exp, Bpl.Expr.Literal(1), Bpl.Expr.Literal(0)))

-                );

-              return;

-            case PrimitiveTypeCode.IntPtr:

-              // just ignore the conversion. REVIEW: is that the right thing to do?

-              this.TranslatedExpressions.Push(exp);

-              return;

-            case PrimitiveTypeCode.Float32:

-            case PrimitiveTypeCode.Float64: {

-                var convExpr = new Bpl.NAryExpr(

-                conversion.Token(),

-                new Bpl.FunctionCall(this.sink.Heap.Real2Int),

-                new Bpl.ExprSeq(exp,

-                  this.sink.FindOrCreateType(conversion.ValueToConvert.Type),

-                  this.sink.FindOrCreateType(conversion.TypeAfterConversion)

-                  )

-                );

-                TranslatedExpressions.Push(convExpr);

-                return;

-              }

-

-            case PrimitiveTypeCode.NotPrimitive:

-                TranslatedExpressions.Push(new Bpl.NAryExpr(

-                  conversion.Token(),

-                  new Bpl.FunctionCall(this.sink.Heap.Ref2Int),

-                  new Bpl.ExprSeq(exp,

-                    this.sink.FindOrCreateType(conversion.ValueToConvert.Type),

-                    this.sink.FindOrCreateType(conversion.TypeAfterConversion)

-                    )

-                    ));

-                    return;

-

-            default:

-              throw new NotImplementedException(msg);

-          }

-        case PrimitiveTypeCode.UIntPtr:

-        case PrimitiveTypeCode.IntPtr:

-          // just ignore the conversion. REVIEW: is that the right thing to do?

-          this.TranslatedExpressions.Push(exp);

-          return;

-

-        case PrimitiveTypeCode.Boolean:

-          if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {

-              TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0)));

-              return;

-          } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.NotPrimitive) {

-            TranslatedExpressions.Push(new Bpl.NAryExpr(

-              conversion.Token(),

-              new Bpl.FunctionCall(this.sink.Heap.Ref2Bool),

-              new Bpl.ExprSeq(exp,

-                this.sink.FindOrCreateType(conversion.ValueToConvert.Type),

-                this.sink.FindOrCreateType(conversion.TypeAfterConversion)

-                )

-                ));

-            return;

-          } else {

-            throw new NotImplementedException(msg);

-          }

-        case PrimitiveTypeCode.NotPrimitive:

-          Bpl.Function func;

-          if (conversion.ValueToConvert.Type is IGenericTypeParameter || conversion.ValueToConvert.Type is IGenericMethodParameter) {

-            func = this.sink.Heap.Box2Ref;

-          } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Boolean) {

-            func = this.sink.Heap.Bool2Ref;

-          } else if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {

-            func = this.sink.Heap.Int2Ref;

-          } else if (conversion.ValueToConvert.Type.IsEnum) {

-            func = this.sink.Heap.Int2Ref;

-          }

-          else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float32 ||

-                   conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float64) {

-            func = this.sink.Heap.Real2Ref;

-          }

-          else {

-            throw new NotImplementedException(msg);

-          }

-          var boxExpr = new Bpl.NAryExpr(

-            conversion.Token(),

-            new Bpl.FunctionCall(func),

-            new Bpl.ExprSeq(exp)

-            );

-            TranslatedExpressions.Push(boxExpr);

-            return;

-        case PrimitiveTypeCode.Float32:

-        case PrimitiveTypeCode.Float64:

-          if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {

-            var convExpr = new Bpl.NAryExpr(

-              conversion.Token(),

-              new Bpl.FunctionCall(this.sink.Heap.Int2Real),

-              new Bpl.ExprSeq(exp,

-                this.sink.FindOrCreateType(conversion.ValueToConvert.Type),

-                this.sink.FindOrCreateType(conversion.TypeAfterConversion)

-                )

-                );

-            TranslatedExpressions.Push(convExpr);

-            return;

-          } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.NotPrimitive) {

-            var convExpr = new Bpl.NAryExpr(

-              conversion.Token(),

-              new Bpl.FunctionCall(this.sink.Heap.Ref2Real),

-              new Bpl.ExprSeq(exp,

-                this.sink.FindOrCreateType(conversion.ValueToConvert.Type),

-                this.sink.FindOrCreateType(conversion.TypeAfterConversion)

-                )

-                );

-            TranslatedExpressions.Push(convExpr);

-            return;

-          } else {

-            throw new NotImplementedException(msg);

-          }

-        default:

-          throw new NotImplementedException(msg);

-      }

     }

 

     public override void Visit(IOnesComplement onesComplement) {

@@ -1575,7 +1509,7 @@ namespace BytecodeTranslator
 

         var loc = new LocalDefinition() {

           Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),

-          Type = boundExpression.Type,

+          Type = e.Type,

         };

         var locDecl = new LocalDeclarationStatement() {

           InitialValue = e,

@@ -1609,7 +1543,7 @@ namespace BytecodeTranslator
 

         var loc = new LocalDefinition() {

           Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),

-          Type = arrayIndexer.IndexedObject.Type

+          Type = e.Type

         };

         var locDecl = new LocalDeclarationStatement() {

           InitialValue = e,

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 759f7b31..6de7cb95 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -108,24 +108,24 @@ namespace BytecodeTranslator {
 

     #region Heap values

 

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

-    public Bpl.Function Box2Int = null;

-

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

     public Bpl.Function Box2Bool = null;

-

+    

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

+    public Bpl.Function Box2Int = null;

+    

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

     public Bpl.Function Box2Ref = null;

 

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

     public Bpl.Function Box2Real = null;

 

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

-    public Bpl.Function Int2Box = null;

-

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

     public Bpl.Function Bool2Box = null;

 

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

+    public Bpl.Function Int2Box = null;

+

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

     public Bpl.Function Ref2Box = null;

 

@@ -188,21 +188,15 @@ namespace BytecodeTranslator {
     /// <summary>

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

     /// </summary>

-    [RepresentationFor("Int2Ref", "function Int2Ref(int): Ref;")]

-    public Bpl.Function Int2Ref = null;

-    [RepresentationFor("Bool2Ref", "function Bool2Ref(bool): Ref;")]

-    public Bpl.Function Bool2Ref = null;

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

+    public Bpl.Constant BoxField = null;

     #endregion

 

     #region Real number conversions

-    [RepresentationFor("Int2Real", "function Int2Real(int, Type, Type): Real;")]

+    [RepresentationFor("Int2Real", "function Int2Real(int): Real;")]

     public Bpl.Function Int2Real = null;

-    [RepresentationFor("Real2Int", "function Real2Int(Real, Type, Type): int;")]

+    [RepresentationFor("Real2Int", "function Real2Int(Real): int;")]

     public Bpl.Function Real2Int = null;

-    [RepresentationFor("Ref2Real", "function Ref2Real(Ref, Type, Type): Real;")]

-    public Bpl.Function Ref2Real = null;

-    [RepresentationFor("Real2Ref", "function Real2Ref(Real): Ref;")]

-    public Bpl.Function Real2Ref = null;

     #endregion

 

     #region Real number operations

@@ -235,13 +229,6 @@ namespace BytecodeTranslator {
     public Bpl.Function BitwiseNegation = null;

     #endregion

 

-    #region Ref conversions

-    [RepresentationFor("Ref2Int", "function Ref2Int(Ref, Type, Type): int;")]

-    public Bpl.Function Ref2Int = null;

-    [RepresentationFor("Ref2Bool", "function Ref2Bool(Ref, Type, Type): bool;")]

-    public Bpl.Function Ref2Bool = null;

-    #endregion

-

     #endregion

 

     /// <summary>

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 7d04401b..45206ddb 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -277,6 +277,11 @@ namespace BytecodeTranslator {
       this.sink.BeginMethod(method);

       var decl = procInfo.Decl;

       var proc = decl as Bpl.Procedure;

+

+      if (proc.Name.StartsWith("Microsoft.Devices.Camera.$get_AvailableResolutions")) {

+

+      }

+

       var formalMap = procInfo.FormalMap;

 

       try {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index da285ee0..c19bc173 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -116,6 +116,8 @@ namespace BytecodeTranslator {
     public Bpl.Type CciTypeToBoogie(ITypeReference type) {

       if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))

         return Bpl.Type.Bool;

+      else if (type.TypeCode == PrimitiveTypeCode.UIntPtr || type.TypeCode == PrimitiveTypeCode.IntPtr)

+        return Bpl.Type.Int;

       else if (TypeHelper.IsPrimitiveInteger(type))

         return Bpl.Type.Int;

       else if (type.TypeCode == PrimitiveTypeCode.Float32 || type.TypeCode == PrimitiveTypeCode.Float64)

@@ -204,6 +206,9 @@ namespace BytecodeTranslator {
       // The Heap has to decide how to represent the field (i.e., its type),

       // all the Sink cares about is adding a declaration for it.

       Bpl.Variable v;

+      var specializedField = field as ISpecializedFieldReference;

+      if (specializedField != null)

+        field = specializedField.UnspecializedVersion;

       var key = field.InternedKey;

       if (!this.declaredFields.TryGetValue(key, out v)) {

         v = this.Heap.CreateFieldVariable(field);