diff options
| author |  Unknown <mbarnett@MBARNETT-LAP2.redmond.corp.microsoft.com> | 2011-04-12 09:40:47 -0700 |
|---|---|---|
| committer | Unknown <mbarnett@MBARNETT-LAP2.redmond.corp.microsoft.com> | 2011-04-12 09:40:47 -0700 |
| commit | 5e46321a3401b01fafe487c91f70d906d1ff0cf5 (patch) | |
| tree | e6470912cd08839eea8037ef5296c0783fb549b1 | |
| parent | 988738952e291361d7f301a179159ffdbbd5374f (diff) | |
Fix stub support (still not completely finished).
Fix generation of delegate methods so that they happen after translating all
input assemblies and not per assembly.
Fix translation of typeof() expressions.
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 8 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 3 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 151 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 166 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 394 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 394 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt | 394 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt | 394 |
8 files changed, 903 insertions, 1001 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 4281d81b..40e13f8a 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -916,7 +916,13 @@ namespace BytecodeTranslator public override void Visit(ITypeOf typeOf) {
var v = this.sink.FindOrCreateType(typeOf.TypeToGet);
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(typeOf.Token(), v));
+ var callTypeOf = new Bpl.NAryExpr(
+ typeOf.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.TypeOfFunction),
+ new Bpl.ExprSeq(new Bpl.IdentifierExpr(typeOf.Token(), v))
+ );
+ TranslatedExpressions.Push(callTypeOf);
+ //TranslatedExpressions.Push(new Bpl.IdentifierExpr(typeOf.Token(), v));
return;
}
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 78be9b53..464846d4 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -116,6 +116,9 @@ namespace BytecodeTranslator { return callDynamicType;
}
+ [RepresentationFor("$TypeOf", "function $TypeOf(Type): ref;")]
+ public Bpl.Function TypeOfFunction = null;
+
protected readonly string DelegateEncodingText =
@"procedure DelegateAdd(a: int, b: int) returns (c: int)
{
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 58b29d81..2a984cfb 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -47,157 +47,6 @@ namespace BytecodeTranslator { public override void Visit(IAssembly assembly) {
base.Visit(assembly);
- foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys)
- {
- CreateDispatchMethod(type);
- }
- }
-
- private Bpl.IfCmd BuildReturnCmd(Bpl.Expr b) {
- Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
- ifStmtBuilder.Add(new Bpl.ReturnCmd(b.tok));
- return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);
- }
-
- private Bpl.IfCmd BuildIfCmd(Bpl.Expr b, Bpl.Cmd cmd, Bpl.IfCmd ifCmd)
- {
- Bpl.StmtListBuilder ifStmtBuilder;
- ifStmtBuilder = new Bpl.StmtListBuilder();
- ifStmtBuilder.Add(cmd);
- return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), ifCmd, null);
- }
-
- private void CreateDispatchMethod(ITypeDefinition type)
- {
- Contract.Assert(type.IsDelegate);
- IMethodDefinition invokeMethod = null;
- foreach (IMethodDefinition m in type.Methods)
- {
- if (m.Name.Value == "Invoke")
- {
- invokeMethod = m;
- break;
- }
- }
-
- try
- {
- var decl = this.sink.FindOrCreateProcedure(invokeMethod);
- var proc = decl as Bpl.Procedure;
- var invars = proc.InParams;
- var outvars = proc.OutParams;
-
- Bpl.IToken token = invokeMethod.Token();
-
- Bpl.Formal method = new Bpl.Formal(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int), true);
- Bpl.Formal receiver = new Bpl.Formal(token, new Bpl.TypedIdent(token, "receiver", Bpl.Type.Int), true);
-
- Bpl.VariableSeq dispatchProcInvars = new Bpl.VariableSeq();
- dispatchProcInvars.Add(method);
- dispatchProcInvars.Add(receiver);
- for (int i = 1; i < invars.Length; i++) {
- Bpl.Variable f = invars[i];
- dispatchProcInvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), true));
- }
-
- Bpl.VariableSeq dispatchProcOutvars = new Bpl.VariableSeq();
- foreach (Bpl.Formal f in outvars) {
- dispatchProcOutvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), false));
- }
-
- Bpl.Procedure dispatchProc =
- new Bpl.Procedure(token,
- "DispatchOne." + proc.Name,
- new Bpl.TypeVariableSeq(),
- dispatchProcInvars,
- dispatchProcOutvars,
- new Bpl.RequiresSeq(),
- new Bpl.IdentifierExprSeq(),
- new Bpl.EnsuresSeq());
- this.sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProc);
-
- Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);
- foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) {
- Bpl.ExprSeq ins = new Bpl.ExprSeq();
- Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
- if (!defn.IsStatic)
- ins.Add(Bpl.Expr.Ident(receiver));
- int index;
- for (index = 2; index < dispatchProcInvars.Length; index++) {
- ins.Add(Bpl.Expr.Ident(dispatchProcInvars[index]));
- }
- for (index = 0; index < dispatchProcOutvars.Length; index++) {
- outs.Add(Bpl.Expr.Ident(dispatchProcOutvars[index]));
- }
- Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn);
- Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c));
- Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs);
- ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd);
- }
- Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
- ifStmtBuilder.Add(ifCmd);
- Bpl.Implementation dispatchImpl =
- new Bpl.Implementation(token,
- dispatchProc.Name,
- new Bpl.TypeVariableSeq(),
- dispatchProc.InParams,
- dispatchProc.OutParams,
- new Bpl.VariableSeq(),
- ifStmtBuilder.Collect(token)
- );
- dispatchImpl.Proc = dispatchProc;
- this.sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchImpl);
-
- Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", Bpl.Type.Int));
- Bpl.LocalVariable niter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "niter", Bpl.Type.Int));
-
- Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder();
- implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0]))));
-
- Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder();
- whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(niter), this.sink.ReadNext(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(iter))));
- whileStmtBuilder.Add(BuildReturnCmd(Bpl.Expr.Eq(Bpl.Expr.Ident(niter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0])))));
- Bpl.ExprSeq inExprs = new Bpl.ExprSeq();
- inExprs.Add(this.sink.ReadMethod(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)));
- inExprs.Add(this.sink.ReadReceiver(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)));
- for (int i = 1; i < invars.Length; i++) {
- Bpl.Variable f = invars[i];
- inExprs.Add(Bpl.Expr.Ident(f));
- }
- Bpl.IdentifierExprSeq outExprs = new Bpl.IdentifierExprSeq();
- foreach (Bpl.Formal f in outvars) {
- outExprs.Add(Bpl.Expr.Ident(f));
- }
- whileStmtBuilder.Add(new Bpl.CallCmd(token, dispatchProc.Name, inExprs, outExprs));
- whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), Bpl.Expr.Ident(niter)));
- Bpl.WhileCmd whileCmd = new Bpl.WhileCmd(token, Bpl.Expr.True, new List<Bpl.PredicateCmd>(), whileStmtBuilder.Collect(token));
-
- implStmtBuilder.Add(whileCmd);
-
- Bpl.Implementation impl =
- new Bpl.Implementation(token,
- proc.Name,
- new Bpl.TypeVariableSeq(),
- invars,
- outvars,
- new Bpl.VariableSeq(iter, niter),
- implStmtBuilder.Collect(token)
- );
- impl.Proc = proc;
- this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
- }
- catch (TranslationException te)
- {
- throw new NotImplementedException(te.ToString());
- }
- catch
- {
- throw;
- }
- finally
- {
- // Maybe this is a good place to add the procedure to the toplevel declarations
- }
}
/// <summary>
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index c5734d0f..387e6134 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -16,6 +16,7 @@ using Microsoft.Cci.MutableContracts; using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
+using Microsoft.Cci.MutableCodeModel.Contracts;
namespace BytecodeTranslator {
@@ -133,10 +134,15 @@ namespace BytecodeTranslator { pdbReader = new PdbReader(pdbStream, host);
}
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
- var reparenter = new Reparent(host,
+
+ var copier = new CodeDeepCopier(host);
+ var mutableModule = copier.Copy(module);
+
+ var mutator = new ReparentModule(host,
TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType),
- module);
- module = reparenter.Visit(module);
+ mutableModule);
+ module = mutator.Rewrite(mutableModule);
+
modules.Add(Tuple.Create(module, pdbReader));
}
}
@@ -171,6 +177,10 @@ namespace BytecodeTranslator { }
+ foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {
+ CreateDispatchMethod(sink, type);
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
@@ -186,26 +196,156 @@ namespace BytecodeTranslator { return name.Substring(0, i);
}
- private class Reparent : CodeAndContractMutatingVisitor {
+ private class ReparentModule : CodeRewriter {
private IUnit targetUnit;
private IUnit sourceUnit;
- public Reparent(IMetadataHost host, IUnit targetUnit, IUnit sourceUnit)
+ public ReparentModule(IMetadataHost host, IUnit targetUnit, IUnit sourceUnit)
: base(host) {
this.targetUnit = targetUnit;
this.sourceUnit = sourceUnit;
}
- public override IRootUnitNamespace Visit(IRootUnitNamespace rootUnitNamespace) {
- return new RootUnitNamespace() {
- Attributes = new List<ICustomAttribute>(rootUnitNamespace.Attributes),
- Locations = new List<ILocation>(rootUnitNamespace.Locations),
- Members = new List<INamespaceMember>(rootUnitNamespace.Members),
- Name = rootUnitNamespace.Name,
- Unit = this.targetUnit,
- };
+ public override void RewriteChildren(RootUnitNamespace rootUnitNamespace) {
+ if (rootUnitNamespace.Unit.UnitIdentity.Equals(this.sourceUnit.UnitIdentity))
+ rootUnitNamespace.Unit = this.targetUnit;
+ base.RewriteChildren(rootUnitNamespace);
}
+
}
+ private static Bpl.IfCmd BuildIfCmd(Bpl.Expr b, Bpl.Cmd cmd, Bpl.IfCmd ifCmd) {
+ Bpl.StmtListBuilder ifStmtBuilder;
+ ifStmtBuilder = new Bpl.StmtListBuilder();
+ ifStmtBuilder.Add(cmd);
+ return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), ifCmd, null);
+ }
+ private static Bpl.IfCmd BuildReturnCmd(Bpl.Expr b) {
+ Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
+ ifStmtBuilder.Add(new Bpl.ReturnCmd(b.tok));
+ return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);
+ }
+ private static void CreateDispatchMethod(Sink sink, ITypeDefinition type) {
+ Contract.Assert(type.IsDelegate);
+ IMethodDefinition invokeMethod = null;
+ foreach (IMethodDefinition m in type.Methods) {
+ if (m.Name.Value == "Invoke") {
+ invokeMethod = m;
+ break;
+ }
+ }
+
+ try {
+ var decl = sink.FindOrCreateProcedure(invokeMethod);
+ var proc = decl as Bpl.Procedure;
+ var invars = proc.InParams;
+ var outvars = proc.OutParams;
+
+ Bpl.IToken token = invokeMethod.Token();
+
+ Bpl.Formal method = new Bpl.Formal(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int), true);
+ Bpl.Formal receiver = new Bpl.Formal(token, new Bpl.TypedIdent(token, "receiver", Bpl.Type.Int), true);
+
+ Bpl.VariableSeq dispatchProcInvars = new Bpl.VariableSeq();
+ dispatchProcInvars.Add(method);
+ dispatchProcInvars.Add(receiver);
+ for (int i = 1; i < invars.Length; i++) {
+ Bpl.Variable f = invars[i];
+ dispatchProcInvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), true));
+ }
+
+ Bpl.VariableSeq dispatchProcOutvars = new Bpl.VariableSeq();
+ foreach (Bpl.Formal f in outvars) {
+ dispatchProcOutvars.Add(new Bpl.Formal(token, new Bpl.TypedIdent(token, f.Name, f.TypedIdent.Type), false));
+ }
+
+ Bpl.Procedure dispatchProc =
+ new Bpl.Procedure(token,
+ "DispatchOne." + proc.Name,
+ new Bpl.TypeVariableSeq(),
+ dispatchProcInvars,
+ dispatchProcOutvars,
+ new Bpl.RequiresSeq(),
+ new Bpl.IdentifierExprSeq(),
+ new Bpl.EnsuresSeq());
+ sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProc);
+
+ Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);
+ foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) {
+ Bpl.ExprSeq ins = new Bpl.ExprSeq();
+ Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
+ if (!defn.IsStatic)
+ ins.Add(Bpl.Expr.Ident(receiver));
+ int index;
+ for (index = 2; index < dispatchProcInvars.Length; index++) {
+ ins.Add(Bpl.Expr.Ident(dispatchProcInvars[index]));
+ }
+ for (index = 0; index < dispatchProcOutvars.Length; index++) {
+ outs.Add(Bpl.Expr.Ident(dispatchProcOutvars[index]));
+ }
+ Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn);
+ Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c));
+ Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs);
+ ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd);
+ }
+ Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
+ ifStmtBuilder.Add(ifCmd);
+ Bpl.Implementation dispatchImpl =
+ new Bpl.Implementation(token,
+ dispatchProc.Name,
+ new Bpl.TypeVariableSeq(),
+ dispatchProc.InParams,
+ dispatchProc.OutParams,
+ new Bpl.VariableSeq(),
+ ifStmtBuilder.Collect(token)
+ );
+ dispatchImpl.Proc = dispatchProc;
+ sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchImpl);
+
+ Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", Bpl.Type.Int));
+ Bpl.LocalVariable niter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "niter", Bpl.Type.Int));
+
+ Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder();
+ implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), sink.ReadHead(Bpl.Expr.Ident(invars[0]))));
+
+ Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder();
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(niter), sink.ReadNext(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(iter))));
+ whileStmtBuilder.Add(BuildReturnCmd(Bpl.Expr.Eq(Bpl.Expr.Ident(niter), sink.ReadHead(Bpl.Expr.Ident(invars[0])))));
+ Bpl.ExprSeq inExprs = new Bpl.ExprSeq();
+ inExprs.Add(sink.ReadMethod(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)));
+ inExprs.Add(sink.ReadReceiver(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter)));
+ for (int i = 1; i < invars.Length; i++) {
+ Bpl.Variable f = invars[i];
+ inExprs.Add(Bpl.Expr.Ident(f));
+ }
+ Bpl.IdentifierExprSeq outExprs = new Bpl.IdentifierExprSeq();
+ foreach (Bpl.Formal f in outvars) {
+ outExprs.Add(Bpl.Expr.Ident(f));
+ }
+ whileStmtBuilder.Add(new Bpl.CallCmd(token, dispatchProc.Name, inExprs, outExprs));
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), Bpl.Expr.Ident(niter)));
+ Bpl.WhileCmd whileCmd = new Bpl.WhileCmd(token, Bpl.Expr.True, new List<Bpl.PredicateCmd>(), whileStmtBuilder.Collect(token));
+
+ implStmtBuilder.Add(whileCmd);
+
+ Bpl.Implementation impl =
+ new Bpl.Implementation(token,
+ proc.Name,
+ new Bpl.TypeVariableSeq(),
+ invars,
+ outvars,
+ new Bpl.VariableSeq(iter, niter),
+ implStmtBuilder.Collect(token)
+ );
+ impl.Proc = proc;
+ sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
+ } catch (TranslationException te) {
+ throw new NotImplementedException(te.ToString());
+ } catch {
+ throw;
+ } finally {
+ // Maybe this is a good place to add the procedure to the toplevel declarations
+ }
+ }
}
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 2453ca20..703c908f 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -214,6 +214,8 @@ type Type; function $DynamicType(ref) : Type;
+function $TypeOf(Type) : ref;
+
var $Head: [int]int;
var $Next: [int][int]int;
@@ -222,165 +224,6 @@ var $Method: [int][int]int; var $Receiver: [int][int]int;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
- $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-const unique RegressionTestInput.ClassWithBoolTypes.b: Field;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
- var local_0: bool;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;
- local_0 := x < y;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp0: bool;
-
- 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;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: int;
@@ -394,20 +237,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: int;
- var $tmp1: int;
+ var $tmp0: int;
var local_1: int;
- var $tmp2: int;
+ var $tmp1: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- local_0 := $tmp1;
+ call $tmp0 := Alloc();
+ local_0 := $tmp0;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- local_1 := $tmp2;
+ call $tmp1 := Alloc();
+ local_1 := $tmp1;
assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
@@ -426,20 +269,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: int;
+ var $tmp2: int;
var local_0: int;
- var $tmp4: int;
+ var $tmp3: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp2 := Alloc();
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- local_0 := $tmp4;
+ call $tmp3 := Alloc();
+ local_0 := $tmp3;
assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
@@ -501,6 +344,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure System.Object.#ctor(this: int);
+
+
+
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
{
$Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Int2Box(0));
@@ -532,13 +379,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;
- local_0 := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := local_0;
+ $result := x + 1;
return;
}
@@ -552,13 +396,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp4: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp4 := x;
+ assert $tmp4 != 0;
+ __temp_1 := 5 / $tmp4;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
@@ -626,14 +470,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
{
- var local_0: int;
- var $tmp6: int;
+ var $tmp5: int;
- 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 34} true;
- $result := local_0;
+ call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
}
@@ -645,14 +486,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns ( implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
{
- var local_0: int;
-
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -664,17 +501,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: 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 42} true;
x$out := x$out + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -687,17 +520,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -710,13 +540,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -729,15 +556,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 local_0: int;
- var $tmp7: int;
+ var $tmp6: int;
y := y$in;
- 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 60} true;
- $result := local_0;
+ call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp6;
return;
}
@@ -765,3 +589,155 @@ implementation RegressionTestInput.Class0.#cctor() }
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
+{
+ assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
+ assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
+{
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
+ $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.ClassWithBoolTypes: Type;
+
+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
+
+const unique RegressionTestInput.ClassWithBoolTypes.b: Field;
+
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ $result := x < y;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
+{
+ var z: bool;
+
+ z := z$in;
+ $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
+ assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ call System.Object.#ctor(this);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ if (z)
+ {
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ RegressionTestInput.ClassWithBoolTypes.staticB := z;
+ }
+ else
+ {
+ }
+
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.Main();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.Main()
+{
+ var $tmp7: bool;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
+ call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+{
+ RegressionTestInput.ClassWithBoolTypes.staticB := false;
+}
+
+
+
+const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
+
+
+
+procedure System.Attribute.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 0a042d98..5245bf3d 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -192,6 +192,8 @@ type Type; function $DynamicType(ref) : Type;
+function $TypeOf(Type) : ref;
+
var $Head: [int]int;
var $Next: [int][int]int;
@@ -200,165 +202,6 @@ var $Method: [int][int]int; var $Receiver: [int][int]int;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int;
-
-var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;
- RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0;
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-var RegressionTestInput.ClassWithBoolTypes.b: [int]bool;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
- var local_0: bool;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;
- local_0 := x < y;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- RegressionTestInput.ClassWithBoolTypes.b[this] := false;
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- RegressionTestInput.ClassWithBoolTypes.b[this] := z;
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp0: bool;
-
- 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;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: int;
@@ -372,20 +215,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: int;
- var $tmp1: int;
+ var $tmp0: int;
var local_1: int;
- var $tmp2: int;
+ var $tmp1: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- local_0 := $tmp1;
+ call $tmp0 := Alloc();
+ local_0 := $tmp0;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- local_1 := $tmp2;
+ call $tmp1 := Alloc();
+ local_1 := $tmp1;
assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
@@ -404,20 +247,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: int;
+ var $tmp2: int;
var local_0: int;
- var $tmp4: int;
+ var $tmp3: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp2 := Alloc();
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- local_0 := $tmp4;
+ call $tmp3 := Alloc();
+ local_0 := $tmp3;
assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
@@ -479,6 +322,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure System.Object.#ctor(this: int);
+
+
+
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
{
RegressionTestInput.ClassWithArrayTypes.a[this] := 0;
@@ -510,13 +357,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;
- local_0 := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := local_0;
+ $result := x + 1;
return;
}
@@ -530,13 +374,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp4: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp4 := x;
+ assert $tmp4 != 0;
+ __temp_1 := 5 / $tmp4;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
@@ -604,14 +448,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
{
- var local_0: int;
- var $tmp6: int;
+ var $tmp5: int;
- 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 34} true;
- $result := local_0;
+ call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
}
@@ -623,14 +464,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns ( implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
{
- var local_0: int;
-
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -642,17 +479,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: 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 42} true;
x$out := x$out + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -665,17 +498,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -688,13 +518,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -707,15 +534,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 local_0: int;
- var $tmp7: int;
+ var $tmp6: int;
y := y$in;
- 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 60} true;
- $result := local_0;
+ call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp6;
return;
}
@@ -743,3 +567,155 @@ implementation RegressionTestInput.Class0.#cctor() }
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int;
+
+var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
+{
+ assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this];
+ assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
+{
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;
+ RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0;
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.ClassWithBoolTypes: Type;
+
+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
+
+var RegressionTestInput.ClassWithBoolTypes.b: [int]bool;
+
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ $result := x < y;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
+{
+ var z: bool;
+
+ z := z$in;
+ RegressionTestInput.ClassWithBoolTypes.b[this] := false;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ call System.Object.#ctor(this);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ RegressionTestInput.ClassWithBoolTypes.b[this] := z;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ if (z)
+ {
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ RegressionTestInput.ClassWithBoolTypes.staticB := z;
+ }
+ else
+ {
+ }
+
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.Main();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.Main()
+{
+ var $tmp7: bool;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
+ call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+{
+ RegressionTestInput.ClassWithBoolTypes.staticB := false;
+}
+
+
+
+const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
+
+
+
+procedure System.Attribute.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt index 0f3d356b..c23df829 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt @@ -200,6 +200,8 @@ type Type; function $DynamicType(ref) : Type;
+function $TypeOf(Type) : ref;
+
var $Head: [int]int;
var $Next: [int][int]int;
@@ -208,165 +210,6 @@ var $Method: [int][int]int; var $Receiver: [int][int]int;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
- var local_0: bool;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;
- local_0 := x < y;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp0: bool;
-
- 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;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: int;
@@ -380,20 +223,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: int;
- var $tmp1: int;
+ var $tmp0: int;
var local_1: int;
- var $tmp2: int;
+ var $tmp1: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- local_0 := $tmp1;
+ call $tmp0 := Alloc();
+ local_0 := $tmp0;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- local_1 := $tmp2;
+ call $tmp1 := Alloc();
+ local_1 := $tmp1;
assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
@@ -412,20 +255,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: int;
+ var $tmp2: int;
var local_0: int;
- var $tmp4: int;
+ var $tmp3: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp2 := Alloc();
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- local_0 := $tmp4;
+ call $tmp3 := Alloc();
+ local_0 := $tmp3;
assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
@@ -487,6 +330,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure System.Object.#ctor(this: int);
+
+
+
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
{
$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0);
@@ -518,13 +365,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;
- local_0 := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := local_0;
+ $result := x + 1;
return;
}
@@ -538,13 +382,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp4: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp4 := x;
+ assert $tmp4 != 0;
+ __temp_1 := 5 / $tmp4;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
@@ -612,14 +456,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
{
- var local_0: int;
- var $tmp6: int;
+ var $tmp5: int;
- 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 34} true;
- $result := local_0;
+ call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
}
@@ -631,14 +472,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns ( implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
{
- var local_0: int;
-
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -650,17 +487,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: 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 42} true;
x$out := x$out + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -673,17 +506,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -696,13 +526,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -715,15 +542,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 local_0: int;
- var $tmp7: int;
+ var $tmp6: int;
y := y$in;
- 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 60} true;
- $result := local_0;
+ call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp6;
return;
}
@@ -751,3 +575,155 @@ implementation RegressionTestInput.Class0.#cctor() }
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
+{
+ assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));
+ assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
+{
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.ClassWithBoolTypes: Type;
+
+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
+
+const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
+
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ $result := x < y;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
+{
+ var z: bool;
+
+ z := z$in;
+ $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ call System.Object.#ctor(this);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ if (z)
+ {
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ RegressionTestInput.ClassWithBoolTypes.staticB := z;
+ }
+ else
+ {
+ }
+
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.Main();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.Main()
+{
+ var $tmp7: bool;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
+ call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+{
+ RegressionTestInput.ClassWithBoolTypes.staticB := false;
+}
+
+
+
+const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
+
+
+
+procedure System.Attribute.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt index 6a9272de..262958c0 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt @@ -190,6 +190,8 @@ type Type; function $DynamicType(ref) : Type;
+function $TypeOf(Type) : ref;
+
var $Head: [int]int;
var $Next: [int][int]int;
@@ -198,165 +200,6 @@ var $Method: [int][int]int; var $Receiver: [int][int]int;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x];
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0;
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
- var local_0: bool;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;
- local_0 := x < y;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := local_0;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false;
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp0: bool;
-
- 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;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
const unique RegressionTestInput.ClassWithArrayTypes: Type;
var RegressionTestInput.ClassWithArrayTypes.s: int;
@@ -370,20 +213,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: int;
- var $tmp1: int;
+ var $tmp0: int;
var local_1: int;
- var $tmp2: int;
+ var $tmp1: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- local_0 := $tmp1;
+ call $tmp0 := Alloc();
+ local_0 := $tmp0;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- local_1 := $tmp2;
+ call $tmp1 := Alloc();
+ local_1 := $tmp1;
assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
@@ -402,20 +245,20 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: int;
+ var $tmp2: int;
var local_0: int;
- var $tmp4: int;
+ var $tmp3: int;
assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp2 := Alloc();
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
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;
assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- local_0 := $tmp4;
+ call $tmp3 := Alloc();
+ local_0 := $tmp3;
assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
@@ -477,6 +320,10 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure System.Object.#ctor(this: int);
+
+
+
implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
{
$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0;
@@ -508,13 +355,10 @@ procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) return implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;
- local_0 := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := local_0;
+ $result := x + 1;
return;
}
@@ -528,13 +372,13 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp4: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp4 := x;
+ assert $tmp4 != 0;
+ __temp_1 := 5 / $tmp4;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
@@ -602,14 +446,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
{
- var local_0: int;
- var $tmp6: int;
+ var $tmp5: int;
- 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 34} true;
- $result := local_0;
+ call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
return;
}
@@ -621,14 +462,10 @@ procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns ( implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
{
- var local_0: int;
-
assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -640,17 +477,13 @@ procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: 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 42} true;
x$out := x$out + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;
- local_0 := x$out;
assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := local_0;
+ $result := x$out;
return;
}
@@ -663,17 +496,14 @@ procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$i implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -686,13 +516,10 @@ procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepr implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
{
var x: int;
- var local_0: int;
x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;
- local_0 := x;
assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := local_0;
+ $result := x;
return;
}
@@ -705,15 +532,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 local_0: int;
- var $tmp7: int;
+ var $tmp6: int;
y := y$in;
- 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 60} true;
- $result := local_0;
+ call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp6;
return;
}
@@ -741,3 +565,155 @@ implementation RegressionTestInput.Class0.#cctor() }
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
+{
+ assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x];
+ assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
+{
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0;
+ $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0;
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+{
+}
+
+
+
+const unique RegressionTestInput.ClassWithBoolTypes: Type;
+
+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
+
+const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
+
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(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;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
+ $result := x < y;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
+{
+ var z: bool;
+
+ z := z$in;
+ $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ call System.Object.#ctor(this);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ if (z)
+ {
+ assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
+ RegressionTestInput.ClassWithBoolTypes.staticB := z;
+ }
+ else
+ {
+ }
+
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.Main();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.Main()
+{
+ var $tmp7: bool;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
+ call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+
+
+
+implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+{
+ RegressionTestInput.ClassWithBoolTypes.staticB := false;
+}
+
+
+
+const unique RegressionTestInput.AsyncAttribute: Type;
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
+
+
+
+procedure System.Attribute.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
+{
+ call System.Attribute.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.AsyncAttribute.#cctor();
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#cctor()
+{
+}
+
+
|