Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.

8 files changed, 0 insertions, 4314 deletions

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<T> 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<T> {

-    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 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

-  <PropertyGroup>

-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>8.0.30703</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>RegressionTestInput</RootNamespace>

-    <AssemblyName>RegressionTestInput</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-  </PropertyGroup>

-  <ItemGroup>

-    <Reference Include="System" />

-    <Reference Include="System.Core" />

-    <Reference Include="System.Xml.Linq" />

-    <Reference Include="System.Data.DataSetExtensions" />

-    <Reference Include="Microsoft.CSharp" />

-    <Reference Include="System.Data" />

-    <Reference Include="System.Xml" />

-  </ItemGroup>

-  <ItemGroup>

-    <Compile Include="Class1.cs" />

-    <Compile Include="Properties\AssemblyInfo.cs" />

-  </ItemGroup>

-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

-       Other similar extension points exist, see Microsoft.Common.targets.

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

-</Project>
\ 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 @@
-<?xml version="1.0" encoding="utf-8"?>

-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

-  <PropertyGroup>

-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>

-    </ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{A112AFBA-D6F6-44A4-A683-C3D458A68D84}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>TranslationTest</RootNamespace>

-    <AssemblyName>TranslationTest</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <ProjectTypeGuids>{3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <DebugType>full</DebugType>

-    <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

-    <DebugType>pdbonly</DebugType>

-    <Optimize>true</Optimize>

-    <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

-    <ErrorReport>prompt</ErrorReport>

-    <WarningLevel>4</WarningLevel>

-  </PropertyGroup>

-  <ItemGroup>

-    <Reference Include="Core">

-      <HintPath>..\..\Binaries\Core.dll</HintPath>

-    </Reference>

-    <Reference Include="Microsoft.VisualStudio.QualityTools.UnitTestFramework, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />

-    <Reference Include="System" />

-    <Reference Include="System.Core">

-      <RequiredTargetFramework>3.5</RequiredTargetFramework>

-    </Reference>

-  </ItemGroup>

-  <ItemGroup>

-    <CodeAnalysisDependentAssemblyPaths Condition=" '$(VS100COMNTOOLS)' != '' " Include="$(VS100COMNTOOLS)..\IDE\PrivateAssemblies">

-      <Visible>False</Visible>

-    </CodeAnalysisDependentAssemblyPaths>

-  </ItemGroup>

-  <ItemGroup>

-    <Compile Include="Properties\AssemblyInfo.cs" />

-    <Compile Include="UnitTest0.cs" />

-  </ItemGroup>

-  <ItemGroup>

-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj">

-      <Project>{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}</Project>

-      <Name>MetadataHelper</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PeReader\PeReader.csproj">

-      <Project>{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}</Project>

-      <Name>PeReader</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\CodeModel\CodeModel.csproj">

-      <Project>{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}</Project>

-      <Name>CodeModel</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\MutableCodeModel\MutableCodeModel.csproj">

-      <Project>{319E150C-8F33-49E7-81CA-30F02F9BA90A}</Project>

-      <Name>MutableCodeModel</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\NewILToCodeModel\NewILToCodeModel.csproj">

-      <Project>{A555D4CB-F16F-4049-A8CF-180B8A05C755}</Project>

-      <Name>NewILToCodeModel</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\..\BytecodeTranslator\BytecodeTranslator.csproj">

-      <Project>{9C8E4D74-0251-479D-ADAC-A9A469977301}</Project>

-      <Name>BytecodeTranslator</Name>

-    </ProjectReference>

-    <ProjectReference Include="..\RegressionTestInput\RegressionTestInput.csproj">

-      <Project>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</Project>

-      <Name>RegressionTestInput</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

-    <EmbeddedResource Include="SplitFieldsHeapInput.txt" />

-  </ItemGroup>

-  <ItemGroup>

-    <EmbeddedResource Include="GeneralHeapInput.txt" />

-  </ItemGroup>

-  <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

-       Other similar extension points exist, see Microsoft.Common.targets.

-  <Target Name="BeforeBuild">

-  </Target>

-  <Target Name="AfterBuild">

-  </Target>

-  -->

-</Project>
\ 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>

-  /// Summary description for UnitTest0

-  /// </summary>

-  [TestClass]

-  public class UnitTest0 {

-    public UnitTest0() {

-      //

-      // TODO: Add constructor logic here

-      //

-    }

-

-    private TestContext testContextInstance;

-

-    /// <summary>

-    ///Gets or sets the test context which provides

-    ///information about and functionality for the current test run.

-    ///</summary>

-    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<string> { 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