Lots of small bug fixes: conversions, overloaded operations on real numbers.

8 files changed, 444 insertions, 85 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index ccd3f748..123280ed 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -349,11 +349,16 @@ namespace BytecodeTranslator
           lit.Type = Bpl.Type.Int;

           TranslatedExpressions.Push(lit);

           break;

-        case PrimitiveTypeCode.Float32:

-        case PrimitiveTypeCode.Float64:

-          var c = this.sink.FindOrCreateConstant((double)(constant.Value));

-          TranslatedExpressions.Push(Bpl.Expr.Ident(c));

-          return;

+        case PrimitiveTypeCode.Float32: {

+            var c = this.sink.FindOrCreateConstant((float)(constant.Value));

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

+            return;

+          }

+        case PrimitiveTypeCode.Float64: {

+            var c = this.sink.FindOrCreateConstant((double)(constant.Value));

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

+            return;

+          }

         case PrimitiveTypeCode.NotPrimitive:

           if (constant.Type.IsEnum) {

             lit = Bpl.Expr.Literal((int)constant.Value);

@@ -902,7 +907,37 @@ namespace BytecodeTranslator
       base.Visit(addition);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp));

+      Bpl.Expr e;

+      switch (addition.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            addition.Token(),

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

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

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

+          break;

+      }

+      TranslatedExpressions.Push(e);

+    }

+

+    // TODO: Encode this correctly!

+    public override void Visit(IBitwiseAnd bitwiseAnd) {

+      base.Visit(bitwiseAnd);

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

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

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, lexp, rexp));

+    }

+

+    // TODO: Encode this correctly!

+    public override void Visit(IBitwiseOr bitwiseOr) {

+      base.Visit(bitwiseOr);

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

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

+      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, lexp, rexp));

     }

 

     public override void Visit(IDivision division)

@@ -910,7 +945,21 @@ namespace BytecodeTranslator
       base.Visit(division);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

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

+      Bpl.Expr e;

+      switch (division.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            division.Token(),

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

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

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

+          break;

+      }

+      TranslatedExpressions.Push(e);

     }

 

     // TODO: Encode this correctly!

@@ -926,7 +975,21 @@ namespace BytecodeTranslator
       base.Visit(subtraction);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp));

+      Bpl.Expr e;

+      switch (subtraction.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            subtraction.Token(),

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

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

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

+          break;

+      }

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IMultiplication multiplication)

@@ -934,7 +997,21 @@ namespace BytecodeTranslator
       base.Visit(multiplication);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp));

+      Bpl.Expr e;

+      switch (multiplication.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            multiplication.Token(),

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

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

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

+          break;

+      }

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IModulus modulus)

@@ -1152,6 +1229,12 @@ namespace BytecodeTranslator
             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)));

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 3dc1b5f9..0b2dd6cf 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -229,6 +229,17 @@ namespace BytecodeTranslator {
     public Bpl.Function Real2Ref = null;

     #endregion

 

+    #region Real number operations

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

+    public Bpl.Function RealPlus = null;

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

+    public Bpl.Function RealMinus = null;

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

+    public Bpl.Function RealTimes = null;

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

+    public Bpl.Function RealDivide = null;

+    #endregion

+

     #region Ref conversions

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

     public Bpl.Function Ref2Int = null;

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 18b8e0e6..1cad1a36 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -396,7 +396,20 @@ namespace BytecodeTranslator {
         } else { // method is translated as a function

           //var func = decl as Bpl.Function;

           //Contract.Assume(func != null);

-          //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);

+          //var blocks = new List<Bpl.Block>();

+          //var counter = 0;

+          //var returnValue = decl.OutParams[0];

+          //foreach (var bb in translatedBody.BigBlocks) {

+          //  var label = bb.LabelName ?? "L" + counter++.ToString();

+          //  var newTransferCmd = (bb.tc is Bpl.ReturnCmd)

+          //    ? new Bpl.ReturnExprCmd(bb.tc.tok, Bpl.Expr.Ident(returnValue))

+          //    : bb.tc;

+          //  var b = new Bpl.Block(bb.tok, label, bb.simpleCmds, newTransferCmd);

+          //  blocks.Add(b);

+          //}

+          //var localVars = new Bpl.VariableSeq();

+          //localVars.Add(returnValue);

+          //func.Body = new Bpl.CodeExpr(localVars, blocks);

         }

         #endregion

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index bc28d9be..127317e9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -251,6 +251,20 @@ namespace BytecodeTranslator {
       }

       return c;

     }

