Added a better options parsing by using functionality from MemberHelper.

Added a new heap representation, TwoDBoxHeap.
Made method names unique (previously, overloads all shared the same procedure name). As part of that, no longer require method references to be resolved in order to generate a name.
Added a regression test for TwoDBoxHeap.
Added tests for method overloads for unique name generation.

9 files changed, 456 insertions, 197 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 150518b0..dd6cbb66 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -462,7 +462,7 @@ namespace BytecodeTranslator
           outvars.Add(new Bpl.IdentifierExpr(cloc, v));

           TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

         }

-        string methodname = TranslationHelper.CreateUniqueMethodName(resolvedMethod);

+        string methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);

 

 

         Bpl.QKeyValue attrib = null;

@@ -626,7 +626,7 @@ namespace BytecodeTranslator
       }

 

       Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();

-      string methodname = TranslationHelper.CreateUniqueMethodName(ctor.ResolvedMethod);

+      string methodname = TranslationHelper.CreateUniqueMethodName(ctor);

 

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, methodname, inexpr, outvars));

 

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index cfc30c97..33610930 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -213,6 +213,147 @@ procedure {:inline 1} Alloc() returns (x: int)
 

   }

 

+  /// <summary>

+  /// A heap representation that uses a global variable, $Heap, which is

+  /// a two-dimensional array indexed by objects and fields. Objects

+  /// are values of type "int", fields are unique constants, and the

+  /// elements of the heap are of type "box". Each value that is read/written

+  /// from/to the heap is wrapped in a type conversion function.

+  /// </summary>

+  public class TwoDBoxHeap : HeapFactory, IHeap {

+

+    #region Fields

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

+    private Bpl.Variable HeapVariable = null;

+

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

+    private Bpl.Function Box2Int = null;

+

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

+    private Bpl.Function Box2Bool = null;

+

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

+    private Bpl.Function Int2Box = null;

+

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

+    private Bpl.Function Bool2Box = null;

+

+    /// <summary>

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

+    /// </summary>

+    private readonly string InitialPreludeText =

+      @"const null: int;

+type box;

+type HeapType = [int,int]box;

+function IsGoodHeap(HeapType): bool;

+var $ArrayContents: [int][int]int;

+var $ArrayLength: [int]int;

+

+var $Alloc: [int] bool;

+procedure {:inline 1} Alloc() returns (x: int)

+  free ensures x != 0;

+  modifies $Alloc;

+{

+  assume $Alloc[x] == false;

+  $Alloc[x] := true;

+}

+";

+    private Sink sink;

+

+    #endregion

+

+    public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {

+      this.sink = sink;

+      heap = this;

+      program = null;

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

+      return b;

+    }

+

+    /// <summary>

+    /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding

+    /// on its type based on the heap representation.

+    /// </summary>

+    public Bpl.Variable CreateFieldVariable(IFieldReference field) {

+      Bpl.Variable v;

+      string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;

+      Bpl.IToken tok = field.Token();

+      Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);

+

+      if (field.IsStatic) {

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

+        v = new Bpl.GlobalVariable(tok, tident);

+      } else {

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

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

+      }

+      return v;

+    }

+

+    /// <summary>

+    /// Returns the (typed) BPL expression that corresponds to the value of the field

+    /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

+    /// <paramref name="o"/> is non-null, otherwise the value of the static field.

+    /// </summary>

+    /// <param name="o">The expression that represents the object to be dereferenced.

+    /// Null if <paramref name="f"/> is a static field.

+    /// </param>

+    /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when

+    /// it is not null. Otherwise the static field whose value should be read.

+    /// </param>

+    public Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {

+      // $Heap[o,f]

+      var selectExpr = Bpl.Expr.Select(new Bpl.IdentifierExpr(f.tok, HeapVariable), new Bpl.Expr[] { o, f });

+      // wrap it in the right conversion function

+      Bpl.Function conversion;

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

+        conversion = this.Box2Bool;

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

+        conversion = this.Box2Int;

+      else

+        throw new InvalidOperationException("Unknown Boogie type");

+      var callExpr = new Bpl.NAryExpr(

+        f.tok,

+        new Bpl.FunctionCall(conversion),

+        new Bpl.ExprSeq(selectExpr)

+        );

+      return callExpr;

+

+    }

