The decompilation is not guaranteed to get rid of all push statements and pop

expressions. So added support for them.
Simplified the API in the sink for creating a local. Not it takes a CCI type
so clients do not have to first translate the CCI type to the Boogie type.

6 files changed, 202 insertions, 70 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index db9da74c..277374cb 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -140,7 +140,7 @@ namespace BytecodeTranslator
         }

       }

       this.Visit(addressDereference.Address);

-      throw new NotImplementedException();

+      return;

     }

 

     public override void Visit(IArrayIndexer arrayIndexer)

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

           currSelectExpr = Bpl.Expr.Select(currSelectExpr, e);

         }

-        Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.CciTypeToBoogie(arrayIndexer.Type.ResolvedType)));

+        Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(arrayIndexer.Type));

         this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, currSelectExpr));

         TranslatedExpressions.Push(temp);

       }

@@ -359,6 +359,11 @@ namespace BytecodeTranslator
       #endregion

     }

 

+    public override void Visit(IPopValue popValue) {

+      var locExpr = this.StmtTraverser.operandStack.Pop();

+      this.TranslatedExpressions.Push(locExpr);

+    }

+

     /// <summary>

     /// 

     /// </summary>

@@ -444,7 +449,7 @@ namespace BytecodeTranslator
         locals.Add(x);

         for (int i = 0; i < args.Count; i++) {

           Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));

-          Bpl.Variable y = this.sink.CreateFreshLocal(this.sink.CciTypeToBoogie(args[i].Type));

+          Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);

           StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct)));

           x = y;

           locals.Add(y);

@@ -686,7 +691,7 @@ namespace BytecodeTranslator
           locals.Add(x);

           for (int i = 0; i < args.Count; i++) {

             Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));

-            Bpl.Variable y = this.sink.CreateFreshLocal(this.sink.CciTypeToBoogie(args[i].Type));

+            Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);

             StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct)));

             x = y;

             locals.Add(y);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index c8b365ba..b41e3f4f 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -139,14 +139,6 @@ namespace BytecodeTranslator {
       return v;

     }

 

-    public Bpl.Variable CreateFreshLocal(Bpl.Type t) {

-      Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

-      ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

-      return v;

-    }

-

     private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = null;

     public Dictionary<ILocalDefinition, Bpl.LocalVariable> LocalVarMap {

       get { return this.localVarMap; }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index a062fca1..81a2c4e8 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -33,6 +33,7 @@ namespace BytecodeTranslator
 

     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

     private bool contractContext;

+    internal readonly Stack<Bpl.Expr> operandStack = new Stack<Bpl.Expr>();

 

     #region Constructors

     public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

@@ -164,6 +165,20 @@ namespace BytecodeTranslator
       return;

     }

 

+    public override void Visit(IPushStatement pushStatement) {

+      var tok = pushStatement.Token();

+      var val = pushStatement.ValueToPush;

+      var dup = val as IDupValue;

+      Bpl.Expr e;

+      if (dup != null) {

+        e = this.operandStack.Peek();

+      } else {

+        e = ExpressionFor(val);

+      }

+      this.operandStack.Push(e);

+      return;

+    }

+

     /// <summary>

     /// 

     /// </summary>

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 40cf9575..90fa7b50 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -151,4 +151,10 @@ namespace RegressionTestInput {
 

   }

 

+  public class RefParameters {

+    public static void M(ref int x) {

+      x++;

+    }

+  }

+

 }

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 5891b6f5..0ff36879 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -258,8 +258,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
 {

   var local_0: int;

   var $tmp0: int;

-  var local_1: int;

   var $tmp1: int;

+  var local_1: int;

+  var $tmp2: int;

+  var $tmp3: int;

+  var $tmp4: int;

 

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

     call $tmp0 := Alloc();

@@ -267,16 +270,19 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
     assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

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

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

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

+    $tmp1 := $ArrayContents[local_0][0];

+    assert $tmp1 == 2;

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

-    call $tmp1 := Alloc();

-    local_1 := $tmp1;

+    call $tmp2 := Alloc();

+    local_1 := $tmp2;

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

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

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

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

+    $tmp3 := $ArrayContents[local_1][0];

+    assert $tmp3 == 1;

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

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

+    $tmp4 := $ArrayContents[local_0][0];

+    assert $tmp4 == 2;

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

     return;

 }

@@ -289,26 +295,32 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp2: int;

+  var $tmp5: int;

+  var $tmp6: int;

   var local_0: int;

-  var $tmp3: int;

+  var $tmp7: int;

+  var $tmp8: int;

+  var $tmp9: int;

 

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

-    call $tmp2 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp2;

+    call $tmp5 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp5;

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

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

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

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

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

+    assert $tmp6 == 2;

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

-    call $tmp3 := Alloc();

-    local_0 := $tmp3;

+    call $tmp7 := Alloc();

+    local_0 := $tmp7;

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

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

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

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

+    $tmp8 := $ArrayContents[local_0][0];

+    assert $tmp8 == 1;

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

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

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

+    assert $tmp9 == 2;

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

     return;

 }

@@ -322,6 +334,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int,
 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

 {

   var x: int;

+  var $tmp10: int;

+  var $tmp11: int;

 

     x := x$in;

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

@@ -329,7 +343,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this:
     assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;

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

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

-    assert $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1] == $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x] + 1;

+    $tmp10 := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1];

+    $tmp11 := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x];

+    assert $tmp10 == $tmp11 + 1;

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

     return;

 }