+    public Bpl.Constant FindOrCreateConstant(float f) {

+      Bpl.Constant c;

+      var str = f.ToString();

+      if (!this.declaredRealConstants.TryGetValue(str, out c)) {

+        var tok = Bpl.Token.NoToken;

+        var t = Heap.RealType;

+        var name = "$real_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str) + "_" + declaredStringConstants.Count;

+        var tident = new Bpl.TypedIdent(tok, name, t);

+        c = new Bpl.Constant(tok, tident, true);

+        this.declaredRealConstants.Add(str, c);

+        this.TranslatedProgram.TopLevelDeclarations.Add(c);

+      }

+      return c;

+    }

     private Dictionary<string, Bpl.Constant> declaredRealConstants = new Dictionary<string, Bpl.Constant>();

 

     private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();

@@ -431,7 +445,7 @@ namespace BytecodeTranslator {
         // Can't visit the method's contracts until the formalMap and procedure are added to the

         // table because information in them might be needed (e.g., if a parameter is mentioned

         // in a contract.

-        #region Check The Method Contracts

+        #region Translate the method's contracts

 

         var possiblyUnspecializedMethod = Unspecialize(method);

 

@@ -586,6 +600,9 @@ namespace BytecodeTranslator {
     // also, should it return true for properties and all of the other things the tools

     // consider pure?

     private bool IsPure(IMethodDefinition method) {

+      bool isPropertyGetter = method.IsSpecialName && method.Name.Value.StartsWith("get_");

+      if (isPropertyGetter) return true;

+

       foreach (var a in method.Attributes) {

         if (TypeHelper.GetTypeName(a.Type).EndsWith("PureAttribute")) {

           return true;

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index d554d83e..cf856024 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -111,6 +111,7 @@ namespace BytecodeTranslator {
       s = s.Replace('-', '$');

       s = s.Replace(' ', '$');

       s = s.Replace('\t', '$');

+      s = s.Replace('\r', '$');

       s = s.Replace('\n', '$');

       s = s.Replace('/', '$');

       s = s.Replace('\\', '$');

@@ -119,6 +120,7 @@ namespace BytecodeTranslator {
       s = s.Replace(';', '$');

       s = s.Replace('%', '$');

       s = s.Replace('&', '$');

+      s = s.Replace('"', '$');

       return s;

     }

 

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 90fa7b50..c811e9eb 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -157,4 +157,21 @@ namespace RegressionTestInput {
     }

   }

 

+  public class RealNumbers {

+    public void WriteDouble(double d) {

+      Console.WriteLine(d);

+    }

+    public void ObjectToDouble(object o) {

+      WriteDouble((double)o);

+    }

+    public void RealOperations() {

+      double d = 3.0;

+      double d2 = 4.0;

+      WriteDouble(d + d2);

+      WriteDouble(d - d2);

+      WriteDouble(d * d2);

+      WriteDouble(d / d2);

+    }

+  }

+

 }

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index eff71038..a5e1fffa 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -333,6 +333,14 @@ function Ref2Real(Ref, Type, Type) : Real;
 

 function Real2Ref(Real, Type, Type) : Ref;

 

+function RealPlus(Real, Real) : Real;

+

+function RealMinus(Real, Real) : Real;

+

+function RealTimes(Real, Real) : Real;

+

+function RealDivide(Real, Real) : Real;

+

 function Ref2Int(Ref, Type, Type) : int;

 

 function Ref2Bool(Ref, Type, Type) : bool;

@@ -351,6 +359,110 @@ var $Method: [Ref][Ref]int;
 

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

 

+const unique RegressionTestInput.RealNumbers: Type;

+

+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real);

+

+

+

+procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);

+

+

+

+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real)

+{

+  var d: Real;

+

+    d := d$in;

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

+    call System.Console.WriteLine$System.Double(d);

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref);

+

+

+

+const {:extern} unique System.Object: Type;

+

+const {:extern} unique System.Double: Type;

+

+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref)

+{

+  var o: Ref;

+

+    o := o$in;

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, Ref2Real(o, System.Object, System.Double));

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.RealOperations(this: Ref);