+

+    /// <summary>

+    /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>

+    /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when

+    /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static

+    /// field.

+    /// </summary>

+    public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {

+      if (o == null) {

+        return Bpl.Cmd.SimpleAssign(tok, f, value);

+      } else {

+        // wrap it in the right conversion function

+        Bpl.Function conversion;

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

+          conversion = this.Bool2Box;

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

+          conversion = this.Int2Box;

+        else

+          throw new InvalidOperationException("Unknown Boogie type");

+

+        // $Heap[o,f] := conversion(value)

+        var callExpr = new Bpl.NAryExpr(

+          f.tok,

+          new Bpl.FunctionCall(conversion),

+          new Bpl.ExprSeq(value)

+          );

+        return

+          Bpl.Cmd.MapAssign(tok,

+          new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), callExpr);

+      }

+    }

+

+  }

+

   internal class RepresentationFor : Attribute {

     internal string name;

     internal string declaration;

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 12ed25a0..09a82009 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -16,64 +16,58 @@ using Microsoft.Cci.ILToCodeModel;
 using Bpl = Microsoft.Boogie;

 

 namespace BytecodeTranslator {

-  public class CommandLineOptions

-  {

-    public static bool SplitFields = false;

+

+  class Options : OptionParsing {

+

+    [OptionDescription("The name of the assembly to use as input", ShortForm = "a")]

+    public string assembly = null;

+

+    [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]

+    public List<string> libpaths = new List<string>();

+

+    public enum HeapRepresentation { splitFields, twoDInt, twoDBox }

+    [OptionDescription("Heap representation to use", ShortForm = "heap")]

+    public HeapRepresentation heapRepresentation = HeapRepresentation.twoDInt;

+

   }

 

   public class BCT {

 

     public static IMetadataHost Host;

 

-    public static bool Parse(string[] args, out string assemblyName)

-    {

-        assemblyName = "";

-        

-        foreach (string arg in args)

-        {

-            if (arg.StartsWith("/"))

-            {

-                if (arg == "/splitFields")

-                {

-                    CommandLineOptions.SplitFields = true;

-                }

-                else

-                {

-                    Console.WriteLine("Illegal option.");

-                    return false;

-                }

-            }

-            else if (assemblyName == "")

-            {

-                assemblyName = arg;

-            }

-            else

-            {

-                Console.WriteLine("Must specify only one input assembly.");

-                return false;

-            }

-        }

-        if (assemblyName == "")

-        {

-            Console.WriteLine("Must specify an input assembly.");

-            return false;

-        }

-        return true;

-    }

-

     static int Main(string[] args)

     {

       int result = 0;

-      string assemblyName;

-      if (!Parse(args, out assemblyName))

-          return result;

+

+      #region Parse options

+      var options = new Options();

+      options.Parse(args);

+      if (options.HasErrors) {

+        if (options.HelpRequested)

+          options.PrintOptions("");

+        return 1;

+      }

+      #endregion

+

+      var assemblyName = String.IsNullOrEmpty(options.assembly) ? options.GeneralArguments[0] : options.assembly;

+

       try {

         HeapFactory heap;

-        if (CommandLineOptions.SplitFields)

-          heap = new SplitFieldsHeap();

-        else

-          heap = new TwoDIntHeap();

-        result = TranslateAssembly(assemblyName, heap);

+        switch (options.heapRepresentation) {

+          case Options.HeapRepresentation.splitFields:

+            heap = new SplitFieldsHeap();

+            break;

+          case Options.HeapRepresentation.twoDInt:

+            heap = new TwoDIntHeap();

+            break;

+          case Options.HeapRepresentation.twoDBox:

+            heap = new TwoDBoxHeap();

+            break;

+          default:

+            Console.WriteLine("Unknown setting for /heap");

+            return 1;

+        }

+        result = TranslateAssembly(assemblyName, heap, options.libpaths);

       } catch (Exception e) { // swallow everything and just return an error code

         Console.WriteLine("The byte-code translator failed with uncaught exception: {0}", e.Message);

         Console.WriteLine("Stack trace: {0}", e.StackTrace);

@@ -82,9 +76,9 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory) {

+    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory, List<string>/*?*/ libPaths) {

 

-      var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment();

+      var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment(libPaths != null ? libPaths : IteratorHelper.GetEmptyEnumerable<string>(), true, true);

       Host = host;

 

       IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 1a326440..9f90f94d 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -79,8 +79,9 @@ namespace BytecodeTranslator {
       return "$tmp" + (tmpVarCounter++).ToString();

     }

 

-    public static string CreateUniqueMethodName(IMethodDefinition method) {

-      if (method.ContainingType.ToString() == "Poirot.Poirot")

+    public static string CreateUniqueMethodName(IMethodReference method) {

+      var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);

+      if (containingTypeName == "Poirot.Poirot")

       {

           string name = method.Name.Value;

           if (name == "BeginAtomic")

@@ -92,7 +93,12 @@ namespace BytecodeTranslator {
           else if (name == "Nondet")

               return "poirot_nondet";

       }

-      return method.ContainingType.ToString() + "." + method.Name.Value + "$" + method.Type.ResolvedType.ToString();

+      var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);

+      s = s.Substring(2);

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

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

+      s = s.TrimEnd(')');

+      return s;

     }

 

     #region Temp Stuff that must be replaced as soon as there is real code to deal with this

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 80f0af40..38d696b7 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -24,6 +24,11 @@ namespace RegressionTestInput {
       Contract.Assert(y == StaticInt);

     }

 

+    // Test to make sure we generate unique procedure names

+    void M(int x, int y) { }

+    void M(bool b) { }

+    void M(Class0 c) { }

+

     int NonVoid() {

       return 3 + StaticInt + StaticMethod(3);

     }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 6fc1bdf1..bcbdb0d5 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -29,11 +29,11 @@ implementation Alloc() returns (x: int)
 

 

 

-procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int)

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

 {

     return;

 }

@@ -44,11 +44,11 @@ var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
 

 var RegressionTestInput.ClassWithBoolTypes.b: [int]bool;

 

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

 {

   var x: int;

   var y: int;

@@ -56,30 +56,30 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int
 

     x := x$in;

     y := y$in;

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

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

     local_0 := x < y;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)

 {

   var z: bool;

 

     z := z$in;

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

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

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

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

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

     if (z)

     {

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

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

         RegressionTestInput.ClassWithBoolTypes.staticB := z;

     }

     else

@@ -91,17 +91,17 @@ implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: in
 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes.Main$System.Void();

+procedure RegressionTestInput.ClassWithBoolTypes.Main();

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.Main$System.Void()

+implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

   var $tmp0: bool;

 

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

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

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

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

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

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

     return;

 }

 

@@ -111,97 +111,97 @@ var RegressionTestInput.ClassWithArrayTypes.s: int;
 

 var RegressionTestInput.ClassWithArrayTypes.a: [int]int;

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main1$System.Void();

+procedure RegressionTestInput.ClassWithArrayTypes.Main1();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main1$System.Void()

+implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

   var $tmp1: int;

   var local_1: int;

   var $tmp2: int;

 

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

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

     call $tmp1 := Alloc();

     local_0 := $tmp1;

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

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

     $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

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

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

     assert $ArrayContents[local_0][0] == 2;

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

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

     call $tmp2 := Alloc();

     local_1 := $tmp2;

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

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

     $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

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

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

     assert $ArrayContents[local_1][0] == 1;

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

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

     assert $ArrayContents[local_0][0] == 2;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main2$System.Void();

+procedure RegressionTestInput.ClassWithArrayTypes.Main2();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main2$System.Void()

+implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

   var $tmp3: int;

   var local_0: int;

   var $tmp4: int;

 

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

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

     call $tmp3 := Alloc();

     RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

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

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

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

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

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

     assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

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

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

     call $tmp4 := Alloc();

     local_0 := $tmp4;

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

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

     $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

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

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

     assert $ArrayContents[local_0][0] == 1;

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

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

     assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int);

+procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int)

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

 {

   var x: int;

 

     x := x$in;

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

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

     $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x := 42]];

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

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

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

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

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

     assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1] == $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x] + 1;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int)

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

 {

     return;

 }

