Renamed outside of SVN, so added the renamed file and deleting this.

1 files changed, 0 insertions, 398 deletions

diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
deleted file mode 100644
index 0b5a0c2d..00000000
--- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
+++ /dev/null
@@ -1,398 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.

-// Bytecode Translator prelude

-

-const null: int;

-

-type HeapType = [int,int]int;

-

-function IsGoodHeap(HeapType) : bool;

-

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

-

-var $ArrayLength: [int]int;

-

-var $Alloc: [int]bool;

-

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

-  modifies $Alloc;

-  free ensures x != 0;

-

-

-

-implementation Alloc() returns (x: int)

-{

-    assume $Alloc[x] == false;

-    $Alloc[x] := true;

-}

-

-

-

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

-

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

-

-

-

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

-{

-    return;

-}

-

-

-

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

-

-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;

-

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

-

-

-

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(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 64} true;

-    local_0 := x < y;

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

-    $result := local_0;

-    return;

-}

-

-

-

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

-

-

-

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

-{

-  var z: bool;

-

-    z := z$in;

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

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

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

-    if (z)

-    {

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

-        RegressionTestInput.ClassWithBoolTypes.staticB := z;

-    }

-    else

-    {

-    }

-

-    return;

-}

-

-

-

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

-

-

-

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

-{

-  var $tmp0: bool;

-

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

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

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

-    return;

-}

-

-

-

-var RegressionTestInput.ClassWithArrayTypes.s: int;

-

-const unique RegressionTestInput.ClassWithArrayTypes.a: int;

-

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

-

-

-

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

-{

-  var local_0: int;

-  var $tmp1: int;

-  var local_1: int;

-  var $tmp2: int;

-

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

-    call $tmp1 := Alloc();

-    local_0 := $tmp1;

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

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

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

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

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

-    call $tmp2 := Alloc();

-    local_1 := $tmp2;

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

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

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

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

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

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

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

-    return;

-}

-

-

-

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

-

-

-

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

-{

-  var $tmp3: int;

-  var local_0: int;

-  var $tmp4: int;

-

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

-    call $tmp3 := Alloc();

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

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

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

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

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

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

-    call $tmp4 := Alloc();

-    local_0 := $tmp4;

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

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

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

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

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

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

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

-    return;

-}

-

-

-

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

-

-

-

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

-{

-  var x: int;

-

-    x := x$in;

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

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

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

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

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

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

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

-    return;

-}

-

-

-

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

-

-

-

-implementation RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(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.Void(this: int, x$in: int);

-

-

-

-implementation RegressionTestInput.Class0.M$System.Void(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.NonVoid$System.Int32(this: int) returns ($result: int);

-

-

-

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

-{

-  var local_0: int;

-  var $tmp6: int;

-

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

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

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

-    assert {:sourceFile "Class1.cs"} {:sourceLine 29} 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 32} true;

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

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

-    local_0 := x$out;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 34} 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 37} true;

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

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

-    RegressionTestInput.Class0.StaticInt := x$out;

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

-    local_0 := x$out;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 40} 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 43} true;

-    x := x + 1;

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

-    RegressionTestInput.Class0.StaticInt := x;

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

-    local_0 := x;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 46} 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 50} true;

-    local_0 := x;

-    assert {:sourceFile "Class1.cs"} {:sourceLine 51} 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 54} true;

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

-    local_0 := $tmp7;

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

-    $result := local_0;

-    return;

-}

-

-

-

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

-

-

-

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

-{

-    return;

-}

-

-