+

+

+

+const unique $real_literal_3_0: Real;

+

+const unique $real_literal_4_0: Real;

+

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

+{

+  var local_0: Real;

+  var local_1: Real;

+  var $tmp0: Real;

+

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

+    local_0 := $real_literal_3_0;

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

+    local_1 := $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(local_0, local_1));

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealMinus(local_0, local_1));

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealTimes(local_0, local_1));

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

+    $tmp0 := local_1;

+    assert $tmp0 != 0;

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, local_0 / $tmp0);

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.#cctor();

+

+

+

+implementation RegressionTestInput.RealNumbers.#cctor()

+{

+}

+

+

+

 const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

 

 const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

@@ -375,10 +487,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Re
 

 

 

-procedure {:extern} System.Object.#ctor(this: Ref);

-

-

-

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

 {

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

@@ -417,14 +525,14 @@ const unique RegressionTestInput.S.b: Field;
 

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

 {

-  var $tmp0: Ref;

+  var $tmp1: Ref;

   var local_0: Ref;

 

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

-    call $tmp0 := Alloc();

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

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

-    local_0 := $tmp0;

+    call $tmp1 := Alloc();

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

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

+    local_0 := $tmp1;

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

     assert Box2Int(Read($Heap, local_0, RegressionTestInput.S.x)) == 0;

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

@@ -491,22 +599,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: Ref;

-  var $tmp1: Ref;

-  var local_1: Ref;

   var $tmp2: Ref;

+  var local_1: Ref;

+  var $tmp3: Ref;

 

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

-    call $tmp1 := Alloc();

-    assume $ArrayLength($tmp1) == 1 * 5;

-    local_0 := $tmp1;

+    call $tmp2 := Alloc();

+    assume $ArrayLength($tmp2) == 1 * 5;

+    local_0 := $tmp2;

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

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

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

     assert local_0 == 2;

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

-    call $tmp2 := Alloc();

-    assume $ArrayLength($tmp2) == 1 * 4;

-    local_1 := $tmp2;

+    call $tmp3 := Alloc();

+    assume $ArrayLength($tmp3) == 1 * 4;

+    local_1 := $tmp3;

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

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

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

@@ -525,22 +633,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: Ref;

-  var local_0: Ref;

   var $tmp4: Ref;

+  var local_0: Ref;

+  var $tmp5: Ref;

 

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

-    call $tmp3 := Alloc();

-    assume $ArrayLength($tmp3) == 1 * 5;

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    call $tmp4 := Alloc();

+    assume $ArrayLength($tmp4) == 1 * 5;

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp4;

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

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

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

     assert RegressionTestInput.ClassWithArrayTypes.s == 2;

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

-    call $tmp4 := Alloc();

-    assume $ArrayLength($tmp4) == 1 * 4;

-    local_0 := $tmp4;

+    call $tmp5 := Alloc();

+    assume $ArrayLength($tmp5) == 1 * 4;

+    local_0 := $tmp5;

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

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

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

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

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp6: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp6 := x;

+    assert $tmp6 != 0;

+    __temp_1 := 5 / $tmp6;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -815,11 +923,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int);
 

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

 {

-  var $tmp6: int;

+  var $tmp7: int;

 

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

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

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

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

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

     return;

 }

 

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

 {

   var y: int;

-  var $tmp7: int;

+  var $tmp8: int;

 

     y := y$in;

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

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

-    $result := $tmp7;

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

+    $result := $tmp8;

     return;

 }

 

@@ -995,10 +1103,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp8: bool;

+  var $tmp9: bool;

 

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

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

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

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

     return;

 }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 77d0950a..f6e4583f 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -323,6 +323,14 @@ function Ref2Real(Ref, Type, Type) : Real;
 

 function Real2Ref(Real, Type, Type) : Ref;

 

+function RealPlus(Real, Real) : Real;

+

+function RealMinus(Real, Real) : Real;

+

+function RealTimes(Real, Real) : Real;

+

+function RealDivide(Real, Real) : Real;

+

 function Ref2Int(Ref, Type, Type) : int;

 

 function Ref2Bool(Ref, Type, Type) : bool;

@@ -341,6 +349,110 @@ var $Method: [Ref][Ref]int;
 

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

 

+const unique RegressionTestInput.RealNumbers: Type;