@@ -229,11 +229,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

-procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

+procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);

 

 

 

-implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)

+implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)

 {

   var x: int;

   var __temp_1: int;

@@ -263,60 +263,107 @@ implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)
 

 

 

-procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int);

+procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)

+{

+  var x: int;

+  var y: int;

+

+    x := x$in;

+    y := y$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)

+{

+  var b: bool;

+

+    b := b$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)

+{

+  var c: int;

+

+    c := c$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)

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

 {

   var local_0: int;

   var $tmp6: int;

 

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

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

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

     local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

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

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

     x$out := 3 + RegressionTestInput.Class0.StaticInt;

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

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

     local_0 := x$out;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

     x$out := x$in;

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

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

     x$out := x$out + 1;

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

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

     RegressionTestInput.Class0.StaticInt := x$out;

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

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

     local_0 := x$out;

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

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

     $result := local_0;

     return;

 }

@@ -333,13 +380,13 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int
   var local_0: int;

 

     x := x$in;

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

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

     x := x + 1;

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

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

     RegressionTestInput.Class0.StaticInt := x;

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

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

     local_0 := x;

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

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

     $result := local_0;

     return;

 }

@@ -356,9 +403,9 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
   var local_0: int;

 

     x := x$in;

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

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

     local_0 := x;

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

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

     $result := local_0;

     return;

 }

