From c819fabbb8da669952cb7e2e5937c73ff6dcfabe Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 5 Mar 2013 16:58:16 -0800 Subject: Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories. --- BCT/RegressionTests/RegressionTestInput/Class1.cs | 212 --- .../RegressionTestInput/Properties/AssemblyInfo.cs | 36 - .../RegressionTestInput/RegressionTestInput.csproj | 54 - .../TranslationTest/GeneralHeapInput.txt | 1893 -------------------- .../TranslationTest/Properties/AssemblyInfo.cs | 35 - .../TranslationTest/SplitFieldsHeapInput.txt | 1879 ------------------- .../TranslationTest/TranslationTest.csproj | 98 - BCT/RegressionTests/TranslationTest/UnitTest0.cs | 107 -- 8 files changed, 4314 deletions(-) delete mode 100644 BCT/RegressionTests/RegressionTestInput/Class1.cs delete mode 100644 BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs delete mode 100644 BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj delete mode 100644 BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt delete mode 100644 BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs delete mode 100644 BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt delete mode 100644 BCT/RegressionTests/TranslationTest/TranslationTest.csproj delete mode 100644 BCT/RegressionTests/TranslationTest/UnitTest0.cs (limited to 'BCT/RegressionTests') diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs deleted file mode 100644 index 51a4ba86..00000000 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ /dev/null @@ -1,212 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; - -namespace RegressionTestInput { - - [AttributeUsage(AttributeTargets.Method)] - public class AsyncAttribute : Attribute { } - - public class Class0 { - - static int StaticInt; - - static int StaticMethod(int x) { - return x + 1; - } - - void M(int x) { - int y = (5 / x) + (x = 3); - Contract.Assert(x == 3 && y <= 8); - StaticInt = y; - Contract.Assert(y == StaticInt); - } - - // Test to make sure we generate unique procedure names - void M(int x, int y) { } - void M(bool b) { } - void M(Class0 c) { } - - int NonVoid() { - return 3 + StaticInt + StaticMethod(3); - } - - int OutParam(out int x) { - x = 3 + StaticInt; - return x; - } - - int RefParam(ref int x) { - x = x + 1; - StaticInt = x; - return x; - } - - int AssignToInParam(int x) { - x = x + 1; - StaticInt = x; - return x; - } - - [AsyncAttribute] - int MethodThatRepresentsAnAynchronousMethod(int x) { - return x; - } - - int CallAsyncMethod(int y) { - return MethodThatRepresentsAnAynchronousMethod(y); - } - - - } - class ClassWithBoolTypes { - static bool staticB; - bool b; - - static bool M(int x, int y) { - return x < y; - } - - public ClassWithBoolTypes(bool z) { - this.b = z; - if (z) ClassWithBoolTypes.staticB = z; - } - - public static void Main() { - ClassWithBoolTypes.M(3, 4); - } - } - - class ClassWithArrayTypes - { - public static void Main1() - { - int[] s = new int[5]; - s[0] = 2; - Contract.Assert(s[0] == 2); - - int[] t = new int[4]; - t[0] = 1; - Contract.Assert(t[0] == 1); - - Contract.Assert(s[0] == 2); - } - - public static int[] s; - public static void Main2() - { - s = new int[5]; - s[0] = 2; - Contract.Assert(s[0] == 2); - - int[] t = new int[4]; - t[0] = 1; - Contract.Assert(t[0] == 1); - - Contract.Assert(s[0] == 2); - } - - public int[] a; - public void Main3(int x) - { - a[x] = 42; - a[x + 1] = 43; - Contract.Assert(a[x + 1] == a[x] + 1); - } - - public void Main4(int[] xs) { - if (xs != null && xs.Length > 0) { - a[0] = xs[0]; - } - } - } - - public class WriteToTheHeapAValueReadFromTheHeap { - int x; - int y; - public void M() { - this.y = this.x; - } - } - - public struct S { - public int x; - public bool b; - } - - public class CreateStruct { - public S Create() { - var s = new S(); - Contract.Assert(s.x == 0); - Contract.Assert(s.b == false); - return s; - } - S AssignThreeToSDotX(S s) { - s.x = 3; - Contract.Assert(s.x == 3); - return s; - } - - } - - public class RefParameters { - public static void M(ref int x) { - x++; - } - } - - public class RealNumbers { - public void WriteDouble(double d) { - Console.WriteLine(d); - } - public void ObjectToDouble(object o) { - WriteDouble((double)o); - } - public void RealOperations() { - double d = 3.0; - double d2 = 4.0; - WriteDouble(d + d2); - WriteDouble(d - d2); - WriteDouble(d * d2); - WriteDouble(d / d2); - } - } - - public class BitwiseOperations { - public int BitwiseAnd(int x, int y) { return x & y; } - public int BitwiseOr(int x, int y) { return x | y; } - public int ExclusiveOr(int x, int y) { return x ^ y; } - public int BitwiseNegation(int x) { return ~x; } - } - - public class NestedGeneric { - public class C { - public class G where T : new() { - public G(int x) { - var y = new T(); // test to make sure index is calculated correctly for type function - } - } - } - } - public class TestForClassesDifferingOnlyInBeingGeneric { - public int x; - } - - public class TestForClassesDifferingOnlyInBeingGeneric { - public int x; - } - - public struct StructContainingStruct { - public double d; - public S s; - - public StructContainingStruct ReturnCopy(StructContainingStruct s) { - StructContainingStruct t = s; - return t; - } - - } - -} diff --git a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs deleted file mode 100644 index b3cc080a..00000000 --- a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("RegressionTestInput")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("")] -[assembly: AssemblyProduct("RegressionTestInput")] -[assembly: AssemblyCopyright("Copyright © 2010")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("dc8e9afb-ef4e-4954-8f86-1a79bb0d77e4")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("1.0.*")] -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj deleted file mode 100644 index 6cf94c40..00000000 --- a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj +++ /dev/null @@ -1,54 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {3D13D2CC-6387-46FA-BDC2-4BEEFC460118} - Library - Properties - RegressionTestInput - RegressionTestInput - v4.0 - 512 - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt deleted file mode 100644 index 0a2a515a..00000000 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ /dev/null @@ -1,1893 +0,0 @@ -// Copyright (c) 2010, Microsoft Corp. -// Bytecode Translator prelude - -type HeapType = [Ref][Field]Union; - -procedure {:inline 1} Alloc() returns (x: Ref); - modifies $Alloc; - - - -implementation {:inline 1} Alloc() returns (x: Ref) -{ - assume $Alloc[x] == false && x != null; - $Alloc[x] := true; -} - - - -function {:builtin "MapAdd"} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapSub"} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapMul"} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapDiv"} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapMod"} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapConst"} DelegateMapconstint(int) : [Delegate]int; - -function {:builtin "MapConst"} DelegateMapconstbool(bool) : [Delegate]bool; - -function {:builtin "MapAnd"} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapOr"} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapNot"} DelegateMapnot([Delegate]bool) : [Delegate]bool; - -function {:builtin "MapIte"} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapIte"} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapLe"} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapLt"} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapGe"} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapGt"} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapEq"} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapIff"} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapImp"} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -axiom MultisetEmpty == DelegateMapconstint(0); - -function IsRef(u: Union) : bool; - -axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x))); - -axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x))); - -axiom (forall x: Real :: { Real2Union(x) } Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x))); - -axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x))); - -axiom (forall x: Ref :: { Struct2Union(x) } Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x))); - -function $TypeOfInv(Ref) : Type; - -axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t); - -procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref); - - - -implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) -{ - $result := $TypeOf($DynamicType(this)); -} - - - -axiom Union2Int($DefaultHeapValue) == 0; - -axiom Union2Bool($DefaultHeapValue) == false; - -axiom Union2Ref($DefaultHeapValue) == null; - -function $ThreadDelegate(Ref) : Ref; - -procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref) -{ - assume $ThreadDelegate(this) == start$in; -} - - - -procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref) -{ - call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in); -} - - - -procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref); - - - -implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref) -{ - $Exception := null; - call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in); -} - - - -procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref); - - - -procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) -{ - assume $ThreadDelegate(this) == start$in; -} - - - -procedure {:inline 1} System.Threading.Thread.Start(this: Ref); - - - -implementation {:inline 1} System.Threading.Thread.Start(this: Ref) -{ - call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this)); -} - - - -procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref); - - - -implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) -{ - $Exception := null; - call System.Threading.ThreadStart.Invoke(this); -} - - - -procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref); - - - -procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref); - - - -implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref) -{ - var d: Delegate; - - if (a == null) - { - c := b; - } - else if (b == null) - { - c := a; - } - else - { - call c := Alloc(); - assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b); - assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)); - } -} - - - -procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref); - - - -implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref) -{ - var d: Delegate; - - if (a == null) - { - c := null; - } - else if (b == null) - { - c := a; - } - else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty) - { - c := null; - } - else - { - call c := Alloc(); - assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)); - assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0; - } -} - - - -procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref); - - - -implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref) -{ - call c := Alloc(); - assume $RefToDelegate(c) == d; - assume $RefToDelegateMultiset(c) == MultisetSingleton(d); -} - - - -procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); - - - -procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); - - - -implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) -{ - $result := a$in == b$in; -} - - - -implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) -{ - $result := a$in != b$in; -} - - - -var $Heap: HeapType; - -function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Union -{ - H[o][f] -} - -function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Union) : HeapType -{ - H[o := H[o][f := v]] -} - -var $ArrayContents: [Ref][int]Union; - -function $ArrayLength(Ref) : int; - -type {:datatype} Delegate; - -type DelegateMultiset = [Delegate]int; - -const unique MultisetEmpty: DelegateMultiset; - -function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset -{ - MultisetEmpty[x := 1] -} - -function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset -{ - DelegateMapadd(x, y) -} - -function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset -{ - DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0)) -} - -type Field; - -type Union; - -const unique $DefaultHeapValue: Union; - -type Ref; - -const unique null: Ref; - -type {:datatype} Type; - -type Real; - -const unique $DefaultReal: Real; - -procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromBool(b: bool) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Bool2Union(b); -} - - - -procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromInt(i: int) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Int2Union(i); -} - - - -procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref); - - - -implementation {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref) -{ - call rf := Alloc(); - assume $BoxedValue(rf) == Real2Union(r); -} - - - -procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Struct2Union(s); -} - - - -procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) -{ - if (IsRef(u)) - { - r := Union2Ref(u); - } - else - { - call r := Alloc(); - assume $BoxedValue(r) == u; - } -} - - - -function $BoxedValue(r: Ref) : Union; - -function {:inline true} $Unbox2Bool(r: Ref) : bool -{ - Union2Bool($BoxedValue(r)) -} - -function {:inline true} $Unbox2Int(r: Ref) : int -{ - Union2Int($BoxedValue(r)) -} - -function {:inline true} $Unbox2Real(r: Ref) : Real -{ - Union2Real($BoxedValue(r)) -} - -function {:inline true} $Unbox2Struct(r: Ref) : Ref -{ - Union2Struct($BoxedValue(r)) -} - -function {:inline true} $Unbox2Union(r: Ref) : Union -{ - $BoxedValue(r) -} - -function Union2Bool(u: Union) : bool; - -function Union2Int(u: Union) : int; - -function Union2Ref(u: Union) : Ref; - -function Union2Real(u: Union) : Real; - -function Union2Struct(u: Union) : Ref; - -function Bool2Union(boolValue: bool) : Union; - -function Int2Union(intValue: int) : Union; - -function Ref2Union(refValue: Ref) : Union; - -function Real2Union(realValue: Real) : Union; - -function Struct2Union(structValue: Ref) : Union; - -function {:inline true} Union2Union(u: Union) : Union -{ - u -} - -function Int2Real(int) : Real; - -function Real2Int(Real) : int; - -function RealPlus(Real, Real) : Real; - -function RealMinus(Real, Real) : Real; - -function RealTimes(Real, Real) : Real; - -function RealDivide(Real, Real) : Real; - -function RealModulus(Real, Real) : Real; - -function RealLessThan(Real, Real) : bool; - -function RealLessThanOrEqual(Real, Real) : bool; - -function RealGreaterThan(Real, Real) : bool; - -function RealGreaterThanOrEqual(Real, Real) : bool; - -function BitwiseAnd(int, int) : int; - -function BitwiseOr(int, int) : int; - -function BitwiseExclusiveOr(int, int) : int; - -function BitwiseNegation(int) : int; - -function RightShift(int, int) : int; - -function LeftShift(int, int) : int; - -function $DynamicType(Ref) : Type; - -function $TypeOf(Type) : Ref; - -function $As(Ref, Type) : Ref; - -function $Subtype(Type, Type) : bool; - -function $DisjointSubtree(Type, Type) : bool; - -var $Alloc: [Ref]bool; - -function {:builtin "MapImp"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool; - -function {:builtin "MapConst"} $allocConstBool(bool) : [Ref]bool; - -function $RefToDelegate(Ref) : Delegate; - -function $RefToDelegateMultiset(Ref) : DelegateMultiset; - -function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate; - -var {:thread_local} $Exception: Ref; - - - - - -function {:constructor} T$RegressionTestInput.StructContainingStruct() : Type; - -function {:constructor} {:extern} T$System.ValueType() : Type; - -function {:constructor} {:extern} T$System.Object() : Type; - -axiom (forall $T: Type :: { $Subtype(T$System.Object(), $T) } $Subtype(T$System.Object(), $T) <==> T$System.Object() == $T); - -axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T)); - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) } $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) <==> T$RegressionTestInput.StructContainingStruct() == $T || $Subtype(T$System.ValueType(), $T)); - -procedure RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref); - - - -const unique F$RegressionTestInput.StructContainingStruct.d: Field; - -procedure RegressionTestInput.S.#default_ctor($this: Ref); - - - -function {:constructor} T$RegressionTestInput.S() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T)); - -const unique F$RegressionTestInput.StructContainingStruct.s: Field; - -implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref) -{ - var $tmp0: Ref; - - $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.d, Real2Union($DefaultReal)); - call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == T$RegressionTestInput.S(); - $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp0)); -} - - - -procedure RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref); - free ensures this != other; - - - -procedure RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref); - free ensures this != other; - - - -implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref) -{ - var $tmp1: Ref; - - call other := Alloc(); - assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct(); - $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.d, Real2Union(Union2Real(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.d)))); - call $tmp1 := RegressionTestInput.S.#copy_ctor(Union2Ref(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.s))); - $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp1)); -} - - - -procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref) -{ - var s: Ref; - var t_Ref: Ref; - var $localExc: Ref; - var $label: int; - - s := s$in; - assume {:breadcrumb 0} true; - call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s); - $result := t_Ref; - return; -} - - - -function {:constructor} T$RegressionTestInput.RealNumbers() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real) -{ - var d: Real; - var $localExc: Ref; - var $label: int; - - d := d$in; - assume {:breadcrumb 1} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - call System.Console.WriteLine$System.Double(d); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref) -{ - var o: Ref; - var $localExc: Ref; - var $label: int; - - o := o$in; - assume {:breadcrumb 2} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o)); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -const unique $real_literal_3_0: Real; - -const unique $real_literal_4_0: Real; - -implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) -{ - var d_Real: Real; - var d2_Real: Real; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 3} true; - d_Real := $real_literal_3_0; - d2_Real := $real_literal_4_0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Object.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 4} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.RealNumbers.#cctor(); - - - -implementation T$RegressionTestInput.RealNumbers.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) } $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) <==> T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() == $T || $Subtype(T$System.Object(), $T)); - -const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field; - -const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field; - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 5} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true; - assume $this != null; - $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(Union2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x)))); -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Union(0)); - $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(0)); - assume {:breadcrumb 6} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(); - - - -implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.CreateStruct() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.CreateStruct(), $T) } $Subtype(T$RegressionTestInput.CreateStruct(), $T) <==> T$RegressionTestInput.CreateStruct() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -const unique F$RegressionTestInput.S.x: Field; - -const unique F$RegressionTestInput.S.b: Field; - -implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref) -{ - var s_Ref: Ref; - var $tmp0: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 7} true; - call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == T$RegressionTestInput.S(); - s_Ref := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true; - assume s_Ref != null; - assert Union2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true; - assume s_Ref != null; - assert !Union2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b)); - $result := s_Ref; - return; -} - - - -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref) -{ - var s: Ref; - var $localExc: Ref; - var $label: int; - - s := s$in; - assume {:breadcrumb 8} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true; - $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Union(3)); - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true; - assume s != null; - assert Union2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3; - $result := s; - return; -} - - - -procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 9} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.CreateStruct.#cctor(); - - - -implementation T$RegressionTestInput.CreateStruct.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) <==> T$RegressionTestInput.ClassWithArrayTypes() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.ClassWithArrayTypes.s: Ref; - -const unique F$RegressionTestInput.ClassWithArrayTypes.a: Field; - -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main1() -{ - var s_Ref: Ref; - var $tmp0: Ref; - var t_Ref: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 10} true; - call $tmp0 := Alloc(); - assume $ArrayLength($tmp0) == 1 * 5; - s_Ref := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true; - assume s_Ref != null; - assert Union2Int($ArrayContents[s_Ref][0]) == 2; - call $tmp1 := Alloc(); - assume $ArrayLength($tmp1) == 1 * 4; - t_Ref := $tmp1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true; - assume t_Ref != null; - assert Union2Int($ArrayContents[t_Ref][0]) == 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true; - assume s_Ref != null; - assert Union2Int($ArrayContents[s_Ref][0]) == 2; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main2() -{ - var $tmp0: Ref; - var t_Ref: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 11} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true; - call $tmp0 := Alloc(); - assume $ArrayLength($tmp0) == 1 * 5; - F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true; - assume F$RegressionTestInput.ClassWithArrayTypes.s != null; - assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; - call $tmp1 := Alloc(); - assume $ArrayLength($tmp1) == 1 * 4; - t_Ref := $tmp1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true; - assume t_Ref != null; - assert Union2Int($ArrayContents[t_Ref][0]) == 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true; - assume F$RegressionTestInput.ClassWithArrayTypes.s != null; - assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var $tmp0: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 12} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true; - assume $this != null; - $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Union(42)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true; - assume $this != null; - $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Union(43)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true; - assume $this != null; - $tmp0 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)); - assume $tmp0 != null; - assume $this != null; - $tmp1 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)); - assume $tmp1 != null; - assert Union2Int($ArrayContents[$tmp0][x + 1]) == Union2Int($ArrayContents[$tmp1][x]) + 1; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref) -{ - var xs: Ref; - var $localExc: Ref; - var $label: int; - - xs := xs$in; - assume {:breadcrumb 13} true; - if (xs != null) - { - } - else - { - } - - if ((if xs != null then $ArrayLength(xs) > 0 else false)) - { - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true; - assume $this != null; - assume xs != null; - $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]]; - } - else - { - } -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Union(null)); - assume {:breadcrumb 14} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor(); - - - -implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor() -{ - F$RegressionTestInput.ClassWithArrayTypes.s := null; -} - - - -function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type; - -axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) == $T || $Subtype(T$System.Object(), $T)); - -const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field; - -procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Union(0)); - assume {:breadcrumb 15} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor(); - - - -implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) } $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) <==> T$RegressionTestInput.BitwiseOperations() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 16} true; - $result := BitwiseAnd(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 17} true; - $result := BitwiseOr(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 18} true; - $result := BitwiseExclusiveOr(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 19} true; - $result := BitwiseNegation(x); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 20} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.BitwiseOperations.#cctor(); - - - -implementation T$RegressionTestInput.BitwiseOperations.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type; - -function {:constructor} {:extern} T$System.Attribute() : Type; - -function {:constructor} {:extern} T$System.Runtime.InteropServices._Attribute() : Type; - -axiom (forall $T: Type :: { $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) } $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) <==> T$System.Runtime.InteropServices._Attribute() == $T); - -axiom (forall $T: Type :: { $Subtype(T$System.Attribute(), $T) } $Subtype(T$System.Attribute(), $T) <==> T$System.Attribute() == $T || $Subtype(T$System.Object(), $T) || $Subtype(T$System.Runtime.InteropServices._Attribute(), $T)); - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) } $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) <==> T$RegressionTestInput.AsyncAttribute() == $T || $Subtype(T$System.Attribute(), $T)); - -procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Attribute.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 21} true; - call System.Attribute.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.AsyncAttribute.#cctor(); - - - -implementation T$RegressionTestInput.AsyncAttribute.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.RefParameters() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RefParameters(), $T) } $Subtype(T$RegressionTestInput.RefParameters(), $T) <==> T$RegressionTestInput.RefParameters() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 22} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true; - x$out := x$out + 1; -} - - - -procedure RegressionTestInput.RefParameters.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RefParameters.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 23} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.RefParameters.#cctor(); - - - -implementation T$RegressionTestInput.RefParameters.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric(), $T) <==> T$RegressionTestInput.NestedGeneric() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 24} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) <==> T$RegressionTestInput.NestedGeneric.C() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 25} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type; - -axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) <==> T$RegressionTestInput.NestedGeneric.C.G`1(T) == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var CS$0$0000_Union: Union; - var $tmp0: Union; - var $tmp1: Union; - var $tmp2: Ref; - var y_Union: Union; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 26} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - CS$0$0000_Union := $DefaultHeapValue; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - call $tmp2 := $BoxFromUnion(CS$0$0000_Union); - if ($tmp2 != null) - { - } - else - { - call $tmp1 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this))); - $tmp0 := Union2Union($tmp1); - if ($Exception != null) - { - return; - } - } - - y_Union := (if $tmp2 != null then $DefaultHeapValue else $tmp0); -} - - - -procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor() -{ -} - - - -procedure T$RegressionTestInput.NestedGeneric.C.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.C.#cctor() -{ -} - - - -procedure T$RegressionTestInput.NestedGeneric.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.#cctor() -{ -} - - - -implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref) -{ - $Heap := Write($Heap, $this, F$RegressionTestInput.S.x, Int2Union(0)); - $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Union(false)); -} - - - -implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref) -{ - call other := Alloc(); - assume $DynamicType(other) == T$RegressionTestInput.S(); - $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Union(Union2Int(Read($Heap, this, F$RegressionTestInput.S.x)))); - $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Union(Union2Bool(Read($Heap, this, F$RegressionTestInput.S.b)))); -} - - - -function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() == $T || $Subtype(T$System.Object(), $T)); - -const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field; - -procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Union(0)); - assume {:breadcrumb 27} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor(); - - - -implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.Class0() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.Class0(), $T) } $Subtype(T$RegressionTestInput.Class0(), $T) <==> T$RegressionTestInput.Class0() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.Class0.StaticInt: int; - -procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 28} true; - $result := x + 1; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var y_int: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 29} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - x := 3; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - y_int := 3 + 5 / x; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true; - if (x != 3) - { - } - else - { - } - - assert (if x != 3 then false else !(y_int > 8)); - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true; - F$RegressionTestInput.Class0.StaticInt := y_int; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true; - assert y_int == F$RegressionTestInput.Class0.StaticInt; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 30} true; -} - - - -procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool) -{ - var b: bool; - var $localExc: Ref; - var $label: int; - - b := b$in; - assume {:breadcrumb 31} true; -} - - - -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref) -{ - var c: Ref; - var $localExc: Ref; - var $label: int; - - c := c$in; - assume {:breadcrumb 32} true; -} - - - -procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int) -{ - var $tmp0: int; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 33} true; - call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - if ($Exception != null) - { - return; - } - - $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp0; - return; -} - - - -procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 34} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - x$out := 3 + F$RegressionTestInput.Class0.StaticInt; - $result := x$out; - return; -} - - - -procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 35} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - x$out := x$out + 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true; - F$RegressionTestInput.Class0.StaticInt := x$out; - $result := x$out; - return; -} - - - -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 36} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true; - x := x + 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true; - F$RegressionTestInput.Class0.StaticInt := x; - $result := x; - return; -} - - - -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 37} true; - $result := x; - return; -} - - - -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int) -{ - var y: int; - var $tmp0: int; - var $localExc: Ref; - var $label: int; - - y := y$in; - assume {:breadcrumb 38} true; - call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y); - if ($Exception != null) - { - return; - } - - $result := $tmp0; - return; -} - - - -procedure RegressionTestInput.Class0.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 39} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.Class0.#cctor(); - - - -implementation T$RegressionTestInput.Class0.#cctor() -{ - F$RegressionTestInput.Class0.StaticInt := 0; -} - - - -function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) <==> T$RegressionTestInput.ClassWithBoolTypes() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool; - -const unique F$RegressionTestInput.ClassWithBoolTypes.b: Field; - -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 40} true; - $result := x < y; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool) -{ - var z: bool; - var $localExc: Ref; - var $label: int; - - z := z$in; - $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(false)); - assume {:breadcrumb 41} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true; - $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(z)); - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - if (z) - { - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - F$RegressionTestInput.ClassWithBoolTypes.staticB := z; - } - else - { - } -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.Main(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.Main() -{ - var $tmp0: bool; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 42} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true; - call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor(); - - - -implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor() -{ - F$RegressionTestInput.ClassWithBoolTypes.staticB := false; -} - - diff --git a/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs deleted file mode 100644 index a0fd3275..00000000 --- a/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,35 +0,0 @@ -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("TranslationTest")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("")] -[assembly: AssemblyProduct("TranslationTest")] -[assembly: AssemblyCopyright("Copyright © 2010")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// The following GUID is for the ID of the typelib if this project is exposed to COM -[assembly: Guid("f448ac99-c5e7-424c-8bdb-243e8276d4d7")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt deleted file mode 100644 index b552ee36..00000000 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ /dev/null @@ -1,1879 +0,0 @@ -// Copyright (c) 2010, Microsoft Corp. -// Bytecode Translator prelude - -procedure {:inline 1} Alloc() returns (x: Ref); - modifies $Alloc; - - - -implementation {:inline 1} Alloc() returns (x: Ref) -{ - assume $Alloc[x] == false && x != null; - $Alloc[x] := true; -} - - - -function {:builtin "MapAdd"} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapSub"} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapMul"} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapDiv"} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapMod"} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapConst"} DelegateMapconstint(int) : [Delegate]int; - -function {:builtin "MapConst"} DelegateMapconstbool(bool) : [Delegate]bool; - -function {:builtin "MapAnd"} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapOr"} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapNot"} DelegateMapnot([Delegate]bool) : [Delegate]bool; - -function {:builtin "MapIte"} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int; - -function {:builtin "MapIte"} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapLe"} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapLt"} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapGe"} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapGt"} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapEq"} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool; - -function {:builtin "MapIff"} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -function {:builtin "MapImp"} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool; - -axiom MultisetEmpty == DelegateMapconstint(0); - -function IsRef(u: Union) : bool; - -axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x))); - -axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x))); - -axiom (forall x: Real :: { Real2Union(x) } Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x))); - -axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x))); - -axiom (forall x: Ref :: { Struct2Union(x) } Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x))); - -function $TypeOfInv(Ref) : Type; - -axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t); - -procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref); - - - -implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref) -{ - $result := $TypeOf($DynamicType(this)); -} - - - -axiom Union2Int($DefaultHeapValue) == 0; - -axiom Union2Bool($DefaultHeapValue) == false; - -axiom Union2Ref($DefaultHeapValue) == null; - -function $ThreadDelegate(Ref) : Ref; - -procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref) -{ - assume $ThreadDelegate(this) == start$in; -} - - - -procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref) -{ - call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in); -} - - - -procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref); - - - -implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref) -{ - $Exception := null; - call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in); -} - - - -procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref); - - - -procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref); - - - -implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) -{ - assume $ThreadDelegate(this) == start$in; -} - - - -procedure {:inline 1} System.Threading.Thread.Start(this: Ref); - - - -implementation {:inline 1} System.Threading.Thread.Start(this: Ref) -{ - call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this)); -} - - - -procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref); - - - -implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) -{ - $Exception := null; - call System.Threading.ThreadStart.Invoke(this); -} - - - -procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref); - - - -procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref); - - - -implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref) -{ - var d: Delegate; - - if (a == null) - { - c := b; - } - else if (b == null) - { - c := a; - } - else - { - call c := Alloc(); - assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b); - assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)); - } -} - - - -procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref); - - - -implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref) -{ - var d: Delegate; - - if (a == null) - { - c := null; - } - else if (b == null) - { - c := a; - } - else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty) - { - c := null; - } - else - { - call c := Alloc(); - assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)); - assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0; - } -} - - - -procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref); - - - -implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref) -{ - call c := Alloc(); - assume $RefToDelegate(c) == d; - assume $RefToDelegateMultiset(c) == MultisetSingleton(d); -} - - - -procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); - - - -procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); - - - -implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) -{ - $result := a$in == b$in; -} - - - -implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) -{ - $result := a$in != b$in; -} - - - -var $ArrayContents: [Ref][int]Union; - -function $ArrayLength(Ref) : int; - -type {:datatype} Delegate; - -type DelegateMultiset = [Delegate]int; - -const unique MultisetEmpty: DelegateMultiset; - -function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset -{ - MultisetEmpty[x := 1] -} - -function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset -{ - DelegateMapadd(x, y) -} - -function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset -{ - DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0)) -} - -type Field; - -type Union; - -const unique $DefaultHeapValue: Union; - -type Ref; - -const unique null: Ref; - -type {:datatype} Type; - -type Real; - -const unique $DefaultReal: Real; - -procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromBool(b: bool) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Bool2Union(b); -} - - - -procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromInt(i: int) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Int2Union(i); -} - - - -procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref); - - - -implementation {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref) -{ - call rf := Alloc(); - assume $BoxedValue(rf) == Real2Union(r); -} - - - -procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref) -{ - call r := Alloc(); - assume $BoxedValue(r) == Struct2Union(s); -} - - - -procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref); - - - -implementation {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) -{ - if (IsRef(u)) - { - r := Union2Ref(u); - } - else - { - call r := Alloc(); - assume $BoxedValue(r) == u; - } -} - - - -function $BoxedValue(r: Ref) : Union; - -function {:inline true} $Unbox2Bool(r: Ref) : bool -{ - Union2Bool($BoxedValue(r)) -} - -function {:inline true} $Unbox2Int(r: Ref) : int -{ - Union2Int($BoxedValue(r)) -} - -function {:inline true} $Unbox2Real(r: Ref) : Real -{ - Union2Real($BoxedValue(r)) -} - -function {:inline true} $Unbox2Struct(r: Ref) : Ref -{ - Union2Struct($BoxedValue(r)) -} - -function {:inline true} $Unbox2Union(r: Ref) : Union -{ - $BoxedValue(r) -} - -function Union2Bool(u: Union) : bool; - -function Union2Int(u: Union) : int; - -function Union2Ref(u: Union) : Ref; - -function Union2Real(u: Union) : Real; - -function Union2Struct(u: Union) : Ref; - -function Bool2Union(boolValue: bool) : Union; - -function Int2Union(intValue: int) : Union; - -function Ref2Union(refValue: Ref) : Union; - -function Real2Union(realValue: Real) : Union; - -function Struct2Union(structValue: Ref) : Union; - -function {:inline true} Union2Union(u: Union) : Union -{ - u -} - -function Int2Real(int) : Real; - -function Real2Int(Real) : int; - -function RealPlus(Real, Real) : Real; - -function RealMinus(Real, Real) : Real; - -function RealTimes(Real, Real) : Real; - -function RealDivide(Real, Real) : Real; - -function RealModulus(Real, Real) : Real; - -function RealLessThan(Real, Real) : bool; - -function RealLessThanOrEqual(Real, Real) : bool; - -function RealGreaterThan(Real, Real) : bool; - -function RealGreaterThanOrEqual(Real, Real) : bool; - -function BitwiseAnd(int, int) : int; - -function BitwiseOr(int, int) : int; - -function BitwiseExclusiveOr(int, int) : int; - -function BitwiseNegation(int) : int; - -function RightShift(int, int) : int; - -function LeftShift(int, int) : int; - -function $DynamicType(Ref) : Type; - -function $TypeOf(Type) : Ref; - -function $As(Ref, Type) : Ref; - -function $Subtype(Type, Type) : bool; - -function $DisjointSubtree(Type, Type) : bool; - -var $Alloc: [Ref]bool; - -function {:builtin "MapImp"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool; - -function {:builtin "MapConst"} $allocConstBool(bool) : [Ref]bool; - -function $RefToDelegate(Ref) : Delegate; - -function $RefToDelegateMultiset(Ref) : DelegateMultiset; - -function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate; - -var {:thread_local} $Exception: Ref; - - - - - -function {:constructor} T$RegressionTestInput.StructContainingStruct() : Type; - -function {:constructor} {:extern} T$System.ValueType() : Type; - -function {:constructor} {:extern} T$System.Object() : Type; - -axiom (forall $T: Type :: { $Subtype(T$System.Object(), $T) } $Subtype(T$System.Object(), $T) <==> T$System.Object() == $T); - -axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T)); - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) } $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) <==> T$RegressionTestInput.StructContainingStruct() == $T || $Subtype(T$System.ValueType(), $T)); - -procedure RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref); - - - -var F$RegressionTestInput.StructContainingStruct.d: [Ref]Real; - -procedure RegressionTestInput.S.#default_ctor($this: Ref); - - - -function {:constructor} T$RegressionTestInput.S() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T)); - -var F$RegressionTestInput.StructContainingStruct.s: [Ref]Ref; - -implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref) -{ - var $tmp0: Ref; - - F$RegressionTestInput.StructContainingStruct.d[$this] := $DefaultReal; - call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == T$RegressionTestInput.S(); - F$RegressionTestInput.StructContainingStruct.s[$this] := $tmp0; -} - - - -procedure RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref); - free ensures this != other; - - - -procedure RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref); - free ensures this != other; - - - -implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref) -{ - var $tmp1: Ref; - - call other := Alloc(); - assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct(); - F$RegressionTestInput.StructContainingStruct.d[other] := F$RegressionTestInput.StructContainingStruct.d[this]; - call $tmp1 := RegressionTestInput.S.#copy_ctor(F$RegressionTestInput.StructContainingStruct.s[this]); - F$RegressionTestInput.StructContainingStruct.s[other] := $tmp1; -} - - - -procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref) -{ - var s: Ref; - var t_Ref: Ref; - var $localExc: Ref; - var $label: int; - - s := s$in; - assume {:breadcrumb 0} true; - call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s); - $result := t_Ref; - return; -} - - - -function {:constructor} T$RegressionTestInput.RealNumbers() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real) -{ - var d: Real; - var $localExc: Ref; - var $label: int; - - d := d$in; - assume {:breadcrumb 1} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - call System.Console.WriteLine$System.Double(d); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref) -{ - var o: Ref; - var $localExc: Ref; - var $label: int; - - o := o$in; - assume {:breadcrumb 2} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o)); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -const unique $real_literal_3_0: Real; - -const unique $real_literal_4_0: Real; - -implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) -{ - var d_Real: Real; - var d2_Real: Real; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 3} true; - d_Real := $real_literal_3_0; - d2_Real := $real_literal_4_0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real)); - if ($Exception != null) - { - return; - } -} - - - -procedure RegressionTestInput.RealNumbers.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Object.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 4} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.RealNumbers.#cctor(); - - - -implementation T$RegressionTestInput.RealNumbers.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) } $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) <==> T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int; - -var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int; - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 5} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true; - assume $this != null; - F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this]; -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0; - F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0; - assume {:breadcrumb 6} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(); - - - -implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.CreateStruct() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.CreateStruct(), $T) } $Subtype(T$RegressionTestInput.CreateStruct(), $T) <==> T$RegressionTestInput.CreateStruct() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -var F$RegressionTestInput.S.x: [Ref]int; - -var F$RegressionTestInput.S.b: [Ref]bool; - -implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref) -{ - var s_Ref: Ref; - var $tmp0: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 7} true; - call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == T$RegressionTestInput.S(); - s_Ref := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true; - assume s_Ref != null; - assert F$RegressionTestInput.S.x[s_Ref] == 0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true; - assume s_Ref != null; - assert !F$RegressionTestInput.S.b[s_Ref]; - $result := s_Ref; - return; -} - - - -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref); - free ensures $result == null || $Alloc[$result]; - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref) -{ - var s: Ref; - var $localExc: Ref; - var $label: int; - - s := s$in; - assume {:breadcrumb 8} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true; - F$RegressionTestInput.S.x[s] := 3; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true; - assume s != null; - assert F$RegressionTestInput.S.x[s] == 3; - $result := s; - return; -} - - - -procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 9} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.CreateStruct.#cctor(); - - - -implementation T$RegressionTestInput.CreateStruct.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) <==> T$RegressionTestInput.ClassWithArrayTypes() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.ClassWithArrayTypes.s: Ref; - -var F$RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref; - -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main1() -{ - var s_Ref: Ref; - var $tmp0: Ref; - var t_Ref: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 10} true; - call $tmp0 := Alloc(); - assume $ArrayLength($tmp0) == 1 * 5; - s_Ref := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true; - assume s_Ref != null; - assert Union2Int($ArrayContents[s_Ref][0]) == 2; - call $tmp1 := Alloc(); - assume $ArrayLength($tmp1) == 1 * 4; - t_Ref := $tmp1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true; - assume t_Ref != null; - assert Union2Int($ArrayContents[t_Ref][0]) == 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true; - assume s_Ref != null; - assert Union2Int($ArrayContents[s_Ref][0]) == 2; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main2() -{ - var $tmp0: Ref; - var t_Ref: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 11} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true; - call $tmp0 := Alloc(); - assume $ArrayLength($tmp0) == 1 * 5; - F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true; - assume F$RegressionTestInput.ClassWithArrayTypes.s != null; - assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; - call $tmp1 := Alloc(); - assume $ArrayLength($tmp1) == 1 * 4; - t_Ref := $tmp1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true; - assume t_Ref != null; - assert Union2Int($ArrayContents[t_Ref][0]) == 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true; - assume F$RegressionTestInput.ClassWithArrayTypes.s != null; - assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var $tmp0: Ref; - var $tmp1: Ref; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 12} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true; - assume $this != null; - $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x := Int2Union(42)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true; - assume $this != null; - $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Union(43)]]; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true; - assume $this != null; - $tmp0 := F$RegressionTestInput.ClassWithArrayTypes.a[$this]; - assume $tmp0 != null; - assume $this != null; - $tmp1 := F$RegressionTestInput.ClassWithArrayTypes.a[$this]; - assume $tmp1 != null; - assert Union2Int($ArrayContents[$tmp0][x + 1]) == Union2Int($ArrayContents[$tmp1][x]) + 1; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref) -{ - var xs: Ref; - var $localExc: Ref; - var $label: int; - - xs := xs$in; - assume {:breadcrumb 13} true; - if (xs != null) - { - } - else - { - } - - if ((if xs != null then $ArrayLength(xs) > 0 else false)) - { - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true; - assume $this != null; - assume xs != null; - $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]]; - } - else - { - } -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - F$RegressionTestInput.ClassWithArrayTypes.a[$this] := null; - assume {:breadcrumb 14} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor(); - - - -implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor() -{ - F$RegressionTestInput.ClassWithArrayTypes.s := null; -} - - - -function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type; - -axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: [Ref]int; - -procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x[$this] := 0; - assume {:breadcrumb 15} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor(); - - - -implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) } $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) <==> T$RegressionTestInput.BitwiseOperations() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 16} true; - $result := BitwiseAnd(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 17} true; - $result := BitwiseOr(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 18} true; - $result := BitwiseExclusiveOr(x, y); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 19} true; - $result := BitwiseNegation(x); - return; -} - - - -procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 20} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.BitwiseOperations.#cctor(); - - - -implementation T$RegressionTestInput.BitwiseOperations.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type; - -function {:constructor} {:extern} T$System.Attribute() : Type; - -function {:constructor} {:extern} T$System.Runtime.InteropServices._Attribute() : Type; - -axiom (forall $T: Type :: { $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) } $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) <==> T$System.Runtime.InteropServices._Attribute() == $T); - -axiom (forall $T: Type :: { $Subtype(T$System.Attribute(), $T) } $Subtype(T$System.Attribute(), $T) <==> T$System.Attribute() == $T || $Subtype(T$System.Object(), $T) || $Subtype(T$System.Runtime.InteropServices._Attribute(), $T)); - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) } $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) <==> T$RegressionTestInput.AsyncAttribute() == $T || $Subtype(T$System.Attribute(), $T)); - -procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Attribute.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 21} true; - call System.Attribute.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.AsyncAttribute.#cctor(); - - - -implementation T$RegressionTestInput.AsyncAttribute.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.RefParameters() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RefParameters(), $T) } $Subtype(T$RegressionTestInput.RefParameters(), $T) <==> T$RegressionTestInput.RefParameters() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 22} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true; - x$out := x$out + 1; -} - - - -procedure RegressionTestInput.RefParameters.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.RefParameters.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 23} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.RefParameters.#cctor(); - - - -implementation T$RegressionTestInput.RefParameters.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric(), $T) <==> T$RegressionTestInput.NestedGeneric() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 24} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) <==> T$RegressionTestInput.NestedGeneric.C() == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 25} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type; - -axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) <==> T$RegressionTestInput.NestedGeneric.C.G`1(T) == $T || $Subtype(T$System.Object(), $T)); - -procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var CS$0$0000_Union: Union; - var $tmp0: Union; - var $tmp1: Union; - var $tmp2: Ref; - var y_Union: Union; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 26} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - CS$0$0000_Union := $DefaultHeapValue; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true; - call $tmp2 := $BoxFromUnion(CS$0$0000_Union); - if ($tmp2 != null) - { - } - else - { - call $tmp1 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this))); - $tmp0 := Union2Union($tmp1); - if ($Exception != null) - { - return; - } - } - - y_Union := (if $tmp2 != null then $DefaultHeapValue else $tmp0); -} - - - -procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor() -{ -} - - - -procedure T$RegressionTestInput.NestedGeneric.C.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.C.#cctor() -{ -} - - - -procedure T$RegressionTestInput.NestedGeneric.#cctor(); - - - -implementation T$RegressionTestInput.NestedGeneric.#cctor() -{ -} - - - -implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref) -{ - F$RegressionTestInput.S.x[$this] := 0; - F$RegressionTestInput.S.b[$this] := false; -} - - - -implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref) -{ - call other := Alloc(); - assume $DynamicType(other) == T$RegressionTestInput.S(); - F$RegressionTestInput.S.x[other] := F$RegressionTestInput.S.x[this]; - F$RegressionTestInput.S.b[other] := F$RegressionTestInput.S.b[this]; -} - - - -function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int; - -procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0; - assume {:breadcrumb 27} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor(); - - - -implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor() -{ -} - - - -function {:constructor} T$RegressionTestInput.Class0() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.Class0(), $T) } $Subtype(T$RegressionTestInput.Class0(), $T) <==> T$RegressionTestInput.Class0() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.Class0.StaticInt: int; - -procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 28} true; - $result := x + 1; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) -{ - var x: int; - var y_int: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 29} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - x := 3; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true; - y_int := 3 + 5 / x; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true; - if (x != 3) - { - } - else - { - } - - assert (if x != 3 then false else !(y_int > 8)); - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true; - F$RegressionTestInput.Class0.StaticInt := y_int; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true; - assert y_int == F$RegressionTestInput.Class0.StaticInt; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 30} true; -} - - - -procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool) -{ - var b: bool; - var $localExc: Ref; - var $label: int; - - b := b$in; - assume {:breadcrumb 31} true; -} - - - -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref) -{ - var c: Ref; - var $localExc: Ref; - var $label: int; - - c := c$in; - assume {:breadcrumb 32} true; -} - - - -procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int) -{ - var $tmp0: int; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 33} true; - call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - if ($Exception != null) - { - return; - } - - $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp0; - return; -} - - - -procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 34} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - x$out := 3 + F$RegressionTestInput.Class0.StaticInt; - $result := x$out; - return; -} - - - -procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) -{ - var $localExc: Ref; - var $label: int; - - x$out := x$in; - assume {:breadcrumb 35} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; - x$out := x$out + 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true; - F$RegressionTestInput.Class0.StaticInt := x$out; - $result := x$out; - return; -} - - - -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 36} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true; - x := x + 1; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true; - F$RegressionTestInput.Class0.StaticInt := x; - $result := x; - return; -} - - - -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int) -{ - var x: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - assume {:breadcrumb 37} true; - $result := x; - return; -} - - - -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int) -{ - var y: int; - var $tmp0: int; - var $localExc: Ref; - var $label: int; - - y := y$in; - assume {:breadcrumb 38} true; - call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y); - if ($Exception != null) - { - return; - } - - $result := $tmp0; - return; -} - - - -procedure RegressionTestInput.Class0.#ctor($this: Ref); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.Class0.#ctor($this: Ref) -{ - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 39} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.Class0.#cctor(); - - - -implementation T$RegressionTestInput.Class0.#cctor() -{ - F$RegressionTestInput.Class0.StaticInt := 0; -} - - - -function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type; - -axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) <==> T$RegressionTestInput.ClassWithBoolTypes() == $T || $Subtype(T$System.Object(), $T)); - -var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool; - -var F$RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool; - -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) -{ - var x: int; - var y: int; - var $localExc: Ref; - var $label: int; - - x := x$in; - y := y$in; - assume {:breadcrumb 40} true; - $result := x < y; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool) -{ - var z: bool; - var $localExc: Ref; - var $label: int; - - z := z$in; - F$RegressionTestInput.ClassWithBoolTypes.b[$this] := false; - assume {:breadcrumb 41} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor($this); - if ($Exception != null) - { - return; - } - - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true; - F$RegressionTestInput.ClassWithBoolTypes.b[$this] := z; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - if (z) - { - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - F$RegressionTestInput.ClassWithBoolTypes.staticB := z; - } - else - { - } -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.Main(); - free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true); - - - -implementation RegressionTestInput.ClassWithBoolTypes.Main() -{ - var $tmp0: bool; - var $localExc: Ref; - var $label: int; - - assume {:breadcrumb 42} true; - assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true; - assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true; - call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); - if ($Exception != null) - { - return; - } -} - - - -procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor(); - - - -implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor() -{ - F$RegressionTestInput.ClassWithBoolTypes.staticB := false; -} - - diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj deleted file mode 100644 index 446c23b2..00000000 --- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj +++ /dev/null @@ -1,98 +0,0 @@ - - - - Debug - AnyCPU - - - 2.0 - {A112AFBA-D6F6-44A4-A683-C3D458A68D84} - Library - Properties - TranslationTest - TranslationTest - v4.0 - 512 - {3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - - - - ..\..\Binaries\Core.dll - - - - - 3.5 - - - - - False - - - - - - - - - {4A34A3C5-6176-49D7-A4C5-B2B671247F8F} - MetadataHelper - - - {34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5} - PeReader - - - {035FEA7F-0D36-4AE4-B694-EC45191B9AF2} - CodeModel - - - {319E150C-8F33-49E7-81CA-30F02F9BA90A} - MutableCodeModel - - - {A555D4CB-F16F-4049-A8CF-180B8A05C755} - NewILToCodeModel - - - {9C8E4D74-0251-479D-ADAC-A9A469977301} - BytecodeTranslator - - - {3D13D2CC-6387-46FA-BDC2-4BEEFC460118} - RegressionTestInput - - - - - - - - - - - \ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs deleted file mode 100644 index 62ce9155..00000000 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ /dev/null @@ -1,107 +0,0 @@ -using System; -using System.Text; -using System.Collections.Generic; -using System.Linq; -using Microsoft.VisualStudio.TestTools.UnitTesting; -using System.IO; -using Microsoft.Cci; -using Microsoft.Cci.MetadataReader; -using Microsoft.Cci.MutableCodeModel; -using Microsoft.Cci.Contracts; -using Microsoft.Cci.ILToCodeModel; -using BytecodeTranslator; - -namespace TranslationTest { - /// - /// Summary description for UnitTest0 - /// - [TestClass] - public class UnitTest0 { - public UnitTest0() { - // - // TODO: Add constructor logic here - // - } - - private TestContext testContextInstance; - - /// - ///Gets or sets the test context which provides - ///information about and functionality for the current test run. - /// - public TestContext TestContext { - get { - return testContextInstance; - } - set { - testContextInstance = value; - } - } - - #region Additional test attributes - // - // You can use the following additional attributes as you write your tests: - // - // Use ClassInitialize to run code before running the first test in the class - // [ClassInitialize()] - // public static void MyClassInitialize(TestContext testContext) { } - // - // Use ClassCleanup to run code after all tests in a class have run - // [ClassCleanup()] - // public static void MyClassCleanup() { } - // - // Use TestInitialize to run code before running each test - // [TestInitialize()] - // public void MyTestInitialize() { } - // - // Use TestCleanup to run code after each test has run - // [TestCleanup()] - // public void MyTestCleanup() { } - // - #endregion - - private string ExecuteTest(string assemblyName, HeapFactory heapFactory) { - var options = new Options(); - options.monotonicHeap = true; - options.dereference = Options.Dereference.Assume; - BCT.TranslateAssemblyAndWriteOutput(new List { assemblyName }, heapFactory, options, null, false); - var fileName = Path.ChangeExtension(assemblyName, "bpl"); - var s = File.ReadAllText(fileName); - return s; - } - - [TestMethod] - public void SplitFieldsHeap() { - string dir = TestContext.DeploymentDirectory; - var fullPath = Path.Combine(dir, "RegressionTestInput.dll"); - Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.SplitFieldsHeapInput.txt"); - StreamReader reader = new StreamReader(resource); - string expected = reader.ReadToEnd(); - var result = ExecuteTest(fullPath, new SplitFieldsHeap()); - if (result != expected) { - string resultFile = Path.GetFullPath("SplitFieldsHeapOutput.txt"); - File.WriteAllText(resultFile, result); - var msg = String.Format("Output didn't match: SplitFieldsHeapInput.txt \"{0}\"", resultFile); - Assert.Fail(msg); - } - } - - [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); - var msg = String.Format("Output didn't match: GeneralHeapInput.txt \"{0}\"", resultFile); - Assert.Fail(msg); - } - } - - } -} - \ No newline at end of file -- cgit v1.2.3