Fixed many bugs.

Ctors now initialize all fields to default (null-equivalent) values.
Generate procedures for interface methods.
Translate enums just by ignoring them and using the integers that they really are.

9 files changed, 324 insertions, 69 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 1c401873..13cb3552 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -360,7 +360,9 @@ namespace BytecodeTranslator
       {

         var bplType = TranslationHelper.CciTypeToBoogie(constant.Type);

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

-          TranslatedExpressions.Push(Bpl.Expr.Literal(0));

+          var lit = Bpl.Expr.Literal(0);

+          lit.Type = Bpl.Type.Int;

+          TranslatedExpressions.Push(lit);

         } else if (bplType == Bpl.Type.Bool) {

           TranslatedExpressions.Push(Bpl.Expr.False);

         } else {

@@ -374,20 +376,24 @@ namespace BytecodeTranslator
       else if (constant.Value is string)

       {

         throw new NotImplementedException("Strings are not translated");

-      }

-      else

-      {

+      } else {

         // TODO: (mschaef) hack

-        TranslatedExpressions.Push(Bpl.Expr.Literal((int)constant.Value));

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

+        lit.Type = Bpl.Type.Int;

+        TranslatedExpressions.Push(lit);

       }

     }

 

     public override void Visit(IDefaultValue defaultValue) {

       var bplType = TranslationHelper.CciTypeToBoogie(defaultValue.Type);

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

-        TranslatedExpressions.Push(Bpl.Expr.Literal(0));

+        var lit = Bpl.Expr.Literal(0);

+        lit.Type = Bpl.Type.Int;

+        TranslatedExpressions.Push(lit);

       } else if (bplType == Bpl.Type.Bool) {

-        TranslatedExpressions.Push(Bpl.Expr.False);

+        var lit = Bpl.Expr.False;

+        lit.Type = Bpl.Type.Bool;

+        TranslatedExpressions.Push(lit);

       } else {

         throw new NotImplementedException("Don't know how to translate type");

       }

@@ -444,7 +450,7 @@ namespace BytecodeTranslator
       Bpl.IToken cloc = methodCall.Token();

 

       // meeting a constructor is always something special

-      if (resolvedMethod.IsConstructor)

+      if (false && resolvedMethod.IsConstructor)

       {

         // Todo: do something with the constructor call

       }

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index ee5206db..9018884b 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -414,6 +414,7 @@ procedure {:inline 1} Alloc() returns (x: int)
         new Bpl.FunctionCall(conversion),

         new Bpl.ExprSeq(selectExpr)

         );

+      callExpr.Type = f.Type;

       return callExpr;

 

     }

@@ -631,6 +632,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
         new Bpl.FunctionCall(conversion),

         new Bpl.ExprSeq(callRead)

         );

+      callExpr.Type = boogieType;

       return callExpr;

 

     }

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 440e829a..5b05a6bd 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -103,7 +103,7 @@ namespace BytecodeTranslator {
             out_count++;

           formalMap.Add(formal, mp);

         }

-        this.sink.FormalMap = formalMap;

+//        this.sink.FormalMap = formalMap;

 

         #region Look for Returnvalue

         if (invokeMethod.Type.TypeCode != PrimitiveTypeCode.Void)

@@ -240,9 +240,15 @@ namespace BytecodeTranslator {
         base.Visit(typeDefinition);

       } else if (typeDefinition.IsDelegate) {

         sink.AddDelegateType(typeDefinition);

+      } else if (typeDefinition.IsInterface) {

+        sink.FindOrCreateType(typeDefinition);

+        base.Visit(typeDefinition);

+      } else if (typeDefinition.IsEnum) {

+        return; // enums just are translated as ints

       } else {

-        Console.WriteLine("Non-Class {0} was found", typeDefinition);

-        throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString()));

+        Console.WriteLine("Unknown kind of type definition '{0}' was found",

+          TypeHelper.GetTypeName(typeDefinition));