@@ -376,21 +423,21 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int
   var $tmp7: int;

 

     y := y$in;

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

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

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

     local_0 := $tmp7;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.Class0..ctor$System.Void(this: int)

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

 {

     return;

 }

diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
index 6620b0c4..0487fefc 100644
--- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
+++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
@@ -107,6 +107,9 @@
   <ItemGroup>

     <EmbeddedResource Include="SplitFieldsHeapInput.txt" />

   </ItemGroup>

+  <ItemGroup>

+    <EmbeddedResource Include="TwoDBoxHeapInput.txt" />

+  </ItemGroup>

   <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

        Other similar extension points exist, see Microsoft.Common.targets.

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
index 0b5a0c2d..6d356d4b 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -29,11 +29,11 @@ implementation Alloc() returns (x: int)
 

 var $Heap: HeapType where IsGoodHeap($Heap);

 

-procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int)

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

 {

     return;

 }

@@ -44,11 +44,11 @@ var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
 

 const unique RegressionTestInput.ClassWithBoolTypes.b: bool;

 

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

 {

   var x: int;

   var y: int;

@@ -56,30 +56,30 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int
 

     x := x$in;

     y := y$in;

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

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

     local_0 := x < y;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)

 {

   var z: bool;

 

     z := z$in;

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

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

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

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

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

     if (z)

     {

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

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

         RegressionTestInput.ClassWithBoolTypes.staticB := z;

     }

     else

@@ -91,17 +91,17 @@ implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: in
 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes.Main$System.Void();

+procedure RegressionTestInput.ClassWithBoolTypes.Main();

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.Main$System.Void()

+implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

   var $tmp0: bool;

 

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

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

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

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

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

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

     return;

 }

 

@@ -111,97 +111,97 @@ var RegressionTestInput.ClassWithArrayTypes.s: int;
 

 const unique RegressionTestInput.ClassWithArrayTypes.a: int;

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main1$System.Void();

+procedure RegressionTestInput.ClassWithArrayTypes.Main1();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main1$System.Void()

+implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var local_0: int;

   var $tmp1: int;

   var local_1: int;

   var $tmp2: int;

 

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

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

     call $tmp1 := Alloc();

     local_0 := $tmp1;

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

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

     $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

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

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

     assert $ArrayContents[local_0][0] == 2;

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

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

     call $tmp2 := Alloc();

     local_1 := $tmp2;

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

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

     $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

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

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

     assert $ArrayContents[local_1][0] == 1;

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

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

     assert $ArrayContents[local_0][0] == 2;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main2$System.Void();

+procedure RegressionTestInput.ClassWithArrayTypes.Main2();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main2$System.Void()

+implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

   var $tmp3: int;

   var local_0: int;

   var $tmp4: int;

 

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

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

     call $tmp3 := Alloc();

     RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

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

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

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

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

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

     assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

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

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

     call $tmp4 := Alloc();

     local_0 := $tmp4;

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

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

     $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

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

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

     assert $ArrayContents[local_0][0] == 1;

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

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

     assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int);

+procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int)

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

 {

   var x: int;

 

     x := x$in;

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

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

     $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x := 42]];

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

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

     $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1 := 43]];

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

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

     assert $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1] == $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x] + 1;

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

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

     return;

 }

 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int)

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

 {

     return;

 }

@@ -229,11 +229,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

-procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

+procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);

 

 

 

-implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)

+implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)

 {

   var x: int;

   var __temp_1: int;

@@ -263,60 +263,107 @@ implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)
 

 

 

-procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int);

+procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)

+{

+  var x: int;

+  var y: int;

+

+    x := x$in;

+    y := y$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)

+{

+  var b: bool;

+

+    b := b$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)

+{

+  var c: int;

+

+    c := c$in;

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)

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

 {

   var local_0: int;

   var $tmp6: int;

 

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

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

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

     local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

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

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

     x$out := 3 + RegressionTestInput.Class0.StaticInt;

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

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

     local_0 := x$out;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int);

+procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);

 

 

 

-implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)

 {

   var local_0: int;

 

     x$out := x$in;

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

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

     x$out := x$out + 1;

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

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

     RegressionTestInput.Class0.StaticInt := x$out;

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

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

     local_0 := x$out;

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

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

     $result := local_0;

     return;

 }

@@ -333,13 +380,13 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int
   var local_0: int;

 

     x := x$in;

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

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

     x := x + 1;

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

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

     RegressionTestInput.Class0.StaticInt := x;

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

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

     local_0 := x;

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

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

     $result := local_0;

     return;

 }

@@ -356,9 +403,9 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
   var local_0: int;

 

     x := x$in;

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

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

     local_0 := x;

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

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

     $result := local_0;

     return;

 }

@@ -376,21 +423,21 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int
   var $tmp7: int;

 

     y := y$in;

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

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

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

     local_0 := $tmp7;

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

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

     $result := local_0;

     return;

 }

 

 

 

-procedure RegressionTestInput.Class0..ctor$System.Void(this: int);

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

 

 

 

-implementation RegressionTestInput.Class0..ctor$System.Void(this: int)

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

 {

     return;

 }

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index 179dbb87..d7f2051c 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(assemblyName, heapFactory);

+      BCT.TranslateAssembly(assemblyName, heapFactory, null);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;

@@ -96,6 +96,22 @@ namespace TranslationTest {
         Assert.Fail("Output didn't match SplitFieldsHeapInput.txt: " + resultFile);

       }

     }

+

+    [TestMethod]

+    public void TwoDBoxHeap() {

+      string dir = TestContext.DeploymentDirectory;

+      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

+      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDBoxHeapInput.txt");

+      StreamReader reader = new StreamReader(resource);

+      string expected = reader.ReadToEnd();

+      var result = ExecuteTest(fullPath, new TwoDBoxHeap());

+      if (result != expected) {

+        string resultFile = Path.GetFullPath("TwoDBoxHeapOutput.txt");

+        File.WriteAllText(resultFile, result);

+        Assert.Fail("Output didn't match TwoDBoxHeapHeapInput.txt: " + resultFile);

+      }

+    }

+  

   }

 }

  
\ No newline at end of file