diff options
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 167 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 5 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 469 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/TranslationTest.csproj | 3 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 19 |
5 files changed, 660 insertions, 3 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 33610930..133aeed5 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -354,6 +354,173 @@ procedure {:inline 1} Alloc() returns (x: int) }
+ /// <summary>
+ /// A heap representation that uses Boogie (in-line) functions
+ /// for all heap reads and writes. That way the decision about
+ /// how to exactly represent the heap is made in the Prelude.
+ /// </summary>
+ public class GeneralHeap : HeapFactory, IHeap {
+
+ #region Fields
+
+ [RepresentationFor("Field", "type Field;")]
+ private Bpl.TypeCtorDecl FieldTypeDecl = null;
+ private Bpl.CtorType FieldType;
+
+ [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
+ private Bpl.Variable HeapVariable = null;
+
+ [RepresentationFor("Box2Int", "function Box2Int(box): int;")]
+ private Bpl.Function Box2Int = null;
+
+ [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]
+ private Bpl.Function Box2Bool = null;
+
+ [RepresentationFor("Int2Box", "function Int2Box(int): box;")]
+ private Bpl.Function Int2Box = null;
+
+ [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]
+ private Bpl.Function Bool2Box = null;
+
+ [RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:ref, f:Field): box { H[o, f] }")]
+ private Bpl.Function Read = null;
+
+ [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:ref, f:Field, v:box): HeapType { H[o,f := v] }")]
+ private Bpl.Function Write = null;
+
+ /// <summary>
+ /// Prelude text for which access to the ASTs is not needed
+ /// </summary>
+ private readonly string InitialPreludeText =
+ @"const null: ref;
+type box;
+type ref = int;
+type HeapType = [ref,Field]box;
+function IsGoodHeap(HeapType): bool;
+var $ArrayContents: [int][int]int;
+var $ArrayLength: [int]int;
+
+var $Alloc: [ref] bool;
+procedure {:inline 1} Alloc() returns (x: ref)
+ free ensures x != null;
+ modifies $Alloc;
+{
+ assume $Alloc[x] == false;
+ $Alloc[x] := true;
+}
+";
+ private Sink sink;
+
+ #endregion
+
+ public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
+ this.sink = sink;
+ heap = this;
+ program = null;
+ var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ if (b) {
+ this.FieldType = new Bpl.CtorType(this.FieldTypeDecl.tok, this.FieldTypeDecl, new Bpl.TypeSeq());
+ }
+ return b;
+ }
+
+ /// <summary>
+ /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
+ /// on its type based on the heap representation.
+ /// </summary>
+ public Bpl.Variable CreateFieldVariable(IFieldReference field) {
+ Bpl.Variable v;
+ string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ Bpl.IToken tok = field.Token();
+
+ if (field.IsStatic) {
+ Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.GlobalVariable(tok, tident);
+ } else {
+ Bpl.Type t = this.FieldType;
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.Constant(tok, tident, true);
+ }
+ this.underlyingTypes.Add(v, field.Type);
+ return v;
+ }
+ private Dictionary<Bpl.Variable, ITypeReference> underlyingTypes = new Dictionary<Bpl.Variable, ITypeReference>();
+
+ /// <summary>
+ /// Returns the (typed) BPL expression that corresponds to the value of the field
+ /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
+ /// <paramref name="o"/> is non-null, otherwise the value of the static field.
+ /// </summary>
+ /// <param name="o">The expression that represents the object to be dereferenced.
+ /// Null if <paramref name="f"/> is a static field.
+ /// </param>
+ /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
+ /// it is not null. Otherwise the static field whose value should be read.
+ /// </param>
+ public Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
+ // $Read($Heap, o, f)
+ var callRead = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(this.Read),
+ new Bpl.ExprSeq(new Bpl.IdentifierExpr(f.tok, this.HeapVariable), o, f)
+ );
+ // wrap it in the right conversion function
+ Bpl.Function conversion;
+ var originalType = this.underlyingTypes[f.Decl];
+ var boogieType = TranslationHelper.CciTypeToBoogie(originalType);
+ if (boogieType == Bpl.Type.Bool)
+ conversion = this.Box2Bool;
+ else if (boogieType == Bpl.Type.Int)
+ conversion = this.Box2Int;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+ var callExpr = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(callRead)
+ );
+ return callExpr;
+
+ }
+
+ /// <summary>
+ /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
+ /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
+ /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
+ /// field.
+ /// </summary>
+ public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
+ if (o == null) {
+ return Bpl.Cmd.SimpleAssign(tok, f, value);
+ } else {
+ // wrap it in the right conversion function
+ Bpl.Function conversion;
+ if (value.Type == Bpl.Type.Bool)
+ conversion = this.Bool2Box;
+ else if (value.Type == Bpl.Type.Int)
+ conversion = this.Int2Box;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+
+ var callConversion = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(value)
+ );
+ // $Write($Heap, o, f)
+ var h = new Bpl.IdentifierExpr(f.tok, this.HeapVariable);
+ var callWrite = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(this.Write),
+ new Bpl.ExprSeq(h, o, f, callConversion)
+ );
+ return Bpl.Cmd.SimpleAssign(f.tok, h, callWrite);
+ }
+ }
+
+ }
+
internal class RepresentationFor : Attribute {
internal string name;
internal string declaration;
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 09a82009..99528902 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -25,7 +25,7 @@ namespace BytecodeTranslator { [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
- public enum HeapRepresentation { splitFields, twoDInt, twoDBox }
+ public enum HeapRepresentation { splitFields, twoDInt, twoDBox, general }
[OptionDescription("Heap representation to use", ShortForm = "heap")]
public HeapRepresentation heapRepresentation = HeapRepresentation.twoDInt;
@@ -63,6 +63,9 @@ namespace BytecodeTranslator { case Options.HeapRepresentation.twoDBox:
heap = new TwoDBoxHeap();
break;
+ case Options.HeapRepresentation.general:
+ heap = new GeneralHeap();
+ break;
default:
Console.WriteLine("Unknown setting for /heap");
return 1;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt new file mode 100644 index 00000000..de33bdc0 --- /dev/null +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -0,0 +1,469 @@ +// Copyright (c) 2010, Microsoft Corp.
+// Bytecode Translator prelude
+
+const null: ref;
+
+type box;
+
+type ref = int;
+
+type HeapType = [ref,Field]box;
+
+function IsGoodHeap(HeapType) : bool;
+
+var $ArrayContents: [int][int]int;
+
+var $ArrayLength: [int]int;
+
+var $Alloc: [ref]bool;
+
+procedure {:inline 1} Alloc() returns (x: ref);
+ modifies $Alloc;
+ free ensures x != null;
+
+
+
+implementation Alloc() returns (x: ref)
+{
+ assume $Alloc[x] == false;
+ $Alloc[x] := true;
+}
+
+
+
+type Field;
+
+var $Heap: HeapType where IsGoodHeap($Heap);
+
+function Box2Int(box) : int;
+
+function Box2Bool(box) : bool;
+
+function Int2Box(int) : box;
+
+function Bool2Box(bool) : box;
+
+function {:inline true} Read(H: HeapType, o: ref, f: Field) : box
+{
+ H[o, f]
+}
+
+function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType
+{
+ H[o, f := v]
+}
+
+procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
+{
+ return;
+}
+
+
+
+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;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
+ $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
+ 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;
+}
+
+
+
+var RegressionTestInput.ClassWithArrayTypes.s: int;
+
+const unique RegressionTestInput.ClassWithArrayTypes.a: Field;
+
+procedure RegressionTestInput.ClassWithArrayTypes.Main1();
+
+
+
+implementation RegressionTestInput.ClassWithArrayTypes.Main1()
+{
+ var local_0: int;
+ var $tmp1: int;
+ var local_1: int;
+ var $tmp2: int;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
+ call $tmp1 := Alloc();
+ local_0 := $tmp1;
+ 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;
+ 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;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;
+ assert $ArrayContents[local_0][0] == 2;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithArrayTypes.Main2();
+
+
+
+implementation RegressionTestInput.ClassWithArrayTypes.Main2()
+{
+ var $tmp3: int;
+ var local_0: int;
+ var $tmp4: int;
+
+ assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
+ call $tmp3 := Alloc();
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ 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;
+ 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;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;
+ assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);
+
+
+
+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)
+{
+ var x: int;
+
+ x := x$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;
+ $ArrayContents := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x := 42]];
+ 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;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
+{
+ return;
+}
+
+
+
+var RegressionTestInput.Class0.StaticInt: int;
+
+procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);
+
+
+
+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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);
+
+
+
+implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
+{
+ var x: int;
+ var __temp_1: int;
+ var $tmp5: int;
+ var __temp_2: int;
+ var __temp_3: int;
+ var local_0: int;
+
+ x := x$in;
+ $tmp5 := x;
+ assert $tmp5 != 0;
+ __temp_1 := 5 / $tmp5;
+ __temp_2 := 3;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 21} true;
+ __temp_3 := __temp_2;
+ x := __temp_3;
+ local_0 := __temp_1 + __temp_2;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
+ assert x == 3 && local_0 <= 8;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
+ RegressionTestInput.Class0.StaticInt := local_0;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
+ assert local_0 == RegressionTestInput.Class0.StaticInt;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);
+
+
+
+implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);
+
+
+
+implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)
+{
+ var b: bool;
+
+ b := b$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);
+
+
+
+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)
+{
+ var c: int;
+
+ c := c$in;
+ assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
+{
+ var local_0: int;
+ var $tmp6: 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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int);
+
+
+
+implementation RegressionTestInput.Class0.OutParam$System.Int32@(this: int) returns (x$out: int, $result: int)
+{
+ 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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int);
+
+
+
+implementation RegressionTestInput.Class0.RefParam$System.Int32@(this: int, x$in: int) returns (x$out: int, $result: int)
+{
+ 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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);
+
+
+
+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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);
+
+
+
+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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)
+{
+ var y: int;
+ var local_0: int;
+ var $tmp7: 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;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.Class0.#ctor(this: int)
+{
+ return;
+}
+
+
diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj index 0487fefc..cef103b7 100644 --- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj +++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj @@ -110,6 +110,9 @@ <ItemGroup>
<EmbeddedResource Include="TwoDBoxHeapInput.txt" />
</ItemGroup>
+ <ItemGroup>
+ <EmbeddedResource Include="GeneralHeapInput.txt" />
+ </ItemGroup>
<Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index d7f2051c..9d7f9204 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -108,10 +108,25 @@ namespace TranslationTest { if (result != expected) {
string resultFile = Path.GetFullPath("TwoDBoxHeapOutput.txt");
File.WriteAllText(resultFile, result);
- Assert.Fail("Output didn't match TwoDBoxHeapHeapInput.txt: " + resultFile);
+ Assert.Fail("Output didn't match TwoDBoxHeapInput.txt: " + resultFile);
}
}
-
+
+ [TestMethod]
+ public void GeneralHeap() {
+ string dir = TestContext.DeploymentDirectory;
+ var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
+ Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.GeneralHeapInput.txt");
+ StreamReader reader = new StreamReader(resource);
+ string expected = reader.ReadToEnd();
+ var result = ExecuteTest(fullPath, new GeneralHeap());
+ if (result != expected) {
+ string resultFile = Path.GetFullPath("GeneralHeapOutput.txt");
+ File.WriteAllText(resultFile, result);
+ Assert.Fail("Output didn't match GeneralHeapInput.txt: " + resultFile);
+ }
+ }
+
}
}
\ No newline at end of file |