+

+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real);

+

+

+

+procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);

+

+

+

+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real)

+{

+  var d: Real;

+

+    d := d$in;

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

+    call System.Console.WriteLine$System.Double(d);

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref);

+

+

+

+const {:extern} unique System.Object: Type;

+

+const {:extern} unique System.Double: Type;

+

+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref)

+{

+  var o: Ref;

+

+    o := o$in;

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, Ref2Real(o, System.Object, System.Double));

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.RealOperations(this: Ref);

+

+

+

+const unique $real_literal_3_0: Real;

+

+const unique $real_literal_4_0: Real;

+

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

+{

+  var local_0: Real;

+  var local_1: Real;

+  var $tmp0: Real;

+

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

+    local_0 := $real_literal_3_0;

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

+    local_1 := $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(local_0, local_1));

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealMinus(local_0, local_1));

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

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealTimes(local_0, local_1));

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

+    $tmp0 := local_1;

+    assert $tmp0 != 0;

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, local_0 / $tmp0);

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RealNumbers.#cctor();

+

+

+

+implementation RegressionTestInput.RealNumbers.#cctor()

+{

+}

+

+

+

 const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

 

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

@@ -365,10 +477,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Re
 

 

 

-procedure {:extern} System.Object.#ctor(this: Ref);

-

-

-

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

 {

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

@@ -407,14 +515,14 @@ var RegressionTestInput.S.b: [Ref]bool;
 

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

 {

-  var $tmp0: Ref;

+  var $tmp1: Ref;

   var local_0: Ref;

 

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

-    call $tmp0 := Alloc();

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

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

-    local_0 := $tmp0;

+    call $tmp1 := Alloc();

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

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

+    local_0 := $tmp1;

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

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

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

@@ -481,22 +589,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: Ref;

-  var $tmp1: Ref;

-  var local_1: Ref;

   var $tmp2: Ref;

+  var local_1: Ref;

+  var $tmp3: Ref;

 

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

-    call $tmp1 := Alloc();

-    assume $ArrayLength($tmp1) == 1 * 5;

-    local_0 := $tmp1;

+    call $tmp2 := Alloc();

+    assume $ArrayLength($tmp2) == 1 * 5;

+    local_0 := $tmp2;

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

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

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

     assert local_0 == 2;

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

-    call $tmp2 := Alloc();

-    assume $ArrayLength($tmp2) == 1 * 4;

-    local_1 := $tmp2;

+    call $tmp3 := Alloc();

+    assume $ArrayLength($tmp3) == 1 * 4;

+    local_1 := $tmp3;

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

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

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

@@ -515,22 +623,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: Ref;

-  var local_0: Ref;

   var $tmp4: Ref;

+  var local_0: Ref;

+  var $tmp5: Ref;

 

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

-    call $tmp3 := Alloc();

-    assume $ArrayLength($tmp3) == 1 * 5;

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    call $tmp4 := Alloc();

+    assume $ArrayLength($tmp4) == 1 * 5;

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp4;

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

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

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

     assert RegressionTestInput.ClassWithArrayTypes.s == 2;

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

-    call $tmp4 := Alloc();

-    assume $ArrayLength($tmp4) == 1 * 4;

-    local_0 := $tmp4;

+    call $tmp5 := Alloc();

+    assume $ArrayLength($tmp5) == 1 * 4;

+    local_0 := $tmp5;

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

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

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

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

   var x: int;

   var __temp_1: int;

-  var $tmp5: int;

+  var $tmp6: int;

   var local_0: int;

 

     x := x$in;

-    $tmp5 := x;

-    assert $tmp5 != 0;

-    __temp_1 := 5 / $tmp5;

+    $tmp6 := x;

+    assert $tmp6 != 0;

+    __temp_1 := 5 / $tmp6;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -805,11 +913,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int);
 

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

 {

-  var $tmp6: int;

+  var $tmp7: int;

 

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

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

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

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

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

     return;

 }

 

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

 {

   var y: int;

-  var $tmp7: int;

+  var $tmp8: int;

 

     y := y$in;

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

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

-    $result := $tmp7;

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

+    $result := $tmp8;

     return;

 }

 

@@ -985,10 +1093,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp8: bool;

+  var $tmp9: bool;

 

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

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

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

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

     return;

 }