summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs13
-rw-r--r--BCT/BytecodeTranslator/Sink.cs8
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs15
-rw-r--r--BCT/RegressionTests/RegressionTestInput/Class1.cs6
-rw-r--r--BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt115
-rw-r--r--BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt115
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;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-27 22:53:55 +0000