+        throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));

       }

     }

 

@@ -260,19 +266,22 @@ namespace BytecodeTranslator {
 

       this.sink.BeginMethod();

 

-      var proc = this.sink.FindOrCreateProcedure(method, method.IsStatic);

+      var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method, method.IsStatic);

 

-      try {

+      if (method.IsAbstract) { // we're done, just define the procedure

+        return;

+      }

 

-        if (method.IsAbstract) {

-          throw new NotImplementedException("abstract methods are not yet implemented");

-        }

+      var proc = procAndFormalMap.Item1;

+      var formalMap = procAndFormalMap.Item2;

+

+      try {

 

         StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader);

 

-        #region Add assignements from In-Params to local-Params

+        #region Add assignments from In-Params to local-Params

 

-        foreach (MethodParameter mparam in this.sink.FormalMap.Values) {

+        foreach (MethodParameter mparam in formalMap.Values) {

           if (mparam.inParameterCopy != null) {

             Bpl.IToken tok = method.Token();

             stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

@@ -283,6 +292,26 @@ namespace BytecodeTranslator {
 

         #endregion

 

+        #region For non-deferring ctors, initialize all fields to null-equivalent values

+        if (method.IsConstructor) {

+          var smb = method.Body as ISourceMethodBody;

+          if (smb != null && !FindCtorCall.IsDeferringCtor(method, smb.Block)) {

+

+            var inits = new List<IStatement>();

+            var thisExp = new ThisReference() { Type = method.ContainingTypeDefinition, };

+            foreach (var f in method.ContainingTypeDefinition.Fields) {

+              var a = new Assignment() {

+                Source = new DefaultValue() { Type = f.Type, },

+                Target = new TargetExpression() { Definition = f, Instance = thisExp, Type = f.Type },

+                Type = f.Type,

+              };

+              inits.Add(new ExpressionStatement() { Expression = a, });

+            }

+            new BlockStatement() { Statements = inits, }.Dispatch(stmtTraverser);

+          }

+        }

+        #endregion

+

         try {

           method.Body.Dispatch(stmtTraverser);

         } catch (TranslationException te) {

@@ -293,7 +322,7 @@ namespace BytecodeTranslator {
 

         #region Create Local Vars For Implementation

         List<Bpl.Variable> vars = new List<Bpl.Variable>();

-        foreach (MethodParameter mparam in this.sink.FormalMap.Values) {

+        foreach (MethodParameter mparam in formalMap.Values) {

           if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))

             vars.Add(mparam.outParameterCopy);

         }

@@ -315,6 +344,7 @@ namespace BytecodeTranslator {
 

         impl.Proc = proc;

 

+        #region Translate method attributes

         // Don't need an expression translator because there is a limited set of things

         // that can appear as arguments to custom attributes

         foreach (var a in method.Attributes) {

@@ -332,7 +362,9 @@ namespace BytecodeTranslator {
                   o = (bool)mdc.Value ? Bpl.Expr.True : Bpl.Expr.False;

                   break;

                 case PrimitiveTypeCode.Int32:

-                  o = Bpl.Expr.Literal((int)mdc.Value);

+                  var lit = Bpl.Expr.Literal((int)mdc.Value);

+                  lit.Type = Bpl.Type.Int;

+                  o = lit;

                   break;

                 case PrimitiveTypeCode.String:

                   o = mdc.Value;

@@ -345,6 +377,7 @@ namespace BytecodeTranslator {
           }

           impl.AddAttribute(attrName, args);

         }

+        #endregion

 

         this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

 

@@ -363,5 +396,26 @@ namespace BytecodeTranslator {
 

     #endregion

 

+    private class FindCtorCall : BaseCodeTraverser {

+      private bool isDeferringCtor = false;

+      public ITypeReference containingType;

+      public static bool IsDeferringCtor(IMethodDefinition method, IBlockStatement body) {

+        var fcc = new FindCtorCall(method.ContainingType);

+        fcc.Visit(body);

+        return fcc.isDeferringCtor;

+      }

+      private FindCtorCall(ITypeReference containingType) {

+        this.containingType = containingType;

+      }

+      public override void Visit(IMethodCall methodCall) {

+        var md = methodCall.MethodToCall.ResolvedMethod;

+        if (md != null && md.IsConstructor && methodCall.ThisArgument is IThisReference) {

+          this.isDeferringCtor = TypeHelper.TypesAreEquivalent(md.ContainingType, containingType);

+          this.stopTraversal = true;

+          return;

+        }

+        base.Visit(methodCall);

+      }

+    }

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index f95675f7..c6fca998 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -130,10 +130,12 @@ namespace BytecodeTranslator {
     /// <returns></returns>

     public Bpl.Variable FindParameterVariable(IParameterDefinition param) {

       MethodParameter mp;

-      this.FormalMap.TryGetValue(param, out mp);

+      Tuple<Bpl.Procedure, Dictionary<IParameterDefinition, MethodParameter>> procAndFormalMap;

+      this.declaredMethods.TryGetValue(param.ContainingSignature, out procAndFormalMap);

+      var formalMap = procAndFormalMap.Item2;

+      formalMap.TryGetValue(param, out mp);

       return mp.outParameterCopy;

     }

-    public Dictionary<IParameterDefinition, MethodParameter> FormalMap = null;

 

     public Bpl.Variable FindOrCreateFieldVariable(IFieldReference field) {

       // The Heap has to decide how to represent the field (i.e., its type),

@@ -172,11 +174,10 @@ namespace BytecodeTranslator {
     }

 

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

-

     public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) {

-      Bpl.Procedure proc;

-      var key = method.InternedKey;

-      if (!this.declaredMethods.TryGetValue(key, out proc)) {

+      Tuple<Bpl.Procedure, Dictionary<IParameterDefinition, MethodParameter>> procAndFormalMap;

+      var key = method; //.InternedKey;

+      if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {

         #region Create in- and out-parameters

 

         int in_count = 0;

@@ -191,7 +192,6 @@ namespace BytecodeTranslator {
             out_count++;

           formalMap.Add(formal, mp);

         }

-        this.FormalMap = formalMap;

 

         #region Look for Returnvalue

 

@@ -300,7 +300,7 @@ namespace BytecodeTranslator {
 

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

 

-        proc = new Bpl.Procedure(method.Token(),

+        var proc = new Bpl.Procedure(method.Token(),

             MethodName,

             new Bpl.TypeVariableSeq(),

             new Bpl.VariableSeq(invars), // in

@@ -311,11 +311,17 @@ namespace BytecodeTranslator {
 

 

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        this.declaredMethods.Add(key, proc);

+        procAndFormalMap = Tuple.Create(proc, formalMap);

+        this.declaredMethods.Add(key, procAndFormalMap);

       }

-      return proc;

+      return procAndFormalMap.Item1;

+    }

+    public Tuple<Bpl.Procedure,Dictionary<IParameterDefinition, MethodParameter>> FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method, bool isStatic) {

+      this.FindOrCreateProcedure(method, isStatic);

+      return this.declaredMethods[method];

     }

 

+

     /// <summary>

     /// Creates a fresh variable that represents the type of

     /// <paramref name="type"/> in the Bpl program. I.e., its

@@ -339,13 +345,14 @@ namespace BytecodeTranslator {
     private Dictionary<uint, Bpl.Variable> declaredTypes = new Dictionary<uint, Bpl.Variable>();

 

     /// <summary>

-    /// The keys to the table are the interned key of the field.

+    /// The keys to the table are the signatures of the methods.

+    /// The values are pairs: first element is the procedure,

+    /// second element is the formal map for the procedure

     /// </summary>

-    private Dictionary<uint, Bpl.Procedure> declaredMethods = new Dictionary<uint, Bpl.Procedure>();

+    private Dictionary<ISignature, Tuple<Bpl.Procedure, Dictionary<IParameterDefinition, MethodParameter>>> declaredMethods = new Dictionary<ISignature, Tuple<Bpl.Procedure, Dictionary<IParameterDefinition, MethodParameter>>>();

 

     public void BeginMethod() {

       this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

-      this.FormalMap = new Dictionary<IParameterDefinition, MethodParameter>();

     }

 

     public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 9b13508f..f2918aa7 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -122,4 +122,12 @@ namespace RegressionTestInput {
       }

     }

   }

+

+  public class WriteToTheHeapAValueReadFromTheHeap {

+    int x;

+    int y;

+    public void M() {

+      this.y = this.x;

+    }

+  }

 }

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index a77683fe..00b54a84 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -222,14 +222,57 @@ var $Method: [int][int]int;
 

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

 

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

+

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

+

+

+

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

+{

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

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

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

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

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

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

+    return;

+}

+

+

+

 const unique RegressionTestInput.AsyncAttribute: Type;

 

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

 

 

 

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

+

+

+

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

 {

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

     return;

 }

 

@@ -271,7 +314,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
   var z: bool;

 

     z := z$in;

+    $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.staticB, Bool2Box(false));

+    $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));

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

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

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

     $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));

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

@@ -406,7 +452,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
   var xs: int;

 

     xs := xs$in;

-    if (!(!(xs != 0) || $ArrayLength[xs] <= 0))

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

     {

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

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

@@ -427,6 +473,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

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

 {

+    $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.s, Int2Box(0));

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

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

     return;

 }

 

@@ -464,21 +513,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
   var x: int;

   var __temp_1: int;

   var $tmp5: int;

-  var __temp_2: int;

-  var __temp_3: int;

   var local_0: int;

 

     x := x$in;

     $tmp5 := x;

     assert $tmp5 != 0;

     __temp_1 := 5 / $tmp5;

-    __temp_2 := 3;

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

-    __temp_3 := __temp_2;

-    x := __temp_3;

-    local_0 := __temp_1 + __temp_2;

+    x := 3;

+    local_0 := __temp_1 + 3;

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

-    assert x == 3 && local_0 <= 8;

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

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

     RegressionTestInput.Class0.StaticInt := local_0;

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

@@ -665,6 +709,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int);
 

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

 {

+    $Heap := Write($Heap, this, RegressionTestInput.Class0.StaticInt, Int2Box(0));

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

     return;

 }

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index d0b573a6..f634d13a 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -194,12 +194,53 @@ var $Method: [int][int]int;
 

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

 

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

+

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

+

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

+

+

+

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

+{

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

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

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

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

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

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

+    return;

+}

+

+

+

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

 

 

 

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

+

+

+

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

 {

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

     return;

 }

 

@@ -239,7 +280,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
   var z: bool;

 

     z := z$in;

+    RegressionTestInput.ClassWithBoolTypes.staticB[this] := false;

+    RegressionTestInput.ClassWithBoolTypes.b[this] := false;

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

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

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

     RegressionTestInput.ClassWithBoolTypes.b[this] := z;

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

@@ -372,7 +416,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
   var xs: int;

 

     xs := xs$in;

-    if (!(!(xs != 0) || $ArrayLength[xs] <= 0))

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

     {

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

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

@@ -393,6 +437,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

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

 {

+    RegressionTestInput.ClassWithArrayTypes.s[this] := 0;

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

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

     return;

 }

 

@@ -428,21 +475,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
   var x: int;

   var __temp_1: int;

   var $tmp5: int;

-  var __temp_2: int;

-  var __temp_3: int;

   var local_0: int;

 

     x := x$in;

     $tmp5 := x;

     assert $tmp5 != 0;

     __temp_1 := 5 / $tmp5;

-    __temp_2 := 3;

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

-    __temp_3 := __temp_2;

-    x := __temp_3;

-    local_0 := __temp_1 + __temp_2;

+    x := 3;

+    local_0 := __temp_1 + 3;

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

-    assert x == 3 && local_0 <= 8;

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

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

     RegressionTestInput.Class0.StaticInt := local_0;

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

@@ -629,6 +671,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int);
 

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

 {

+    RegressionTestInput.Class0.StaticInt[this] := 0;

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

     return;

 }

 

diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index 918bf1f7..35328269 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -204,12 +204,53 @@ var $Method: [int][int]int;
 

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

 

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;

+

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

+

+

+

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

+{

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

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);

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

+    return;

+}

+

+

+

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

 

 

 

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

+

+

+

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

 {

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

     return;

 }

 

@@ -249,7 +290,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
   var z: bool;

 

     z := z$in;

+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.staticB] := Bool2Box(false);

+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);

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

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

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

     $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);

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

@@ -382,7 +426,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
   var xs: int;

 

     xs := xs$in;

-    if (!(!(xs != 0) || $ArrayLength[xs] <= 0))

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

     {

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

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

@@ -403,6 +447,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

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

 {

+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.s] := Int2Box(0);

+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0);

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

     return;

 }

 

@@ -438,21 +485,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
   var x: int;

   var __temp_1: int;

   var $tmp5: int;

-  var __temp_2: int;

-  var __temp_3: int;

   var local_0: int;

 

     x := x$in;

     $tmp5 := x;

     assert $tmp5 != 0;

     __temp_1 := 5 / $tmp5;

-    __temp_2 := 3;

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

-    __temp_3 := __temp_2;

-    x := __temp_3;

-    local_0 := __temp_1 + __temp_2;

+    x := 3;

+    local_0 := __temp_1 + 3;

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

-    assert x == 3 && local_0 <= 8;

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

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

     RegressionTestInput.Class0.StaticInt := local_0;

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

@@ -639,6 +681,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int);
 

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

 {

+    $Heap[this, RegressionTestInput.Class0.StaticInt] := Int2Box(0);

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

     return;

 }

 

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
index 1b0f35b8..e48e4bd1 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -194,12 +194,53 @@ var $Method: [int][int]int;
 

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

 

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;