@@ -343,12 +359,14 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this:
 implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)

 {

   var xs: int;

+  var $tmp12: int;

 

     xs := xs$in;

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

+        $tmp12 := $ArrayContents[xs][0];

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

     }

     else

     {

@@ -388,6 +406,45 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
 

 

 

+const unique RegressionTestInput.RefParameters: Type;

+

+procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+

+

+

+implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)

+{

+    x$out := x$in;

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

+    x$out := x$out + 1;

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

+    return;

+}

+

+

+

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

+

+

+

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

+{

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RefParameters.#cctor();

+

+

+

+implementation RegressionTestInput.RefParameters.#cctor()

+{

+}

+

+

+

 const unique RegressionTestInput.Class0: Type;

 

 var RegressionTestInput.Class0.StaticInt: int;

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

   var x: int;

   var __temp_1: int;

-  var $tmp4: int;

+  var $tmp13: int;

   var local_0: int;

 

     x := x$in;

-    $tmp4 := x;

-    assert $tmp4 != 0;

-    __temp_1 := 5 / $tmp4;

+    $tmp13 := x;

+    assert $tmp13 != 0;

+    __temp_1 := 5 / $tmp13;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -490,11 +547,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var $tmp5: int;

+  var $tmp14: int;

 

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

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

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

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

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

     return;

 }

 

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

 {

   var y: int;

-  var $tmp6: int;

+  var $tmp15: int;

 

     y := y$in;

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

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

-    $result := $tmp6;

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

+    $result := $tmp15;

     return;

 }

 

@@ -713,10 +770,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp7: bool;

+  var $tmp16: bool;

 

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

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

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

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

     return;

 }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index b6df83bc..53e9a8c3 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -248,8 +248,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
 {

   var local_0: int;

   var $tmp0: int;

-  var local_1: int;

   var $tmp1: int;

+  var local_1: int;

+  var $tmp2: int;

+  var $tmp3: int;

+  var $tmp4: int;

 

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

     call $tmp0 := Alloc();

@@ -257,16 +260,19 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
     assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

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

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

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

+    $tmp1 := $ArrayContents[local_0][0];

+    assert $tmp1 == 2;

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

-    call $tmp1 := Alloc();

-    local_1 := $tmp1;

+    call $tmp2 := Alloc();

+    local_1 := $tmp2;

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

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

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

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

+    $tmp3 := $ArrayContents[local_1][0];

+    assert $tmp3 == 1;

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

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

+    $tmp4 := $ArrayContents[local_0][0];

+    assert $tmp4 == 2;

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

     return;

 }

@@ -279,26 +285,32 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp2: int;

+  var $tmp5: int;

+  var $tmp6: int;

   var local_0: int;

-  var $tmp3: int;

+  var $tmp7: int;

+  var $tmp8: int;

+  var $tmp9: int;

 

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

-    call $tmp2 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp2;

+    call $tmp5 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp5;

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

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

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

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

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

+    assert $tmp6 == 2;

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

-    call $tmp3 := Alloc();

-    local_0 := $tmp3;

+    call $tmp7 := Alloc();

+    local_0 := $tmp7;

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

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

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

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

+    $tmp8 := $ArrayContents[local_0][0];

+    assert $tmp8 == 1;

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

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

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

+    assert $tmp9 == 2;

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

     return;

 }

@@ -312,6 +324,8 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int,
 implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)

 {

   var x: int;

+  var $tmp10: int;

+  var $tmp11: int;

 

     x := x$in;

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

@@ -319,7 +333,9 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this:
     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 116} true;

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

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

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

+    assert $tmp10 == $tmp11 + 1;

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

     return;

 }

@@ -333,12 +349,14 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this:
 implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)

 {

   var xs: int;

+  var $tmp12: int;

 

     xs := xs$in;

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

+        $tmp12 := $ArrayContents[xs][0];

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

     }

     else

     {

@@ -378,6 +396,45 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
 

 

 

+const unique RegressionTestInput.RefParameters: Type;

+

+procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+

+

+

+implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)

+{

+    x$out := x$in;

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

+    x$out := x$out + 1;

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

+    return;

+}

+

+

+

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

+

+

+

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

+{

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

+    return;

+}

+

+

+

+procedure RegressionTestInput.RefParameters.#cctor();

+

+

+

+implementation RegressionTestInput.RefParameters.#cctor()

+{

+}

+

+

+

 const unique RegressionTestInput.Class0: Type;

 

 var RegressionTestInput.Class0.StaticInt: int;

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

   var x: int;

   var __temp_1: int;

-  var $tmp4: int;

+  var $tmp13: int;

   var local_0: int;

 

     x := x$in;

-    $tmp4 := x;

-    assert $tmp4 != 0;

-    __temp_1 := 5 / $tmp4;

+    $tmp13 := x;

+    assert $tmp13 != 0;

+    __temp_1 := 5 / $tmp13;

     x := 3;

     local_0 := __temp_1 + 3;

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

@@ -480,11 +537,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
 

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

 {

-  var $tmp5: int;

+  var $tmp14: int;

 

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

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

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

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

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

     return;

 }

 

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

 {

   var y: int;

-  var $tmp6: int;

+  var $tmp15: int;

 

     y := y$in;

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

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

-    $result := $tmp6;

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

+    $result := $tmp15;

     return;

 }

 

@@ -703,10 +760,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp7: bool;

+  var $tmp16: bool;

 

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

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

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

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

     return;

 }