+

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;

+

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

+

+

+

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

+{

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

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x];

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

+    return;

+}

+

+

+

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

+

+

+

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

+

+

+

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

+{

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0;

+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0;

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

+    return;

+}

+

+

+

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

 

 

 

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

+

+

+

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

 {

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

     return;

 }

 

@@ -239,7 +280,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
   var z: bool;

 

     z := z$in;

+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.staticB] := false;

+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false;

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

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

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

     $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;

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

@@ -372,7 +416,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
   var xs: int;

 

     xs := xs$in;

-    if (!(!(xs != 0) || $ArrayLength[xs] <= 0))

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

     {

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

         $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][0 := $ArrayContents[xs][0]]];

@@ -393,6 +437,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 

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

 {

+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.s] := 0;

+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0;

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

     return;

 }

 

@@ -428,21 +475,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
   var x: int;

   var __temp_1: int;

   var $tmp5: int;

-  var __temp_2: int;

-  var __temp_3: int;

   var local_0: int;

 

     x := x$in;

     $tmp5 := x;

     assert $tmp5 != 0;

     __temp_1 := 5 / $tmp5;

-    __temp_2 := 3;

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

-    __temp_3 := __temp_2;

-    x := __temp_3;

-    local_0 := __temp_1 + __temp_2;

+    x := 3;

+    local_0 := __temp_1 + 3;

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

-    assert x == 3 && local_0 <= 8;

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

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

     RegressionTestInput.Class0.StaticInt := local_0;

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

@@ -629,6 +671,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int);
 

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

 {

+    $Heap[this, RegressionTestInput.Class0.StaticInt] := 0;

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

     return;

 }