Boogie: I have successfully ported the AbsInt project. It passes all regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL.

Address any error complaints to t-abarbe@microsoft.com

15 files changed, 1074 insertions, 2584 deletions

diff --git a/Source/AbsInt/..svnbridge/InterimKey.snk b/Source/AbsInt/..svnbridge/InterimKey.snk
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Source/AbsInt/..svnbridge/InterimKey.snk
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index d0efb860..d26f5c60 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -1,124 +1,119 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="AbsInt"

-     ProjectGuid="11d06232-2039-4bca-853b-c596e2a4edb0"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="AbsInt"

-         OutputType="Library"

-         RootNamespace="AbsInt"

-         StartupObject=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-         ShadowedAssembly=""

-         StandardLibraryLocation=""

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="bin\Debug"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           RunProgramVerifier="False"

-           ProgramVerifierCommandLineOptions=""

-           ReferenceTypesAreNonNullByDefault="False"

-           RunProgramVerifierWhileEditing="False"

-           AllowPointersToManagedStructures="False"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="True"

-           WarningLevel="4"

-           />

-      </Settings>

-      <References>

-        <Reference Name="Mscorlib.Contracts"

-             AssemblyName="Mscorlib.Contracts"

-             Private="false"

-             HintPath="../../Binaries/Mscorlib.Contracts.dll"

-             />

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Compiler"

-             AssemblyName="System.Compiler"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.dll"

-             />

-        <Reference Name="System.Compiler.Framework"

-             AssemblyName="System.Compiler.Framework"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.Framework.dll"

-             />

-        <Reference Name="AIFramework"

-             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"

-             Private="true"

-             />

-        <Reference Name="Core"

-             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"

-             Private="true"

-             />

-        <Reference Name="Basetypes"

-             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"

-             Private="true"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="Traverse.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AbstractInterpretation.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="ExprFactories.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="..\version.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="LoopInvariantsOnDemand.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AssemblyInfo.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>
\ No newline at end of file
+<?xml version="1.0" encoding="utf-8"?>

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

+  <PropertyGroup>

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

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

+    <ProductVersion>9.0.30729</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>AbsInt</RootNamespace>

+    <AssemblyName>AbsInt</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

+    <SignAssembly>true</SignAssembly>

+    <AssemblyOriginatorKeyFile>InterimKey.snk</AssemblyOriginatorKeyFile>

+  </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>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly>

+    </CodeContractsCustomRewriterAssembly>

+    <CodeContractsCustomRewriterClass>

+    </CodeContractsCustomRewriterClass>

+    <CodeContractsLibPaths>

+    </CodeContractsLibPaths>

+    <CodeContractsExtraRewriteOptions>

+    </CodeContractsExtraRewriteOptions>

+    <CodeContractsExtraAnalysisOptions>

+    </CodeContractsExtraAnalysisOptions>

+    <CodeContractsBaseLineFile>

+    </CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </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="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\AIFramework.dll</HintPath>

+    </Reference>

+    <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Basetypes.dll</HintPath>

+    </Reference>

+    <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

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

+    </Reference>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Compiler.Framework, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\System.Compiler.Framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Core">

+      <RequiredTargetFramework>3.5</RequiredTargetFramework>

+    </Reference>

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

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

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="AbstractInterpretation.cs" />

+    <Compile Include="cce.cs" />

+    <Compile Include="ExprFactories.cs" />

+    <Compile Include="LoopInvariantsOnDemand.cs" />

+    <Compile Include="Traverse.cs" />

+    <Compile Include="version.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="InterimKey.snk" />

+  </ItemGroup>

+  <ItemGroup>

+    <Folder Include="Properties\" />

+  </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/Source/AbsInt/AbsInt.sscproj b/Source/AbsInt/AbsInt.sscproj
deleted file mode 100644
index d0efb860..00000000
--- a/Source/AbsInt/AbsInt.sscproj
+++ /dev/null
@@ -1,124 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>

-<VisualStudioProject>

-  <XEN ProjectType="Local"

-     SchemaVersion="1.0"

-     Name="AbsInt"

-     ProjectGuid="11d06232-2039-4bca-853b-c596e2a4edb0"

-    >

-    <Build>

-      <Settings ApplicationIcon=""

-         AssemblyName="AbsInt"

-         OutputType="Library"

-         RootNamespace="AbsInt"

-         StartupObject=""

-         TargetPlatform="v2"

-         TargetPlatformLocation=""

-         ShadowedAssembly=""

-         StandardLibraryLocation=""

-        >

-        <Config Name="Debug"

-           AllowUnsafeBlocks="False"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="False"

-           ConfigurationOverrideFile=""

-           DefineConstants="DEBUG;TRACE"

-           DocumentationFile=""

-           DebugSymbols="True"

-           FileAlignment="4096"

-           IncrementalBuild="True"

-           Optimize="False"

-           OutputPath="bin\Debug"

-           RegisterForComInterop="False"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="False"

-           WarningLevel="4"

-           RunProgramVerifier="False"

-           ProgramVerifierCommandLineOptions=""

-           ReferenceTypesAreNonNullByDefault="False"

-           RunProgramVerifierWhileEditing="False"

-           AllowPointersToManagedStructures="False"

-           CheckContractAdmissibility="True"

-           CheckPurity="False"

-           />

-        <Config Name="Release"

-           AllowUnsafeBlocks="false"

-           BaseAddress="285212672"

-           CheckForOverflowUnderflow="false"

-           ConfigurationOverrideFile=""

-           DefineConstants="TRACE"

-           DocumentationFile=""

-           DebugSymbols="false"

-           FileAlignment="4096"

-           IncrementalBuild="false"

-           Optimize="true"

-           OutputPath="bin\release"

-           RegisterForComInterop="false"

-           RemoveIntegerChecks="false"

-           TreatWarningsAsErrors="True"

-           WarningLevel="4"

-           />

-      </Settings>

-      <References>

-        <Reference Name="Mscorlib.Contracts"

-             AssemblyName="Mscorlib.Contracts"

-             Private="false"

-             HintPath="../../Binaries/Mscorlib.Contracts.dll"

-             />

-        <Reference Name="System"

-             AssemblyName="System"

-             Private="false"

-             />

-        <Reference Name="System.Compiler"

-             AssemblyName="System.Compiler"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.dll"

-             />

-        <Reference Name="System.Compiler.Framework"

-             AssemblyName="System.Compiler.Framework"

-             Private="false"

-             HintPath="../../Binaries/System.Compiler.Framework.dll"

-             />

-        <Reference Name="AIFramework"

-             Project="{24B55172-AD8B-47D1-8952-5A95CFDB9B31}"

-             Private="true"

-             />

-        <Reference Name="Core"

-             Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"

-             Private="true"

-             />

-        <Reference Name="Basetypes"

-             Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"

-             Private="true"

-             />

-      </References>

-    </Build>

-    <Files>

-      <Include>

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="Traverse.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AbstractInterpretation.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="ExprFactories.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="..\version.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="LoopInvariantsOnDemand.ssc"

-                 />

-        <File BuildAction="Compile"

-                 SubType="Code"

-                 RelPath="AssemblyInfo.ssc"

-                 />

-      </Include>

-    </Files>

-  </XEN>

-</VisualStudioProject>
\ No newline at end of file
diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index ee5a1f06..bf25434a 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -3,40 +3,53 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-using Microsoft.Contracts;

 

-namespace Microsoft.Boogie.AbstractInterpretation

-{

+namespace Microsoft.Boogie.AbstractInterpretation {

   using System;

   using System.Collections;

-  using System.Collections.Generic;  

+  using System.Collections.Generic;

   using System.Diagnostics;

+  using System.Diagnostics.Contracts;

   using Microsoft.Boogie;

   using Cci = System.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

-  using Microsoft.Contracts;

+

 

   /// <summary>

   /// Defines invariant propagation methods over ASTs for an abstract interpretation policy.

   /// </summary>

-  public class AbstractionEngine 

-  {

-    private AI.Lattice! lattice;

-    private Queue<ProcedureWorkItem!>! procWorkItems;  //PM: changed to generic queue

-    private Queue/*<CallSite>*/! callReturnWorkItems;

+  public class AbstractionEngine {

+    private AI.Lattice lattice;

+    private Queue<ProcedureWorkItem> procWorkItems;  //PM: changed to generic queue

+    private Queue/*<CallSite>*/ callReturnWorkItems;

     private Cci.IRelation/*<Procedure,Implementation>*/ procedureImplementations;

-           

-    private class ProcedureWorkItem

-    {

+

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(lattice != null);

+      Contract.Invariant(procWorkItems != null);

+      Contract.Invariant(callReturnWorkItems != null);

+    }

+

+

+    private class ProcedureWorkItem {

       [Rep]  // KRML: this doesn't seem like the right designation to me; but I'm not sure what is

-      public Procedure! Proc;

+      public Procedure Proc;

+

       public int Index; // pre state is Impl.Summary[Index]

-   

-      invariant 0 <= Index && Index < Proc.Summary.Count;

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(Proc != null);

+        Contract.Invariant(0 <= Index && Index < Proc.Summary.Count);

+        Contract.Invariant(log != null);

+      }

 

-      public ProcedureWorkItem ([Captured] Procedure! p, AI.Lattice.Element! v, AI.Lattice! lattice)

-        ensures p == Proc; 

-      {

+      public ProcedureWorkItem([Captured] Procedure p, AI.Lattice.Element v, AI.Lattice lattice) {

+        Contract.Requires(p != null);

+        Contract.Requires(v != null);

+        Contract.Requires(lattice != null);

+

+        Contract.Ensures(p == Proc);

         this.Proc = p;

         p.Summary.Add(new ProcedureSummaryEntry(lattice, v));

         this.Index = p.Summary.Count - 1;

@@ -44,22 +57,23 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

     }

 

-    private readonly static AI.Logger! log = new AI.Logger("Engine");

+    private readonly static AI.Logger log = new AI.Logger("Engine");

 

-    public AbstractionEngine (AI.Lattice! lattice) 

-    {

-      assume log.IsExposable;  //PM: One would need static class invariants to prove this property

-      expose(log) { 

-        log.Enabled = AI.Lattice.LogSwitch;

-      }

-      this.lattice = lattice; 

-      this.procWorkItems = new Queue<ProcedureWorkItem!>();

+

+    public AbstractionEngine(AI.Lattice lattice) {

+      Contract.Requires(lattice != null);

+      Contract.Assume(cce.IsExposable(log)); //TODO: use the extension method syntax  //PM: One would need static class invariants to prove this property

+      cce.BeginExpose(log);

+      log.Enabled = AI.Lattice.LogSwitch;

+      cce.EndExpose();

+      this.lattice = lattice;

+      this.procWorkItems = new Queue<ProcedureWorkItem>();

       this.callReturnWorkItems = new Queue();

     }

 

-    private Cci.IGraphNavigator ComputeCallGraph (Program! program)

-      ensures this.procedureImplementations != null;

-    {

+    private Cci.IGraphNavigator ComputeCallGraph(Program program) {

+      Contract.Requires(program != null);

+      Contract.Ensures(this.procedureImplementations != null);

       // Since implementations call procedures (impl. signatures) 

       // rather than directly calling other implementations, we first

       // need to compute which implementations implement which

@@ -69,53 +83,45 @@ namespace Microsoft.Boogie.AbstractInterpretation
       Cci.IMutableRelation/*<Implementation,Procedure>*/ callsProcedure = new Cci.Relation();

       Cci.IMutableRelation/*<Procedure,Implementation>*/ implementsProcedure = new Cci.Relation();

       this.procedureImplementations = implementsProcedure;

-      

-//      ArrayList publics = new ArrayList();

-//      publicImpls = publics;

 

-      foreach (Declaration member in program.TopLevelDeclarations)

-      {

+      //      ArrayList publics = new ArrayList();

+      //      publicImpls = publics;

+

+      foreach (Declaration member in program.TopLevelDeclarations) {

         Implementation impl = member as Implementation;

-        if (impl != null) 

-        {

+        if (impl != null) {

           implementsProcedure.Add(impl.Proc, impl);

- //         if (impl.IsPublic) { publics.Add(impl); }          // PR: what does "IsPublic" stand for?

+          //         if (impl.IsPublic) { publics.Add(impl); }          // PR: what does "IsPublic" stand for?

 

-          foreach (Block block in impl.Blocks)

-          {

-            foreach (Cmd cmd in block.Cmds)

-            {

+          foreach (Block block in impl.Blocks) {

+            foreach (Cmd cmd in block.Cmds) {

               CallCmd call = cmd as CallCmd;

-              if (call != null)

-              {

+              if (call != null) {

                 callsProcedure.Add(impl, call.Proc);

               }

             }

           }

         }

       }

-      

+

       // Now compute a graph from implementations to implementations.

 

       Cci.GraphBuilder callGraph = new Cci.GraphBuilder();

 

       IEnumerable callerImpls = callsProcedure.GetKeys();

-      assume callerImpls != null;  // because of non-generic collection

-      foreach (Implementation caller in callerImpls)

-      {

+      Contract.Assume(callerImpls != null);  // because of non-generic collection

+      foreach (Implementation caller in callerImpls) {

         IEnumerable callerProcs = callsProcedure.GetValues(caller);

-        assume callerProcs != null;  // because of non-generic collection

-        foreach (Procedure callee in callerProcs)

-        {

+        Contract.Assume(callerProcs != null);  // because of non-generic collection

+        foreach (Procedure callee in callerProcs) {

           IEnumerable calleeImpls = implementsProcedure.GetValues(callee);

-          assume calleeImpls != null;  // because of non-generic collection

-          foreach (Implementation calleeImpl in calleeImpls)

-          {

+          Contract.Assume(calleeImpls != null);  // because of non-generic collection

+          foreach (Implementation calleeImpl in calleeImpls) {

             callGraph.AddEdge(caller, calleeImpl);

           }

         }

       }

-      

+

       return callGraph;

     }

 

@@ -180,10 +186,15 @@ namespace Microsoft.Boogie.AbstractInterpretation
     }

 #endif

 

-    public AI.Lattice.Element! ApplyProcedureSummary (CallCmd! call, Implementation! caller, AI.Lattice.Element! knownAtCallSite, CallSite! callSite)

-      requires call.Proc != null; 

-    {

-      Procedure! proc = call.Proc;

+    public AI.Lattice.Element ApplyProcedureSummary(CallCmd call, Implementation caller, AI.Lattice.Element knownAtCallSite, CallSite callSite) {

+      Contract.Requires(call.Proc != null);

+      Contract.Requires(call != null);

+      Contract.Requires(caller != null);

+      Contract.Requires(knownAtCallSite != null);

+      Contract.Requires(callSite != null);

+

+      Contract.Ensures(Contract.Result<AI.Lattice.Element>() != null);

+      Procedure proc = call.Proc;//Precondition required that call.Proc !=null, therefore no assert necessarry.

 

       // NOTE: Here, we count on the fact that an implementation's variables

       // are distinct from an implementation's procedure's variables. So, even for

@@ -197,73 +208,75 @@ namespace Microsoft.Boogie.AbstractInterpretation
       // where the notation i' means a variable with the same (string) name as i, 

       // but a different identity.

 

-      AI.Lattice.Element! relevantToCall = knownAtCallSite;

-      for (int i=0; i<proc.InParams.Length; i++)

-      {

+      AI.Lattice.Element relevantToCall = knownAtCallSite; //Precondition of the method implies that this can never be null, therefore no need for an assert.

+      for (int i = 0; i < proc.InParams.Length; i++) {

         // "Assign" the actual expressions to the corresponding formal variables.

-        assume proc.InParams[i] != null;  //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

-        assume call.Ins[i] != null;       //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

-        Expr equality = Expr.Eq(Expr.Ident( (!) proc.InParams[i]), (!) call.Ins[i]);

+        Contract.Assume(proc.InParams[i] != null);  //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

+        Contract.Assume(call.Ins[i] != null);       //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

+        Expr equality = Expr.Eq(Expr.Ident(cce.NonNull(proc.InParams[i])), cce.NonNull(call.Ins[i]));

         relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr);

       }

-      foreach (Variable! var in caller.LocVars) {

-          relevantToCall = this.lattice.Eliminate(relevantToCall, var);

+      foreach (Variable var in caller.LocVars) {

+        Contract.Assert(var != null);

+        relevantToCall = this.lattice.Eliminate(relevantToCall, var);

       }

 

-      ProcedureSummary! summary = proc.Summary;

+      ProcedureSummary summary = proc.Summary;

+      Contract.Assert(summary != null);

       ProcedureSummaryEntry applicableEntry = null;

 

-      for (int i=0; i<summary.Count; i++)

-      {

-        ProcedureSummaryEntry! current = (!) summary[i];

+      for (int i = 0; i < summary.Count; i++) {

+        ProcedureSummaryEntry current = cce.NonNull(summary[i]);

 

-        if (lattice.Equivalent(current.OnEntry, relevantToCall))

-        {

+        if (lattice.Equivalent(current.OnEntry, relevantToCall)) {

           applicableEntry = current;

           break;

         }

       }

 

       // Not found in current map, so add new entry.

-      if (applicableEntry == null)

-      {

-        ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice);

+      if (applicableEntry == null) {

+        ProcedureWorkItem newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice);

+        Contract.Assert(newWorkItem != null);

         this.procWorkItems.Enqueue(newWorkItem);

-        applicableEntry = (!)  proc.Summary[newWorkItem.Index];

+        applicableEntry = cce.NonNull(proc.Summary[newWorkItem.Index]);

       }

       applicableEntry.ReturnPoints.Add(callSite);

-      

+

 

       AI.Lattice.Element atReturn = applicableEntry.OnExit;

 

-      for (int i=0; i<call.Outs.Count; i++)

-      {

-        atReturn = this.lattice.Rename(atReturn, (!) call.Proc.OutParams[i], (!)((!) call.Outs[i]).Decl);

-        knownAtCallSite = this.lattice.Eliminate(knownAtCallSite, (!)((!) call.Outs[i]).Decl);

+      for (int i = 0; i < call.Outs.Count; i++) {

+        atReturn = this.lattice.Rename(atReturn, cce.NonNull(call.Proc.OutParams[i]), cce.NonNull(cce.NonNull(call.Outs[i]).Decl));

+        knownAtCallSite = this.lattice.Eliminate(knownAtCallSite, cce.NonNull(cce.NonNull(call.Outs[i]).Decl));

       }

 

       return this.lattice.Meet(atReturn, knownAtCallSite);

     }

 

     private Cci.IGraphNavigator callGraph;

-    public Cci.IGraphNavigator CallGraph { 

-      get { return this.callGraph; } 

-    } 

-     

+    public Cci.IGraphNavigator CallGraph {

+      get {

+        return this.callGraph;

+      }

+    }

+

     /// <summary>

     /// Compute the invariants for the program using the underlying abstract domain

     /// </summary>

-    public void ComputeProgramInvariants (Program! program) 

-    {        

-      

+    public void ComputeProgramInvariants(Program program) {

+      Contract.Requires(program != null);

+

 #if NOT_YET

       Cci.IGraphNavigator callGraph = 

 #endif

 

       callGraph = this.ComputeCallGraph(program);

-      assert this.procedureImplementations != null;

-      Cci.IRelation! procedureImplementations = this.procedureImplementations;

-

+      Contract.Assert(this.procedureImplementations != null);

+      Cci.IRelation procedureImplementations = this.procedureImplementations;//Non-nullability was already asserted in

+      //the line above, ergo there is no need for

+      //an assert after this statement to maintain

+      //the non-null type.

 #if NOT_YET

       IEnumerable/*<IStronglyConnectedComponent>*/ sccs = 

           StronglyConnectedComponent.ConstructSCCs(publicImpls, callGraph);

@@ -277,89 +290,75 @@ namespace Microsoft.Boogie.AbstractInterpretation
         this.ComputeSccInvariants(scc.Nodes);

       }

 #endif

-      AI.Lattice.Element! initialElement = this.lattice.Top;

+      AI.Lattice.Element initialElement = this.lattice.Top;

+      Contract.Assert(initialElement != null);

       // Gather all the axioms to create the initial lattice element

       // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain

 

-      foreach (Declaration decl in program.TopLevelDeclarations)

-      {

+      foreach (Declaration decl in program.TopLevelDeclarations) {

         Axiom ax = decl as Axiom;

-        if (ax != null)

-        {

+        if (ax != null) {

           initialElement = this.lattice.Constrain(initialElement, ax.Expr.IExpr);

         }

       }

 

       // propagate over all procedures...

-      foreach (Declaration decl in program.TopLevelDeclarations)

-      {

+      foreach (Declaration decl in program.TopLevelDeclarations) {

         Procedure proc = decl as Procedure;

-        if (proc != null) 

-        {

+        if (proc != null) {

           this.procWorkItems.Enqueue(new ProcedureWorkItem(proc, initialElement, this.lattice));

         }

       }

 

       // analyze all the procedures...

-      while (this.procWorkItems.Count + this.callReturnWorkItems.Count > 0)

-      {

-        while (this.procWorkItems.Count > 0)

-        {

+      while (this.procWorkItems.Count + this.callReturnWorkItems.Count > 0) {

+        while (this.procWorkItems.Count > 0) {

           ProcedureWorkItem workItem = this.procWorkItems.Dequeue();

 

-          ProcedureSummaryEntry summaryEntry = (!) workItem.Proc.Summary[workItem.Index];

+          ProcedureSummaryEntry summaryEntry = cce.NonNull(workItem.Proc.Summary[workItem.Index]);

 

-          if (((!) procedureImplementations.GetValues(workItem.Proc)).Count == 0)

-          {

+          if (cce.NonNull(procedureImplementations.GetValues(workItem.Proc)).Count == 0) {

             // This procedure has no given implementations.  We therefore treat the procedure

             // according to its specification only.

 

-            if (!CommandLineOptions.Clo.IntraproceduralInfer)

-            {

+            if (!CommandLineOptions.Clo.IntraproceduralInfer) {

               AI.Lattice.Element post = summaryEntry.OnEntry;

               // BUGBUG.  Here, we should process "post" according to the requires, modifies, ensures

               // specification of the procedure, including any OLD expressions in the postcondition.

               AI.Lattice.Element atReturn = post;

 

-              if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))

-              {

+              if (!this.lattice.LowerThan(atReturn, summaryEntry.OnExit)) {

                 // If the results of this analysis are strictly worse than

                 // what we previous knew for the same input assumptions,

                 // update the summary and re-do the call sites.

 

                 summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);

 

-                foreach (CallSite callSite in summaryEntry.ReturnPoints)

-                {

+                foreach (CallSite callSite in summaryEntry.ReturnPoints) {

                   this.callReturnWorkItems.Enqueue(callSite);

                 }

               }

             }

-          }

-          else

-          {

+          } else {

             // There are implementations, so do inference based on those implementations

 

-            if (!CommandLineOptions.Clo.IntraproceduralInfer)

-            {

+            if (!CommandLineOptions.Clo.IntraproceduralInfer) {

               summaryEntry.OnExit = lattice.Bottom;

             }

 

             // For each implementation in the procedure...

-            foreach (Implementation! impl in (!) procedureImplementations.GetValues(workItem.Proc))

-            {

+            foreach (Implementation impl in cce.NonNull(procedureImplementations.GetValues(workItem.Proc))) {

               // process each procedure implementation by recursively processing the first (entry) block...

-              ((!)impl.Blocks[0]).Lattice = lattice;

-              ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry, summaryEntry);

+              cce.NonNull(impl.Blocks[0]).Lattice = lattice;

+              ComputeBlockInvariants(impl, cce.NonNull(impl.Blocks[0]), summaryEntry.OnEntry, summaryEntry);

               AdjustProcedureSummary(impl, summaryEntry);

             }

           }

         }

 

 

-        while (this.callReturnWorkItems.Count > 0)

-        {

-          CallSite callSite = (CallSite!) this.callReturnWorkItems.Dequeue();

+        while (this.callReturnWorkItems.Count > 0) {

+          CallSite callSite = cce.NonNull((CallSite)this.callReturnWorkItems.Dequeue());

 

           PropagateStartingAtStatement(callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall, callSite.SummaryEntry);

           AdjustProcedureSummary(callSite.Impl, callSite.SummaryEntry);

@@ -368,62 +367,61 @@ namespace Microsoft.Boogie.AbstractInterpretation
       } // both queues

 

     }

-    

-    void AdjustProcedureSummary(Implementation! impl, ProcedureSummaryEntry! summaryEntry)

-    {

+

+    void AdjustProcedureSummary(Implementation impl, ProcedureSummaryEntry summaryEntry) {

+      Contract.Requires(impl != null);

+      Contract.Requires(summaryEntry != null);

       if (CommandLineOptions.Clo.IntraproceduralInfer) {

         return;  // no summary to adjust

       }

 

       // compute the procedure invariant by joining all terminal block invariants...

       AI.Lattice.Element post = lattice.Bottom;

-      foreach (Block block in impl.Blocks) 

-      {

-        if (block.TransferCmd is ReturnCmd) 

-        {                 

+      foreach (Block block in impl.Blocks) {

+        if (block.TransferCmd is ReturnCmd) {

           // note: if program control cannot reach this block, then postValue will be null

-          if (block.PostInvariant != null) 

-          {

-            post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);

+          if (block.PostInvariant != null) {

+            post = (AI.Lattice.Element)lattice.Join(post, block.PostInvariant);

           }

         }

       }

 

       AI.Lattice.Element atReturn = post;

-      foreach (Variable! var in impl.LocVars) 

-      {

-          atReturn = this.lattice.Eliminate(atReturn, var);

+      foreach (Variable var in impl.LocVars) {

+        Contract.Assert(var != null);

+        atReturn = this.lattice.Eliminate(atReturn, var);

       }

-      foreach (Variable! var in impl.InParams) 

-      {

-          atReturn = this.lattice.Eliminate(atReturn, var);

+      foreach (Variable var in impl.InParams) {

+        Contract.Assert(var != null);

+        atReturn = this.lattice.Eliminate(atReturn, var);

       }

 

-      if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))

-      {

+      if (!this.lattice.LowerThan(atReturn, summaryEntry.OnExit)) {

         // If the results of this analysis are strictly worse than

         // what we previous knew for the same input assumptions,

         // update the summary and re-do the call sites.

 

         summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);

 

-        foreach (CallSite! callSite in summaryEntry.ReturnPoints)

-        {

+        foreach (CallSite callSite in summaryEntry.ReturnPoints) {

+          Contract.Assert(callSite != null);

           this.callReturnWorkItems.Enqueue(callSite);

         }

       }

     }

 

     private static int freshVarId = 0;

-    private static Variable! FreshVar(Boogie.Type! ty)

-    {

+    private static Variable FreshVar(Boogie.Type ty) {

+      Contract.Requires(ty != null);

+      Contract.Ensures(Contract.Result<Variable>() != null);

+

       Variable fresh = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "fresh" + freshVarId, ty));

       freshVarId++;

       return fresh;

     }

-    

-    private delegate CallSite! MarkCallSite(AI.Lattice.Element! currentValue);

-    

+

+    private delegate CallSite/*!*/ MarkCallSite(AI.Lattice.Element/*!*/ currentValue);//TODO: Think this is an invariant, but not sure how2 deal with it

+

     /// <summary>

     /// Given a basic block, it propagates the abstract state at the entry point through the exit point of the block

     /// <param name="impl"> The implementation that owns the block </param>

@@ -431,44 +429,45 @@ namespace Microsoft.Boogie.AbstractInterpretation
     /// <param name="statementIndex">  </param> 

     /// <param name="currentValue"> The initial value </param>

     /// </summary>

-    private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue,

-                                               ProcedureSummaryEntry! summaryEntry)

-    {

-      assume log.IsPeerConsistent;

-      log.DbgMsg(string.Format("{0}:", block.Label)); log.DbgMsgIndent();

+    private void PropagateStartingAtStatement(Implementation/*!*/ impl, Block/*!*/ block, int statementIndex, AI.Lattice.Element/*!*/ currentValue,

+                                               ProcedureSummaryEntry/*!*/ summaryEntry) {

+      Contract.Requires(impl != null);

+      Contract.Requires(block != null);

+      Contract.Requires(currentValue != null);

+      Contract.Requires(summaryEntry != null);

+      Contract.Assume(cce.IsPeerConsistent(log));

+      log.DbgMsg(string.Format("{0}:", block.Label));

+      log.DbgMsgIndent();

 

       #region Apply the abstract transition relation to the statements in the block

-      for (int cmdIndex = statementIndex; cmdIndex < block.Cmds.Length; cmdIndex++) 

-      {

-        Cmd! cmd = (!) block.Cmds[cmdIndex];              // Fetch the command

+      for (int cmdIndex = statementIndex; cmdIndex < block.Cmds.Length; cmdIndex++) {

+        Cmd cmd = cce.NonNull(block.Cmds[cmdIndex]);              // Fetch the command

         currentValue = Step(cmd, currentValue, impl,      // Apply the transition function

-                            delegate (AI.Lattice.Element! currentValue) 

-                            {

-                              return new CallSite(impl, block, cmdIndex, currentValue, summaryEntry);

+                            delegate(AI.Lattice.Element cv) {

+                              Contract.Requires(cv != null);

+                              return new CallSite(impl, block, cmdIndex, cv, summaryEntry);

                             }

                            );

       }

-      

+

       block.PostInvariant = currentValue;      // The invariant at the exit point of the block is that of the last statement

-           

-      log.DbgMsg(string.Format("pre   {0}", ((!)block.PreInvariant).ToString()));

+

+      log.DbgMsg(string.Format("pre   {0}", cce.NonNull(block.PreInvariant).ToString()));

       log.DbgMsg(string.Format("post  {0}", (block.PostInvariant).ToString()));

       log.DbgMsgUnindent();

-      #endregion    

+      #endregion

       #region Propagate the post-condition to the successor nodes

       GotoCmd @goto = block.TransferCmd as GotoCmd;

-      if (@goto != null) 

-      {

+      if (@goto != null) {

         // labelTargets is non-null after calling Resolve in a prior phase.

-        assume @goto.labelTargets != null;

+        Contract.Assume(@goto.labelTargets != null);

 

         // For all the successors of this block, propagate the abstract state

-        foreach (Block! succ in @goto.labelTargets) 

-        { 

-          if(impl.Blocks.Contains(succ))

-          {

+        foreach (Block succ in @goto.labelTargets) {

+          Contract.Assert(succ != null);

+          if (impl.Blocks.Contains(succ)) {

             succ.Lattice = block.Lattice;         // The lattice is the same

-                                                // Propagate the post-abstract state of this block to the successor

+            // Propagate the post-abstract state of this block to the successor

             ComputeBlockInvariants(impl, succ, block.PostInvariant, summaryEntry);

           }

         }

@@ -479,38 +478,46 @@ namespace Microsoft.Boogie.AbstractInterpretation
     /// <summary>

     /// The abstract transition relation.

     /// </summary>

-    private AI.Lattice.Element! Step(Cmd! cmd, AI.Lattice.Element! pre, Implementation! impl, MarkCallSite/*?*/ callSiteMarker)

-    {

-      assume log.IsPeerConsistent;

-      log.DbgMsg(string.Format("{0}", cmd)); log.DbgMsgIndent();

-      

-      AI.Lattice.Element! currentValue = pre;

-      

+    private AI.Lattice.Element Step(Cmd cmd, AI.Lattice.Element pre, Implementation impl, MarkCallSite/*?*/ callSiteMarker) {

+      Contract.Requires(cmd != null);

+      Contract.Requires(pre != null);

+      Contract.Requires(impl != null);

+      Contract.Ensures(Contract.Result<AI.Lattice.Element>() != null);

+

+      Contract.Assume(cce.IsPeerConsistent(log));

+      log.DbgMsg(string.Format("{0}", cmd));

+      log.DbgMsgIndent();

+

+      AI.Lattice.Element currentValue = pre;//Nonnullability was a precondition

+

       // Case split...

       #region AssignCmd

       if (cmd is AssignCmd) { // parallel assignment

         // we first eliminate map assignments

-        AssignCmd! assmt = ((AssignCmd)cmd).AsSimpleAssignCmd;

+        AssignCmd assmt = cce.NonNull((AssignCmd)cmd).AsSimpleAssignCmd;

         //PM: Assume variables have been resolved

-        assume forall {AssignLhs! lhs in assmt.Lhss;

-                       lhs.DeepAssignedVariable != null};

+        Contract.Assume(Contract.ForAll<AssignLhs>(assmt.Lhss, lhs => lhs.DeepAssignedVariable != null));//TODO: Check my work, please, Mike.

 

-        List<IdentifierExpr!>! freshLhs = new List<IdentifierExpr!> ();

-        foreach (AssignLhs! lhs in assmt.Lhss)

-          freshLhs.Add(Expr.Ident(FreshVar(((!)lhs.DeepAssignedVariable)

+        List<IdentifierExpr/*!>!*/> freshLhs = new List<IdentifierExpr/*!*/>();

+        foreach (AssignLhs lhs in assmt.Lhss) {

+          Contract.Assert(lhs != null);

+          freshLhs.Add(Expr.Ident(FreshVar(cce.NonNull(lhs.DeepAssignedVariable)

                                            .TypedIdent.Type)));

+        }

 

         for (int i = 0; i < freshLhs.Count; ++i)

           currentValue =

             this.lattice.Constrain(currentValue,

                                    Expr.Eq(freshLhs[i], assmt.Rhss[i]).IExpr);

-        foreach (AssignLhs! lhs in assmt.Lhss)

+        foreach (AssignLhs lhs in assmt.Lhss) {

+          Contract.Assert(lhs != null);

           currentValue =

-            this.lattice.Eliminate(currentValue, (!)lhs.DeepAssignedVariable);

+            this.lattice.Eliminate(currentValue, cce.NonNull(lhs.DeepAssignedVariable));

+        }

         for (int i = 0; i < freshLhs.Count; ++i)

           currentValue =

-            this.lattice.Rename(currentValue, (!)freshLhs[i].Decl,

-                                (!)assmt.Lhss[i].DeepAssignedVariable);

+            this.lattice.Rename(currentValue, cce.NonNull(freshLhs[i].Decl),

+                                cce.NonNull(assmt.Lhss[i].DeepAssignedVariable));

       }

 

       /*

@@ -570,23 +577,23 @@ namespace Microsoft.Boogie.AbstractInterpretation
         } */

       #endregion

       #region Havoc

-      else if (cmd is HavocCmd)

-      {

+      else if (cmd is HavocCmd) {

         HavocCmd havoc = (HavocCmd)cmd;

-        foreach (IdentifierExpr! id in havoc.Vars)

-        {

-          currentValue = this.lattice.Eliminate(currentValue, (!)id.Decl);

+        foreach (IdentifierExpr id in havoc.Vars) {

+          Contract.Assert(id != null);

+          currentValue = this.lattice.Eliminate(currentValue, cce.NonNull(id.Decl));

         }

       }

       #endregion

       #region PredicateCmd

-      else if (cmd is PredicateCmd)

-      {

+ else if (cmd is PredicateCmd) {

         //System.Console.WriteLine("Abstract State BEFORE " + ((PredicateCmd) cmd).Expr + " : " +this.lattice.ToPredicate(currentValue));

 

-        Expr! embeddedExpr = (!)((PredicateCmd)cmd).Expr;

-        List<Expr!>! conjuncts = flatConjunction(embeddedExpr);           // Handle "assume P && Q" as if it was "assume P; assume Q"

-        foreach(Expr! c in conjuncts) {

+        Expr embeddedExpr = cce.NonNull((PredicateCmd)cmd).Expr;

+        List<Expr/*!>!*/> conjuncts = flatConjunction(embeddedExpr);           // Handle "assume P && Q" as if it was "assume P; assume Q"

+        Contract.Assert(conjuncts != null);

+        foreach (Expr c in conjuncts) {

+          Contract.Assert(c != null);

           currentValue = this.lattice.Constrain(currentValue, c.IExpr);

         }

 

@@ -594,86 +601,91 @@ namespace Microsoft.Boogie.AbstractInterpretation
       }

       #endregion

       #region CallCmd

-      else if (cmd is CallCmd)

-      {

+ else if (cmd is CallCmd) {

         CallCmd call = (CallCmd)cmd;

-        

-        if (!CommandLineOptions.Clo.IntraproceduralInfer)

-        {

+

+        if (!CommandLineOptions.Clo.IntraproceduralInfer) {

           // Interprocedural analysis

-          

-          if (callSiteMarker == null)

-          {

+

+          if (callSiteMarker == null) {

             throw new System.InvalidOperationException("INTERNAL ERROR: Context does not allow CallCmd.");

           }

-          

+

           CallSite here = callSiteMarker(currentValue);

           currentValue = ApplyProcedureSummary(call, impl, currentValue, here);

-        }

-        else

-        {

+        } else {

           // Intraprocedural analysis

-          

+

           StateCmd statecmd = call.Desugaring as StateCmd;

-          if (statecmd != null)

-          {

+          if (statecmd != null) {

             // Iterate the abstract transition on all the commands in the desugaring of the call

-            foreach (Cmd! callDesug in statecmd.Cmds) { currentValue = Step(callDesug, currentValue, impl, null); }

-            

+            foreach (Cmd callDesug in statecmd.Cmds) {

+              Contract.Assert(callDesug != null);

+              currentValue = Step(callDesug, currentValue, impl, null);

+            }

+

             // Now, project out the local variables

-            foreach (Variable! local in statecmd.Locals) { currentValue = this.lattice.Eliminate(currentValue, local); }

-          }

-          else throw new System.InvalidOperationException("INTERNAL ERROR: CallCmd does not desugar to StateCmd.");

+            foreach (Variable local in statecmd.Locals) {

+              Contract.Assert(local != null);

+              currentValue = this.lattice.Eliminate(currentValue, local);

+            }

+          } else

+            throw new System.InvalidOperationException("INTERNAL ERROR: CallCmd does not desugar to StateCmd.");

         }

       }

       #endregion

       #region CommentCmd

-      else if (cmd is CommentCmd)

-      {

+ else if (cmd is CommentCmd) {

         // skip

       }

-      #endregion      

-      else if (cmd is SugaredCmd)

-      {

+      #endregion

+ else if (cmd is SugaredCmd) {

         // other sugared commands are treated like their desugaring

         SugaredCmd sugar = (SugaredCmd)cmd;

         Cmd desugaring = sugar.Desugaring;

         if (desugaring is StateCmd) {

           StateCmd statecmd = (StateCmd)desugaring;

           // Iterate the abstract transition on all the commands in the desugaring of the call

-          foreach (Cmd! callDesug in statecmd.Cmds) { currentValue = Step(callDesug, currentValue, impl, null); }

+          foreach (Cmd callDesug in statecmd.Cmds) {

+            Contract.Assert(callDesug != null);

+            currentValue = Step(callDesug, currentValue, impl, null);

+          }

           // Now, project out the local variables

-          foreach (Variable! local in statecmd.Locals) { currentValue = this.lattice.Eliminate(currentValue, local); }

+          foreach (Variable local in statecmd.Locals) {

+            Contract.Assert(local != null);

+            currentValue = this.lattice.Eliminate(currentValue, local);

+          }

         } else {

           currentValue = Step(desugaring, currentValue, impl, null);

         }

+      } else {

+        Contract.Assert(false);  // unknown command

+        throw new cce.UnreachableException();

       }

-      else

-      {

-          assert false;  // unknown command

-      }

-      

+

       log.DbgMsgUnindent();

-      

+

       return currentValue;

     }

- 

+

     /// <summary>

     /// Flat an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]

     /// </summary>

-    private List<Expr!>! flatConjunction(Expr! embeddedExpr) 

-    {

-      List<Expr!>! retValue = new List<Expr!>();

+    private List<Expr/*!>!*/> flatConjunction(Expr embeddedExpr) {

+      Contract.Requires(embeddedExpr != null);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expr>>()));

+

+

+      List<Expr/*!>!*/> retValue = new List<Expr/*!*/>();//No asserts necessarry.  It is the return value, and thus will be subject to the postcondition

       NAryExpr e = embeddedExpr as NAryExpr;

-      if(e != null && e.Fun.FunctionName.CompareTo("&&") == 0) {    // if it is a conjunction

-        foreach(Expr! arg in e.Args) 

-        {

-          List<Expr!>! newConjuncts = flatConjunction(arg);

+      if (e != null && e.Fun.FunctionName.CompareTo("&&") == 0) {    // if it is a conjunction

+        foreach (Expr arg in e.Args) {

+          Contract.Assert(arg != null);

+          List<Expr/*!*/>/*!*/  newConjuncts = flatConjunction(arg);

+          Contract.Assert(cce.NonNullElements(newConjuncts));

           retValue.AddRange(newConjuncts);

-        }          

-      }

-      else 

-      {     

+        }

+      } else {

         retValue.Add(embeddedExpr);

       }

       return retValue;

@@ -685,24 +697,26 @@ namespace Microsoft.Boogie.AbstractInterpretation
     /// <param name="block">  The block for which we compute the invariants </param>

     /// <param name="incomingValue">  The "init" abstract state for the block </param>

     /// </summary>

-    private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue, ProcedureSummaryEntry! summaryEntry)

-    {

+    private void ComputeBlockInvariants(Implementation impl, Block block, AI.Lattice.Element incomingValue, ProcedureSummaryEntry summaryEntry) {

+      Contract.Requires(impl != null);

+      Contract.Requires(block != null);

+      Contract.Requires(incomingValue != null);

+      Contract.Requires(summaryEntry != null);

       if (block.PreInvariant == null) // block has not yet been processed

       {

-        assert block.PostInvariant == null;

-        

+        Contract.Assert(block.PostInvariant == null);

+

         // To a first approximation the block is unreachable

         block.PreInvariant = this.lattice.Bottom;

         block.PostInvariant = this.lattice.Bottom;

       }

 

-      assert block.PreInvariant != null;

-      assert block.PostInvariant != null;

+      Contract.Assert(block.PreInvariant != null);

+      Contract.Assert(block.PostInvariant != null);

 

       #region Check if we have reached a postfixpoint

 

-      if (lattice.LowerThan(incomingValue, block.PreInvariant))

-      {

+      if (lattice.LowerThan(incomingValue, block.PreInvariant)) {

         // We have reached a post-fixpoint, so we are done...

 #if DEBUG_PRINT

         System.Console.WriteLine("@@ Compared for block {0}:", block.Label);

@@ -733,37 +747,32 @@ namespace Microsoft.Boogie.AbstractInterpretation
       System.Console.WriteLine("@@ end Compare");

       string operation = "";

 #endif

-      #endregion       

+      #endregion

       #region If it is not the case, then join or widen the incoming abstract state with the previous one

       if (block.widenBlock)     // If the considered block is the entry point of a loop

       {

-        if( block.iterations <= CommandLineOptions.Clo.StepsBeforeWidening+1)

-        {        

+        if (block.iterations <= CommandLineOptions.Clo.StepsBeforeWidening + 1) {

 #if DEBUG_PRINT 

     operation = "join";

 #endif

-          block.PreInvariant = (AI.Lattice.Element) lattice.Join( block.PreInvariant, incomingValue);

-        }        

-        else

-        {

+          block.PreInvariant = (AI.Lattice.Element)lattice.Join(block.PreInvariant, incomingValue);

+        } else {

 #if DEBUG_PRINT

       operation = "widening";

-#endif 

+#endif

 

-            // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision

-        //    block.PreInvariant =  WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);            

-         block.PreInvariant = (AI.Lattice.Element) lattice.Widen( block.PreInvariant, incomingValue);

+          // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision

+          //    block.PreInvariant =  WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);            

+          block.PreInvariant = (AI.Lattice.Element)lattice.Widen(block.PreInvariant, incomingValue);

         }

         block.iterations++;

-      } 

-      else 

-      {

+      } else {

 #if DEBUG_PRINT

   operation = "join";

 #endif

-        block.PreInvariant = (AI.Lattice.Element) lattice.Join( block.PreInvariant, incomingValue);

+        block.PreInvariant = (AI.Lattice.Element)lattice.Join(block.PreInvariant, incomingValue);

       }

-      

+

 #if DEBUG_PRINT

       System.Console.WriteLine("@@ {0} for block {1}:", operation, block.Label);

       System.Console.WriteLine("@@ {0}", lattice.ToPredicate(block.PreInvariant));

@@ -771,7 +780,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
 #endif

       #endregion

       #region Propagate the entry abstract state through the method

-        PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone(), summaryEntry);

+      PropagateStartingAtStatement(impl, block, 0, cce.NonNull(block.PreInvariant.Clone()), summaryEntry);

       #endregion

     }

 

@@ -794,26 +803,26 @@ namespace Microsoft.Boogie.AbstractInterpretation
   /// <summary>

   /// Defines a class for building the abstract domain according to the parameters switch

   /// </summary>

-  public class AbstractDomainBuilder

-  {

+  public class AbstractDomainBuilder {

+

+    private AbstractDomainBuilder() { /* do nothing */

+    }

 

-    private AbstractDomainBuilder()

-    { /* do nothing */ }

-  

     /// <summary>

     /// Return a fresh instance of the abstract domain of intervals

     /// </summary>

-    static public AbstractAlgebra! BuildIntervalsAbstractDomain() 

-    { 

+    static public AbstractAlgebra BuildIntervalsAbstractDomain() {

+      Contract.Ensures(Contract.Result<AbstractAlgebra>() != null);

+

       AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();

-      AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();     

+      AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();

       AI.IValueExprFactory valuefactory = new BoogieValueFactory();

       IComparer variableComparer = new VariableComparer();

 

-      AbstractAlgebra! retAlgebra;

-      AI.Lattice! intervals = new AI.VariableMapLattice(propfactory, valuefactory, new AI.IntervalLattice(linearfactory), variableComparer);

-

-      retAlgebra = new AbstractAlgebra(intervals, propfactory, linearfactory, null, valuefactory, null, variableComparer);    

+      AbstractAlgebra retAlgebra;

+      AI.Lattice intervals = new AI.VariableMapLattice(propfactory, valuefactory, new AI.IntervalLattice(linearfactory), variableComparer);

+      Contract.Assert(intervals != null);

+      retAlgebra = new AbstractAlgebra(intervals, propfactory, linearfactory, null, valuefactory, null, variableComparer);

 

       return retAlgebra;

     }

@@ -821,154 +830,154 @@ namespace Microsoft.Boogie.AbstractInterpretation
     /// <summary>

     /// Return a fresh abstract domain, according to the parameters specified by the command line

     /// </summary>

-    static public AbstractAlgebra! BuildAbstractDomain()

-    {

-        AbstractAlgebra! retAlgebra;

-      

-        AI.Lattice! returnLattice;

+    static public AbstractAlgebra BuildAbstractDomain() {

+      Contract.Ensures(Contract.Result<AbstractAlgebra>() != null);

 

-        AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();

-        AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();

-        AI.IIntExprFactory intfactory = new BoogieIntFactory();

-        AI.IValueExprFactory valuefactory = new BoogieValueFactory();

-        AI.INullnessFactory nullfactory = new BoogieNullnessFactory();

-        IComparer variableComparer = new VariableComparer();

+      AbstractAlgebra retAlgebra;

 

-        AI.MultiLattice multilattice = new AI.MultiLattice(propfactory, valuefactory);

+      AI.Lattice returnLattice;

 

-        if (CommandLineOptions.Clo.Ai.Intervals)        // Intervals

-        {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                  new AI.IntervalLattice(linearfactory),

-                                  variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Constant)         // Constant propagation

+      AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();

+      AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();

+      AI.IIntExprFactory intfactory = new BoogieIntFactory();

+      AI.IValueExprFactory valuefactory = new BoogieValueFactory();

+      AI.INullnessFactory nullfactory = new BoogieNullnessFactory();

+      IComparer variableComparer = new VariableComparer();

+

+      AI.MultiLattice multilattice = new AI.MultiLattice(propfactory, valuefactory);

 

+      if (CommandLineOptions.Clo.Ai.Intervals)        // Intervals

         {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                  new AI.ConstantLattice(intfactory),

-                                  variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.DynamicType)      // Class types

+        multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

+                                new AI.IntervalLattice(linearfactory),

+                                variableComparer));

+      }

+      if (CommandLineOptions.Clo.Ai.Constant)         // Constant propagation

+

         {

-          BoogieTypeFactory typeFactory = new BoogieTypeFactory();

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                                    new AI.DynamicTypeLattice(typeFactory, propfactory),

-                                                    variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Nullness)       // Nullness

+        multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

+                                new AI.ConstantLattice(intfactory),

+                                variableComparer));

+      }

+      if (CommandLineOptions.Clo.Ai.DynamicType)      // Class types

         {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                                    new AI.NullnessLattice(nullfactory),

-                                                    variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Polyhedra)    // Polyhedra

+        BoogieTypeFactory typeFactory = new BoogieTypeFactory();

+        multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

+                                                  new AI.DynamicTypeLattice(typeFactory, propfactory),

+                                                  variableComparer));

+      }

+      if (CommandLineOptions.Clo.Ai.Nullness)       // Nullness

         {

-          multilattice.AddLattice(new AI.PolyhedraLattice(linearfactory, propfactory));

-        }

-        

-                

-        returnLattice = multilattice;

-        if (CommandLineOptions.Clo.Ai.DebugStatistics) 

+        multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

+                                                  new AI.NullnessLattice(nullfactory),

+                                                  variableComparer));

+      }

+      if (CommandLineOptions.Clo.Ai.Polyhedra)    // Polyhedra

         {

-          returnLattice = new AI.StatisticsLattice(returnLattice);

-        }

+        multilattice.AddLattice(new AI.PolyhedraLattice(linearfactory, propfactory));

+      }

 

-        returnLattice.Validate();

 

-        retAlgebra = new AbstractAlgebra(returnLattice, propfactory, linearfactory, intfactory, valuefactory, nullfactory, 

-                                                        variableComparer);

+      returnLattice = multilattice;

+      if (CommandLineOptions.Clo.Ai.DebugStatistics) {

+        returnLattice = new AI.StatisticsLattice(returnLattice);

+      }

 

-        return retAlgebra;

+      returnLattice.Validate();

+

+      retAlgebra = new AbstractAlgebra(returnLattice, propfactory, linearfactory, intfactory, valuefactory, nullfactory,

+                                                      variableComparer);

+

+      return retAlgebra;

 

     }

-  } 

-  

+  }

+

   /// <summary>

   /// An Abstract Algebra is a tuple made of a Lattice and several factories

   /// </summary>

-  public class AbstractAlgebra

-  {

-    [Peer] private AI.Lattice! lattice;

-    [Peer] private AI.IQuantPropExprFactory propFactory;

-    [Peer] private AI.ILinearExprFactory linearFactory;

-    [Peer] private AI.IIntExprFactory intFactory;

-    [Peer] private AI.IValueExprFactory valueFactory;

-    [Peer] private AI.INullnessFactory nullFactory;

-    [Peer] private IComparer variableComparer;

-

-    public AI.Lattice! Lattice

-    {

-      get

-      {

-        return lattice; 

+  public class AbstractAlgebra {

+    [Peer]

+    private AI.Lattice lattice;

+    [Peer]

+    private AI.IQuantPropExprFactory propFactory;

+    [Peer]

+    private AI.ILinearExprFactory linearFactory;

+    [Peer]

+    private AI.IIntExprFactory intFactory;

+    [Peer]

+    private AI.IValueExprFactory valueFactory;

+    [Peer]

+    private AI.INullnessFactory nullFactory;

+    [Peer]

+    private IComparer variableComparer;

+

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(lattice != null);

+    }

+

+    public AI.Lattice Lattice {

+      get {

+        Contract.Ensures(Contract.Result<AI.Lattice>() != null);

+

+        return lattice;

       }

-    }      

+    }

 

-    public AI.IQuantPropExprFactory PropositionFactory

-    {

-      get

-      {

+    public AI.IQuantPropExprFactory PropositionFactory {

+      get {

         return this.propFactory;

       }

     }

 

-    public AI.ILinearExprFactory LinearExprFactory

-    {

-      get

-      {

+    public AI.ILinearExprFactory LinearExprFactory {

+      get {

         return this.linearFactory;

       }

     }

 

-    public AI.IIntExprFactory IntExprFactory

-    {

-      get

-      {

+    public AI.IIntExprFactory IntExprFactory {

+      get {

         return this.intFactory;

       }

     }

 

-    public AI.IValueExprFactory ValueFactory

-    {

-      get

-      {

+    public AI.IValueExprFactory ValueFactory {

+      get {

         return this.valueFactory;

       }

     }

-    

-    public AI.INullnessFactory NullFactory

-    {

-      get

-      {

+

+    public AI.INullnessFactory NullFactory {

+      get {

         return this.nullFactory;

       }

     }

 

-    public IComparer VariableComparer

-    {

-      get

-      {

+    public IComparer VariableComparer {

+      get {

         return this.variableComparer;

       }

     }

 

     [Captured]

-    public AbstractAlgebra(AI.Lattice! lattice, 

-                          AI.IQuantPropExprFactory propFactory, 

+    public AbstractAlgebra(AI.Lattice lattice,

+                          AI.IQuantPropExprFactory propFactory,

                           AI.ILinearExprFactory linearFactory,

                           AI.IIntExprFactory intFactory,

                           AI.IValueExprFactory valueFactory,

                           AI.INullnessFactory nullFactory,

-                          IComparer variableComparer)

-      requires propFactory != null ==> Owner.Same(lattice, propFactory);

-      requires linearFactory != null ==> Owner.Same(lattice, linearFactory);

-      requires intFactory != null ==> Owner.Same(lattice, intFactory);

-      requires valueFactory != null ==> Owner.Same(lattice, valueFactory);

-      requires nullFactory != null ==> Owner.Same(lattice, nullFactory);

-      requires variableComparer != null ==> Owner.Same(lattice, variableComparer);

+                          IComparer variableComparer) {

+      Contract.Requires(propFactory == null || cce.Owner.Same(lattice, propFactory));//TODO: Owner is Microsoft.Contracts (mscorlib.Contracts).Owner

+      Contract.Requires(linearFactory == null || cce.Owner.Same(lattice, linearFactory));

+      Contract.Requires(intFactory == null || cce.Owner.Same(lattice, intFactory));

+      Contract.Requires(valueFactory == null || cce.Owner.Same(lattice, valueFactory));

+      Contract.Requires(nullFactory == null || cce.Owner.Same(lattice, nullFactory));

+      Contract.Requires(variableComparer == null || cce.Owner.Same(lattice, variableComparer));

       // ensures Owner.Same(this, lattice);  // KRML: 

-    {

+

+      Contract.Requires(lattice != null);

       this.lattice = lattice;

 

       this.propFactory = propFactory;

@@ -978,69 +987,69 @@ namespace Microsoft.Boogie.AbstractInterpretation
       this.nullFactory = nullFactory;

       this.variableComparer = variableComparer;

     }

-    

+

   }

 

-public class AbstractInterpretation

-{

-	/// <summary>

-  /// Run the abstract interpretation.

-  /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn

-  /// </summary>

-  public static void RunAbstractInterpretation(Program! program) 

-  {

-    Helpers.ExtraTraceInformation("Starting abstract interpretation");

+  public class AbstractInterpretation {

+    /// <summary>

+    /// Run the abstract interpretation.

+    /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn

+    /// </summary>

+    public static void RunAbstractInterpretation(Program program) {

+      Contract.Requires(program != null);

+      Helpers.ExtraTraceInformation("Starting abstract interpretation");

+

+      if (CommandLineOptions.Clo.UseAbstractInterpretation) {

+        DateTime start = new DateTime();  // to please compiler's definite assignment rules

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine();

+          Console.WriteLine("Running abstract interpretation...");

+          start = DateTime.Now;

+        }

 

-    if(CommandLineOptions.Clo.UseAbstractInterpretation)    

-    {

-      DateTime start = new DateTime();  // to please compiler's definite assignment rules

-      if (CommandLineOptions.Clo.Trace) {

-        Console.WriteLine();

-        Console.WriteLine("Running abstract interpretation...");

-        start = DateTime.Now;

-      }

+        WidenPoints.Compute(program);

 

-      WidenPoints.Compute(program);

-      

-      if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)

-      {             

-        AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;

-        ApplyAbstractInterpretation(program, lattice);

+        if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)

+      {

+          AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;

+          ApplyAbstractInterpretation(program, lattice);

 

-        if (CommandLineOptions.Clo.Ai.DebugStatistics) 

-        {

-          Console.Error.WriteLine(lattice);

-        }

-      }

-      else    // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)

+          if (CommandLineOptions.Clo.Ai.DebugStatistics) {

+            Console.Error.WriteLine(lattice);

+          }

+        } else    // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)

       {

-        AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;

-        ApplyAbstractInterpretation(program, lattice);

-      }  

-    

-      program.InstrumentWithInvariants();

-

-      if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.Now;

-        TimeSpan elapsed = end - start;

-        Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

-        Console.Out.Flush();

+          AI.Lattice lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;

+          Contract.Assert(lattice != null);

+          ApplyAbstractInterpretation(program, lattice);

+        }

+

+        program.InstrumentWithInvariants();

+

+        if (CommandLineOptions.Clo.Trace) {

+          DateTime end = DateTime.Now;

+          TimeSpan elapsed = end - start;

+          Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

+          Console.Out.Flush();

+        }

       }

     }

-  }

 

-	static void ApplyAbstractInterpretation (Program! program, AI.Lattice! lattice) 

-    {

+    static void ApplyAbstractInterpretation(Program program, AI.Lattice lattice) {

+      Contract.Requires(program != null);

+      Contract.Requires(lattice != null);

       AbstractionEngine engine = new AbstractionEngine(lattice);

       engine.ComputeProgramInvariants(program);

       callGraph = engine.CallGraph;

     }

     private static Cci.IGraphNavigator callGraph;

     public static Cci.IGraphNavigator CallGraph {

-      get { return callGraph; } 

+      get {

+        return callGraph;

+      }

     }

-    

-    

-}

-	 

-} // namespace

+

+

+  }

+

+} // namespace
\ No newline at end of file
diff --git a/Source/AbsInt/AbstractInterpretation.ssc b/Source/AbsInt/AbstractInterpretation.ssc
deleted file mode 100644
index ee5a1f06..00000000
--- a/Source/AbsInt/AbstractInterpretation.ssc
+++ /dev/null
@@ -1,1046 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using Microsoft.Contracts;

-

-namespace Microsoft.Boogie.AbstractInterpretation

-{

-  using System;

-  using System.Collections;

-  using System.Collections.Generic;  

-  using System.Diagnostics;

-  using Microsoft.Boogie;

-  using Cci = System.Compiler;

-  using AI = Microsoft.AbstractInterpretationFramework;

-  using Microsoft.Contracts;

-

-  /// <summary>

-  /// Defines invariant propagation methods over ASTs for an abstract interpretation policy.

-  /// </summary>

-  public class AbstractionEngine 

-  {

-    private AI.Lattice! lattice;

-    private Queue<ProcedureWorkItem!>! procWorkItems;  //PM: changed to generic queue

-    private Queue/*<CallSite>*/! callReturnWorkItems;

-    private Cci.IRelation/*<Procedure,Implementation>*/ procedureImplementations;

-           

-    private class ProcedureWorkItem

-    {

-      [Rep]  // KRML: this doesn't seem like the right designation to me; but I'm not sure what is

-      public Procedure! Proc;

-      public int Index; // pre state is Impl.Summary[Index]

-   

-      invariant 0 <= Index && Index < Proc.Summary.Count;

-

-      public ProcedureWorkItem ([Captured] Procedure! p, AI.Lattice.Element! v, AI.Lattice! lattice)

-        ensures p == Proc; 

-      {

-        this.Proc = p;

-        p.Summary.Add(new ProcedureSummaryEntry(lattice, v));

-        this.Index = p.Summary.Count - 1;

-        // KRML: axioms are now in place:  assume 0 <= Index && Index < Proc.Summary.Count; //PM: Should not be necessary once axioms for pure methods are there

-      }

-    }

-

-    private readonly static AI.Logger! log = new AI.Logger("Engine");

-

-    public AbstractionEngine (AI.Lattice! lattice) 

-    {

-      assume log.IsExposable;  //PM: One would need static class invariants to prove this property

-      expose(log) { 

-        log.Enabled = AI.Lattice.LogSwitch;

-      }

-      this.lattice = lattice; 

-      this.procWorkItems = new Queue<ProcedureWorkItem!>();

-      this.callReturnWorkItems = new Queue();

-    }

-

-    private Cci.IGraphNavigator ComputeCallGraph (Program! program)

-      ensures this.procedureImplementations != null;

-    {

-      // Since implementations call procedures (impl. signatures) 

-      // rather than directly calling other implementations, we first

-      // need to compute which implementations implement which

-      // procedures and remember which implementations call which

-      // procedures.

-

-      Cci.IMutableRelation/*<Implementation,Procedure>*/ callsProcedure = new Cci.Relation();

-      Cci.IMutableRelation/*<Procedure,Implementation>*/ implementsProcedure = new Cci.Relation();

-      this.procedureImplementations = implementsProcedure;

-      

-//      ArrayList publics = new ArrayList();

-//      publicImpls = publics;

-

-      foreach (Declaration member in program.TopLevelDeclarations)

-      {

-        Implementation impl = member as Implementation;

-        if (impl != null) 

-        {

-          implementsProcedure.Add(impl.Proc, impl);

- //         if (impl.IsPublic) { publics.Add(impl); }          // PR: what does "IsPublic" stand for?

-

-          foreach (Block block in impl.Blocks)

-          {

-            foreach (Cmd cmd in block.Cmds)

-            {

-              CallCmd call = cmd as CallCmd;

-              if (call != null)

-              {

-                callsProcedure.Add(impl, call.Proc);

-              }

-            }

-          }

-        }

-      }

-      

-      // Now compute a graph from implementations to implementations.

-

-      Cci.GraphBuilder callGraph = new Cci.GraphBuilder();

-

-      IEnumerable callerImpls = callsProcedure.GetKeys();

-      assume callerImpls != null;  // because of non-generic collection

-      foreach (Implementation caller in callerImpls)

-      {

-        IEnumerable callerProcs = callsProcedure.GetValues(caller);

-        assume callerProcs != null;  // because of non-generic collection

-        foreach (Procedure callee in callerProcs)

-        {

-          IEnumerable calleeImpls = implementsProcedure.GetValues(callee);

-          assume calleeImpls != null;  // because of non-generic collection

-          foreach (Implementation calleeImpl in calleeImpls)

-          {

-            callGraph.AddEdge(caller, calleeImpl);

-          }

-        }

-      }

-      

-      return callGraph;

-    }

-

-#if OLDCODE

-    public void ComputeImplementationInvariants (Implementation impl)

-    {

-        // process each procedure implementation by recursively processing the first (entry) block...

-        ComputeBlockInvariants(impl.Blocks[0], lattice.Top);

-

-        // compute the procedure invariant by joining all terminal block invariants...

-        AI.Lattice.Element post = lattice.Bottom;

-        foreach (Block block in impl.Blocks) 

-        {

-            if (block.TransferCmd is ReturnCmd) 

-            {

-                AI.Lattice.Element postValue = block.PostInvariantBuckets[invariantIndex];

-                Debug.Assert(postValue != null);

-                post = post.Join(postValue);

-            }

-        }

-        impl.PostInvariant = post;

-

-        // Now update the procedure to reflect the new properties

-        // of this implementation.

-

-        if (impl.Proc.PreInvariant <= impl.PreInvariant)

-        {

-            // Strengthen the precondition

-            impl.Proc.PreInvariant = impl.PreInvariant;

-            foreach (Implementation otherImpl in this.procedureImplementations.GetValues(impl.Proc))

-            {

-                if (otherImpl == impl) { continue; }

-                if (otherImpl.PreInvariant <= impl.Proc.PreInvariant)

-                {

-                    // If another implementation of the same procedure has

-                    // a weaker precondition, re-do it with the stronger

-                    // precondition.

-                    otherImpl.PreInvariant = impl.Proc.PreInvariant;

-                    this.implWorkItems.Enqueue(otherImpl);

-                }

-            }

-        }

-    }

-#endif

-

-

-#if NOTYET

-    public void ComputeSccInvariants (IEnumerable/*<Implementation>*/ implementations)

-    {

-      Debug.Assert(this.implWorkItems.Count == 0); // no work left over from last SCC

-

-      foreach (Implementation impl in implementations) 

-      { 

-        impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom);

-        this.implWorkItems.Enqueue(impl); 

-      }

-

-      while (this.implWorkItems.Count > 0) // until fixed point reached

-      {

-        Implementation impl = (Implementation)this.implWorkItems.Dequeue();

-      }

-    }

-#endif

-

-    public AI.Lattice.Element! ApplyProcedureSummary (CallCmd! call, Implementation! caller, AI.Lattice.Element! knownAtCallSite, CallSite! callSite)

-      requires call.Proc != null; 

-    {

-      Procedure! proc = call.Proc;

-

-      // NOTE: Here, we count on the fact that an implementation's variables

-      // are distinct from an implementation's procedure's variables. So, even for

-      // a recursive implementation, we're free to use the implementation's

-      // procedure's input parameters as though they were temporary local variables.

-      //

-      // Hence, in the program

-      //    procedure Foo (i:int);  implementation Foo (i':int) { ...call Foo(i'+1)... }

-      // we can treat the recursive call as

-      //    i:=i'+1; call Foo(i);

-      // where the notation i' means a variable with the same (string) name as i, 

-      // but a different identity.

-

-      AI.Lattice.Element! relevantToCall = knownAtCallSite;

-      for (int i=0; i<proc.InParams.Length; i++)

-      {

-        // "Assign" the actual expressions to the corresponding formal variables.

-        assume proc.InParams[i] != null;  //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

-        assume call.Ins[i] != null;       //PM: this can be fixed once VariableSeq is replaced by List<Variable!>;

-        Expr equality = Expr.Eq(Expr.Ident( (!) proc.InParams[i]), (!) call.Ins[i]);

-        relevantToCall = lattice.Constrain(relevantToCall, equality.IExpr);

-      }

-      foreach (Variable! var in caller.LocVars) {

-          relevantToCall = this.lattice.Eliminate(relevantToCall, var);

-      }

-

-      ProcedureSummary! summary = proc.Summary;

-      ProcedureSummaryEntry applicableEntry = null;

-

-      for (int i=0; i<summary.Count; i++)

-      {

-        ProcedureSummaryEntry! current = (!) summary[i];

-

-        if (lattice.Equivalent(current.OnEntry, relevantToCall))

-        {

-          applicableEntry = current;

-          break;

-        }

-      }

-

-      // Not found in current map, so add new entry.

-      if (applicableEntry == null)

-      {

-        ProcedureWorkItem! newWorkItem = new ProcedureWorkItem(proc, relevantToCall, lattice);

-        this.procWorkItems.Enqueue(newWorkItem);

-        applicableEntry = (!)  proc.Summary[newWorkItem.Index];

-      }

-      applicableEntry.ReturnPoints.Add(callSite);

-      

-

-      AI.Lattice.Element atReturn = applicableEntry.OnExit;

-

-      for (int i=0; i<call.Outs.Count; i++)

-      {

-        atReturn = this.lattice.Rename(atReturn, (!) call.Proc.OutParams[i], (!)((!) call.Outs[i]).Decl);

-        knownAtCallSite = this.lattice.Eliminate(knownAtCallSite, (!)((!) call.Outs[i]).Decl);

-      }

-

-      return this.lattice.Meet(atReturn, knownAtCallSite);

-    }

-

-    private Cci.IGraphNavigator callGraph;

-    public Cci.IGraphNavigator CallGraph { 

-      get { return this.callGraph; } 

-    } 

-     

-    /// <summary>

-    /// Compute the invariants for the program using the underlying abstract domain

-    /// </summary>

-    public void ComputeProgramInvariants (Program! program) 

-    {        

-      

-#if NOT_YET

-      Cci.IGraphNavigator callGraph = 

-#endif

-

-      callGraph = this.ComputeCallGraph(program);

-      assert this.procedureImplementations != null;

-      Cci.IRelation! procedureImplementations = this.procedureImplementations;

-

-#if NOT_YET

-      IEnumerable/*<IStronglyConnectedComponent>*/ sccs = 

-          StronglyConnectedComponent.ConstructSCCs(publicImpls, callGraph);

-

-      IList/*<IStronglyConnectedComponent>*/ sortedSccs = 

-          GraphUtil.TopologicallySortComponentGraph(sccs);

-

-      // Go bottom-up through the SCCs of the call graph

-      foreach (IStronglyConnectedComponent scc in sortedSccs)

-      {

-        this.ComputeSccInvariants(scc.Nodes);

-      }

-#endif

-      AI.Lattice.Element! initialElement = this.lattice.Top;

-      // Gather all the axioms to create the initial lattice element

-      // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain

-

-      foreach (Declaration decl in program.TopLevelDeclarations)

-      {

-        Axiom ax = decl as Axiom;

-        if (ax != null)

-        {

-          initialElement = this.lattice.Constrain(initialElement, ax.Expr.IExpr);

-        }

-      }

-

-      // propagate over all procedures...

-      foreach (Declaration decl in program.TopLevelDeclarations)

-      {

-        Procedure proc = decl as Procedure;

-        if (proc != null) 

-        {

-          this.procWorkItems.Enqueue(new ProcedureWorkItem(proc, initialElement, this.lattice));

-        }

-      }

-

-      // analyze all the procedures...

-      while (this.procWorkItems.Count + this.callReturnWorkItems.Count > 0)

-      {

-        while (this.procWorkItems.Count > 0)

-        {

-          ProcedureWorkItem workItem = this.procWorkItems.Dequeue();

-

-          ProcedureSummaryEntry summaryEntry = (!) workItem.Proc.Summary[workItem.Index];

-

-          if (((!) procedureImplementations.GetValues(workItem.Proc)).Count == 0)

-          {

-            // This procedure has no given implementations.  We therefore treat the procedure

-            // according to its specification only.

-

-            if (!CommandLineOptions.Clo.IntraproceduralInfer)

-            {

-              AI.Lattice.Element post = summaryEntry.OnEntry;

-              // BUGBUG.  Here, we should process "post" according to the requires, modifies, ensures

-              // specification of the procedure, including any OLD expressions in the postcondition.

-              AI.Lattice.Element atReturn = post;

-

-              if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))

-              {

-                // If the results of this analysis are strictly worse than

-                // what we previous knew for the same input assumptions,

-                // update the summary and re-do the call sites.

-

-                summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);

-

-                foreach (CallSite callSite in summaryEntry.ReturnPoints)

-                {

-                  this.callReturnWorkItems.Enqueue(callSite);

-                }

-              }

-            }

-          }

-          else

-          {

-            // There are implementations, so do inference based on those implementations

-

-            if (!CommandLineOptions.Clo.IntraproceduralInfer)

-            {

-              summaryEntry.OnExit = lattice.Bottom;

-            }

-

-            // For each implementation in the procedure...

-            foreach (Implementation! impl in (!) procedureImplementations.GetValues(workItem.Proc))

-            {

-              // process each procedure implementation by recursively processing the first (entry) block...

-              ((!)impl.Blocks[0]).Lattice = lattice;

-              ComputeBlockInvariants(impl, (!) impl.Blocks[0], summaryEntry.OnEntry, summaryEntry);

-              AdjustProcedureSummary(impl, summaryEntry);

-            }

-          }

-        }

-

-

-        while (this.callReturnWorkItems.Count > 0)

-        {

-          CallSite callSite = (CallSite!) this.callReturnWorkItems.Dequeue();

-

-          PropagateStartingAtStatement(callSite.Impl, callSite.Block, callSite.Statement, callSite.KnownBeforeCall, callSite.SummaryEntry);

-          AdjustProcedureSummary(callSite.Impl, callSite.SummaryEntry);

-        }

-

-      } // both queues

-

-    }

-    

-    void AdjustProcedureSummary(Implementation! impl, ProcedureSummaryEntry! summaryEntry)

-    {

-      if (CommandLineOptions.Clo.IntraproceduralInfer) {

-        return;  // no summary to adjust

-      }

-

-      // compute the procedure invariant by joining all terminal block invariants...

-      AI.Lattice.Element post = lattice.Bottom;

-      foreach (Block block in impl.Blocks) 

-      {

-        if (block.TransferCmd is ReturnCmd) 

-        {                 

-          // note: if program control cannot reach this block, then postValue will be null

-          if (block.PostInvariant != null) 

-          {

-            post = (AI.Lattice.Element) lattice.Join(post, block.PostInvariant);

-          }

-        }

-      }

-

-      AI.Lattice.Element atReturn = post;

-      foreach (Variable! var in impl.LocVars) 

-      {

-          atReturn = this.lattice.Eliminate(atReturn, var);

-      }

-      foreach (Variable! var in impl.InParams) 

-      {

-          atReturn = this.lattice.Eliminate(atReturn, var);

-      }

-

-      if ( ! this.lattice.LowerThan(atReturn, summaryEntry.OnExit))

-      {

-        // If the results of this analysis are strictly worse than

-        // what we previous knew for the same input assumptions,

-        // update the summary and re-do the call sites.

-

-        summaryEntry.OnExit = this.lattice.Join(summaryEntry.OnExit, atReturn);

-

-        foreach (CallSite! callSite in summaryEntry.ReturnPoints)

-        {

-          this.callReturnWorkItems.Enqueue(callSite);

-        }

-      }

-    }

-

-    private static int freshVarId = 0;

-    private static Variable! FreshVar(Boogie.Type! ty)

-    {

-      Variable fresh = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "fresh" + freshVarId, ty));

-      freshVarId++;

-      return fresh;

-    }

-    

-    private delegate CallSite! MarkCallSite(AI.Lattice.Element! currentValue);

-    

-    /// <summary>

-    /// Given a basic block, it propagates the abstract state at the entry point through the exit point of the block

-    /// <param name="impl"> The implementation that owns the block </param>

-    /// <param name="block"> The from where we propagate </param>

-    /// <param name="statementIndex">  </param> 

-    /// <param name="currentValue"> The initial value </param>

-    /// </summary>

-    private void PropagateStartingAtStatement (Implementation! impl, Block! block, int statementIndex, AI.Lattice.Element! currentValue,

-                                               ProcedureSummaryEntry! summaryEntry)

-    {

-      assume log.IsPeerConsistent;

-      log.DbgMsg(string.Format("{0}:", block.Label)); log.DbgMsgIndent();

-

-      #region Apply the abstract transition relation to the statements in the block

-      for (int cmdIndex = statementIndex; cmdIndex < block.Cmds.Length; cmdIndex++) 

-      {

-        Cmd! cmd = (!) block.Cmds[cmdIndex];              // Fetch the command

-        currentValue = Step(cmd, currentValue, impl,      // Apply the transition function

-                            delegate (AI.Lattice.Element! currentValue) 

-                            {

-                              return new CallSite(impl, block, cmdIndex, currentValue, summaryEntry);

-                            }

-                           );

-      }

-      

-      block.PostInvariant = currentValue;      // The invariant at the exit point of the block is that of the last statement

-           

-      log.DbgMsg(string.Format("pre   {0}", ((!)block.PreInvariant).ToString()));

-      log.DbgMsg(string.Format("post  {0}", (block.PostInvariant).ToString()));

-      log.DbgMsgUnindent();

-      #endregion    

-      #region Propagate the post-condition to the successor nodes

-      GotoCmd @goto = block.TransferCmd as GotoCmd;

-      if (@goto != null) 

-      {

-        // labelTargets is non-null after calling Resolve in a prior phase.

-        assume @goto.labelTargets != null;

-

-        // For all the successors of this block, propagate the abstract state

-        foreach (Block! succ in @goto.labelTargets) 

-        { 

-          if(impl.Blocks.Contains(succ))

-          {

-            succ.Lattice = block.Lattice;         // The lattice is the same

-                                                // Propagate the post-abstract state of this block to the successor

-            ComputeBlockInvariants(impl, succ, block.PostInvariant, summaryEntry);

-          }

-        }

-      }

-      #endregion

-    }

-

-    /// <summary>

-    /// The abstract transition relation.

-    /// </summary>

-    private AI.Lattice.Element! Step(Cmd! cmd, AI.Lattice.Element! pre, Implementation! impl, MarkCallSite/*?*/ callSiteMarker)

-    {

-      assume log.IsPeerConsistent;

-      log.DbgMsg(string.Format("{0}", cmd)); log.DbgMsgIndent();

-      

-      AI.Lattice.Element! currentValue = pre;

-      

-      // Case split...

-      #region AssignCmd

-      if (cmd is AssignCmd) { // parallel assignment

-        // we first eliminate map assignments

-        AssignCmd! assmt = ((AssignCmd)cmd).AsSimpleAssignCmd;

-        //PM: Assume variables have been resolved

-        assume forall {AssignLhs! lhs in assmt.Lhss;

-                       lhs.DeepAssignedVariable != null};

-

-        List<IdentifierExpr!>! freshLhs = new List<IdentifierExpr!> ();

-        foreach (AssignLhs! lhs in assmt.Lhss)

-          freshLhs.Add(Expr.Ident(FreshVar(((!)lhs.DeepAssignedVariable)

-                                           .TypedIdent.Type)));

-

-        for (int i = 0; i < freshLhs.Count; ++i)

-          currentValue =

-            this.lattice.Constrain(currentValue,

-                                   Expr.Eq(freshLhs[i], assmt.Rhss[i]).IExpr);

-        foreach (AssignLhs! lhs in assmt.Lhss)

-          currentValue =

-            this.lattice.Eliminate(currentValue, (!)lhs.DeepAssignedVariable);

-        for (int i = 0; i < freshLhs.Count; ++i)

-          currentValue =

-            this.lattice.Rename(currentValue, (!)freshLhs[i].Decl,

-                                (!)assmt.Lhss[i].DeepAssignedVariable);

-      }

-

-      /*

-      if (cmd is SimpleAssignCmd)

-      {

-        SimpleAssignCmd! assmt = (SimpleAssignCmd)cmd;

-        assume assmt.Lhs.Decl != null; //PM: Assume variables have been resolved

-        Variable! dest = assmt.Lhs.Decl;

-        Variable! fresh = FreshVar(dest.TypedIdent.Type);

-        IdentifierExpr newLhs = Expr.Ident(fresh);

-        Expr equality = Expr.Eq(newLhs, assmt.Rhs);

-

-        currentValue = this.lattice.Constrain(currentValue, equality.IExpr);

-        currentValue = this.lattice.Eliminate(currentValue, dest);

-        currentValue = this.lattice.Rename(currentValue, fresh, dest);

-      }

-      #endregion

-      #region ArrayAssignCmd

-      else if (cmd is ArrayAssignCmd)

-      {

-        ArrayAssignCmd assmt = (ArrayAssignCmd)cmd;

-        

-        assume assmt.Array.Type != null;  //PM: assume that type checker has run

-        ArrayType! arrayType = (ArrayType)assmt.Array.Type;

-        

-        Variable newHeapVar = FreshVar(arrayType);

-        IdentifierExpr newHeap = Expr.Ident(newHeapVar);

-        IdentifierExpr oldHeap = assmt.Array;

-        assume oldHeap.Decl != null; //PM: assume that variable has been resolved

-

-        // For now, we only know how to handle heaps

-        if (arrayType.IndexType0.IsRef && arrayType.IndexType1 != null && arrayType.IndexType1.IsName)

-        {

-          //PM: The following assertion follows from a nontrivial invariant of ArrayAssignCmd,

-          //PM: which we do not have yet. Therefore, we put in an assume fo now.

-          assume assmt.Index1 != null;

-          assert assmt.Index1 != null;          

-          // heap succession predicate

-          Expr heapsucc = Expr.HeapSucc(oldHeap, newHeap, assmt.Index0, assmt.Index1);

-

-          currentValue = this.lattice.Constrain(currentValue, heapsucc.IExpr);

-       

-        }   

-        else

-        {

-          // TODO: We can do this case as well if the heap succession array can handle non-heap arrays

-        }

-        // new select expression

-        IndexedExpr newLhs = new IndexedExpr(Token.NoToken, newHeap, assmt.Index0, assmt.Index1);

-        Expr equality = Expr.Eq(newLhs, assmt.Rhs);

-        

-        currentValue = this.lattice.Constrain(currentValue, equality.IExpr);

-        currentValue = this.lattice.Eliminate(currentValue, oldHeap.Decl);

-        currentValue = this.lattice.Rename(currentValue, newHeapVar, oldHeap.Decl);

-       

-     

-        } */

-      #endregion

-      #region Havoc

-      else if (cmd is HavocCmd)

-      {

-        HavocCmd havoc = (HavocCmd)cmd;

-        foreach (IdentifierExpr! id in havoc.Vars)

-        {

-          currentValue = this.lattice.Eliminate(currentValue, (!)id.Decl);

-        }

-      }

-      #endregion

-      #region PredicateCmd

-      else if (cmd is PredicateCmd)

-      {

-        //System.Console.WriteLine("Abstract State BEFORE " + ((PredicateCmd) cmd).Expr + " : " +this.lattice.ToPredicate(currentValue));

-

-        Expr! embeddedExpr = (!)((PredicateCmd)cmd).Expr;

-        List<Expr!>! conjuncts = flatConjunction(embeddedExpr);           // Handle "assume P && Q" as if it was "assume P; assume Q"

-        foreach(Expr! c in conjuncts) {

-          currentValue = this.lattice.Constrain(currentValue, c.IExpr);

-        }

-

-        //System.Console.WriteLine("Abstract State AFTER assert/assume "+ this.lattice.ToPredicate(currentValue));

-      }

-      #endregion

-      #region CallCmd

-      else if (cmd is CallCmd)

-      {

-        CallCmd call = (CallCmd)cmd;

-        

-        if (!CommandLineOptions.Clo.IntraproceduralInfer)

-        {

-          // Interprocedural analysis

-          

-          if (callSiteMarker == null)

-          {

-            throw new System.InvalidOperationException("INTERNAL ERROR: Context does not allow CallCmd.");

-          }

-          

-          CallSite here = callSiteMarker(currentValue);

-          currentValue = ApplyProcedureSummary(call, impl, currentValue, here);

-        }

-        else

-        {

-          // Intraprocedural analysis

-          

-          StateCmd statecmd = call.Desugaring as StateCmd;

-          if (statecmd != null)

-          {

-            // Iterate the abstract transition on all the commands in the desugaring of the call

-            foreach (Cmd! callDesug in statecmd.Cmds) { currentValue = Step(callDesug, currentValue, impl, null); }

-            

-            // Now, project out the local variables

-            foreach (Variable! local in statecmd.Locals) { currentValue = this.lattice.Eliminate(currentValue, local); }

-          }

-          else throw new System.InvalidOperationException("INTERNAL ERROR: CallCmd does not desugar to StateCmd.");

-        }

-      }

-      #endregion

-      #region CommentCmd

-      else if (cmd is CommentCmd)

-      {

-        // skip

-      }

-      #endregion      

-      else if (cmd is SugaredCmd)

-      {

-        // other sugared commands are treated like their desugaring

-        SugaredCmd sugar = (SugaredCmd)cmd;

-        Cmd desugaring = sugar.Desugaring;

-        if (desugaring is StateCmd) {

-          StateCmd statecmd = (StateCmd)desugaring;

-          // Iterate the abstract transition on all the commands in the desugaring of the call

-          foreach (Cmd! callDesug in statecmd.Cmds) { currentValue = Step(callDesug, currentValue, impl, null); }

-          // Now, project out the local variables

-          foreach (Variable! local in statecmd.Locals) { currentValue = this.lattice.Eliminate(currentValue, local); }

-        } else {

-          currentValue = Step(desugaring, currentValue, impl, null);

-        }

-      }

-      else

-      {

-          assert false;  // unknown command

-      }

-      

-      log.DbgMsgUnindent();

-      

-      return currentValue;

-    }

- 

-    /// <summary>

-    /// Flat an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]

-    /// </summary>

-    private List<Expr!>! flatConjunction(Expr! embeddedExpr) 

-    {

-      List<Expr!>! retValue = new List<Expr!>();

-      NAryExpr e = embeddedExpr as NAryExpr;

-      if(e != null && e.Fun.FunctionName.CompareTo("&&") == 0) {    // if it is a conjunction

-        foreach(Expr! arg in e.Args) 

-        {

-          List<Expr!>! newConjuncts = flatConjunction(arg);

-          retValue.AddRange(newConjuncts);

-        }          

-      }

-      else 

-      {     

-        retValue.Add(embeddedExpr);

-      }

-      return retValue;

-    }

-

-    /// <summary>

-    /// Compute the invariants for a basic block 

-    /// <param name="impl"> The implementation the block belongs to </param>

-    /// <param name="block">  The block for which we compute the invariants </param>

-    /// <param name="incomingValue">  The "init" abstract state for the block </param>

-    /// </summary>

-    private void ComputeBlockInvariants (Implementation! impl, Block! block, AI.Lattice.Element! incomingValue, ProcedureSummaryEntry! summaryEntry)

-    {

-      if (block.PreInvariant == null) // block has not yet been processed

-      {

-        assert block.PostInvariant == null;

-        

-        // To a first approximation the block is unreachable

-        block.PreInvariant = this.lattice.Bottom;

-        block.PostInvariant = this.lattice.Bottom;

-      }

-

-      assert block.PreInvariant != null;

-      assert block.PostInvariant != null;

-

-      #region Check if we have reached a postfixpoint

-

-      if (lattice.LowerThan(incomingValue, block.PreInvariant))

-      {

-        // We have reached a post-fixpoint, so we are done...

-#if DEBUG_PRINT

-        System.Console.WriteLine("@@ Compared for block {0}:", block.Label);

-        System.Console.WriteLine("@@ {0}", lattice.ToPredicate(incomingValue));

-        System.Console.WriteLine("@@ {0}", lattice.ToPredicate(block.PreInvariant));

-        System.Console.WriteLine("@@ result = True");

-        System.Console.WriteLine("@@ end Compare");

-#endif

-        return;

-      }

-#if DEBUG_PRINT

-      // Compute the free variables in incoming and block.PreInvariant

-      FreeVariablesVisitor freeVarsVisitorForA = new FreeVariablesVisitor();

-      FreeVariablesVisitor freeVarsVisitorForB = new FreeVariablesVisitor();

-

-      lattice.ToPredicate(incomingValue).DoVisit(freeVarsVisitorForA);

-      lattice.ToPredicate(block.PreInvariant).DoVisit(freeVarsVisitorForB);

-      

-      List<AI.IVariable!>! freeVarsOfA = freeVarsVisitorForA.FreeVariables; 

-      List<AI.IVariable!>! freeVarsOfB = freeVarsVisitorForB.FreeVariables; 

-

-      System.Console.WriteLine("@@ Compared for block {0}:", block.Label);

-      System.Console.WriteLine("@@ Incoming: {0}", lattice.ToPredicate((!) incomingValue));

-      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA)); 

-      System.Console.WriteLine("@@ Previous: {0}", lattice.ToPredicate(block.PreInvariant));

-      System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB)); 

-      System.Console.WriteLine("@@ result = False");

-      System.Console.WriteLine("@@ end Compare");

-      string operation = "";

-#endif

-      #endregion       

-      #region If it is not the case, then join or widen the incoming abstract state with the previous one

-      if (block.widenBlock)     // If the considered block is the entry point of a loop

-      {

-        if( block.iterations <= CommandLineOptions.Clo.StepsBeforeWidening+1)

-        {        

-#if DEBUG_PRINT 

-    operation = "join";

-#endif

-          block.PreInvariant = (AI.Lattice.Element) lattice.Join( block.PreInvariant, incomingValue);

-        }        

-        else

-        {

-#if DEBUG_PRINT

-      operation = "widening";

-#endif 

-

-            // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision

-        //    block.PreInvariant =  WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue);            

-         block.PreInvariant = (AI.Lattice.Element) lattice.Widen( block.PreInvariant, incomingValue);

-        }

-        block.iterations++;

-      } 

-      else 

-      {

-#if DEBUG_PRINT

-  operation = "join";

-#endif

-        block.PreInvariant = (AI.Lattice.Element) lattice.Join( block.PreInvariant, incomingValue);

-      }

-      

-#if DEBUG_PRINT

-      System.Console.WriteLine("@@ {0} for block {1}:", operation, block.Label);

-      System.Console.WriteLine("@@ {0}", lattice.ToPredicate(block.PreInvariant));

-      System.Console.WriteLine("@@ end");

-#endif

-      #endregion

-      #region Propagate the entry abstract state through the method

-        PropagateStartingAtStatement(impl, block, 0, (!) block.PreInvariant.Clone(), summaryEntry);

-      #endregion

-    }

-

-#if DEBUG_PRINT

-    private string! ToString(List<AI.IVariable!>! vars) 

-    {

-      string s = "";

-        

-      foreach(AI.IVariable! v in vars) 

-      {

-        s += v.Name +" ";

-      }

-      return s;

-    }

-#endif

-

-  } // class

-

-

-  /// <summary>

-  /// Defines a class for building the abstract domain according to the parameters switch

-  /// </summary>

-  public class AbstractDomainBuilder

-  {

-

-    private AbstractDomainBuilder()

-    { /* do nothing */ }

-  

-    /// <summary>

-    /// Return a fresh instance of the abstract domain of intervals

-    /// </summary>

-    static public AbstractAlgebra! BuildIntervalsAbstractDomain() 

-    { 

-      AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();

-      AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();     

-      AI.IValueExprFactory valuefactory = new BoogieValueFactory();

-      IComparer variableComparer = new VariableComparer();

-

-      AbstractAlgebra! retAlgebra;

-      AI.Lattice! intervals = new AI.VariableMapLattice(propfactory, valuefactory, new AI.IntervalLattice(linearfactory), variableComparer);

-

-      retAlgebra = new AbstractAlgebra(intervals, propfactory, linearfactory, null, valuefactory, null, variableComparer);    

-

-      return retAlgebra;

-    }

-

-    /// <summary>

-    /// Return a fresh abstract domain, according to the parameters specified by the command line

-    /// </summary>

-    static public AbstractAlgebra! BuildAbstractDomain()

-    {

-        AbstractAlgebra! retAlgebra;

-      

-        AI.Lattice! returnLattice;

-

-        AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();

-        AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();

-        AI.IIntExprFactory intfactory = new BoogieIntFactory();

-        AI.IValueExprFactory valuefactory = new BoogieValueFactory();

-        AI.INullnessFactory nullfactory = new BoogieNullnessFactory();

-        IComparer variableComparer = new VariableComparer();

-

-        AI.MultiLattice multilattice = new AI.MultiLattice(propfactory, valuefactory);

-

-        if (CommandLineOptions.Clo.Ai.Intervals)        // Intervals

-        {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                  new AI.IntervalLattice(linearfactory),

-                                  variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Constant)         // Constant propagation

-

-        {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                  new AI.ConstantLattice(intfactory),

-                                  variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.DynamicType)      // Class types

-        {

-          BoogieTypeFactory typeFactory = new BoogieTypeFactory();

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                                    new AI.DynamicTypeLattice(typeFactory, propfactory),

-                                                    variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Nullness)       // Nullness

-        {

-          multilattice.AddLattice(new AI.VariableMapLattice(propfactory, valuefactory,

-                                                    new AI.NullnessLattice(nullfactory),

-                                                    variableComparer));

-        }

-        if (CommandLineOptions.Clo.Ai.Polyhedra)    // Polyhedra

-        {

-          multilattice.AddLattice(new AI.PolyhedraLattice(linearfactory, propfactory));

-        }

-        

-                

-        returnLattice = multilattice;

-        if (CommandLineOptions.Clo.Ai.DebugStatistics) 

-        {

-          returnLattice = new AI.StatisticsLattice(returnLattice);

-        }

-

-        returnLattice.Validate();

-

-        retAlgebra = new AbstractAlgebra(returnLattice, propfactory, linearfactory, intfactory, valuefactory, nullfactory, 

-                                                        variableComparer);

-

-        return retAlgebra;

-

-    }

-  } 

-  

-  /// <summary>

-  /// An Abstract Algebra is a tuple made of a Lattice and several factories

-  /// </summary>

-  public class AbstractAlgebra

-  {

-    [Peer] private AI.Lattice! lattice;

-    [Peer] private AI.IQuantPropExprFactory propFactory;

-    [Peer] private AI.ILinearExprFactory linearFactory;

-    [Peer] private AI.IIntExprFactory intFactory;

-    [Peer] private AI.IValueExprFactory valueFactory;

-    [Peer] private AI.INullnessFactory nullFactory;

-    [Peer] private IComparer variableComparer;

-

-    public AI.Lattice! Lattice

-    {

-      get

-      {

-        return lattice; 

-      }

-    }      

-

-    public AI.IQuantPropExprFactory PropositionFactory

-    {

-      get

-      {

-        return this.propFactory;

-      }

-    }

-

-    public AI.ILinearExprFactory LinearExprFactory

-    {

-      get

-      {

-        return this.linearFactory;

-      }

-    }

-

-    public AI.IIntExprFactory IntExprFactory

-    {

-      get

-      {

-        return this.intFactory;

-      }

-    }

-

-    public AI.IValueExprFactory ValueFactory

-    {

-      get

-      {

-        return this.valueFactory;

-      }

-    }

-    

-    public AI.INullnessFactory NullFactory

-    {

-      get

-      {

-        return this.nullFactory;

-      }

-    }

-

-    public IComparer VariableComparer

-    {

-      get

-      {

-        return this.variableComparer;

-      }

-    }

-

-    [Captured]

-    public AbstractAlgebra(AI.Lattice! lattice, 

-                          AI.IQuantPropExprFactory propFactory, 

-                          AI.ILinearExprFactory linearFactory,

-                          AI.IIntExprFactory intFactory,

-                          AI.IValueExprFactory valueFactory,

-                          AI.INullnessFactory nullFactory,

-                          IComparer variableComparer)

-      requires propFactory != null ==> Owner.Same(lattice, propFactory);

-      requires linearFactory != null ==> Owner.Same(lattice, linearFactory);

-      requires intFactory != null ==> Owner.Same(lattice, intFactory);

-      requires valueFactory != null ==> Owner.Same(lattice, valueFactory);

-      requires nullFactory != null ==> Owner.Same(lattice, nullFactory);

-      requires variableComparer != null ==> Owner.Same(lattice, variableComparer);

-      // ensures Owner.Same(this, lattice);  // KRML: 

-    {

-      this.lattice = lattice;

-

-      this.propFactory = propFactory;

-      this.linearFactory = linearFactory;

-      this.intFactory = intFactory;

-      this.valueFactory = valueFactory;

-      this.nullFactory = nullFactory;

-      this.variableComparer = variableComparer;

-    }

-    

-  }

-

-public class AbstractInterpretation

-{

-	/// <summary>

-  /// Run the abstract interpretation.

-  /// It has two entry points. One is the RunBoogie method. The other is the CCI PlugIn

-  /// </summary>

-  public static void RunAbstractInterpretation(Program! program) 

-  {

-    Helpers.ExtraTraceInformation("Starting abstract interpretation");

-

-    if(CommandLineOptions.Clo.UseAbstractInterpretation)    

-    {

-      DateTime start = new DateTime();  // to please compiler's definite assignment rules

-      if (CommandLineOptions.Clo.Trace) {

-        Console.WriteLine();

-        Console.WriteLine("Running abstract interpretation...");

-        start = DateTime.Now;

-      }

-

-      WidenPoints.Compute(program);

-      

-      if (CommandLineOptions.Clo.Ai.AnySet) // if there is some user defined domain we override the default (= intervals)

-      {             

-        AI.Lattice lattice = AbstractDomainBuilder.BuildAbstractDomain().Lattice;

-        ApplyAbstractInterpretation(program, lattice);

-

-        if (CommandLineOptions.Clo.Ai.DebugStatistics) 

-        {

-          Console.Error.WriteLine(lattice);

-        }

-      }

-      else    // Otherwise the default is the use of the abstract domain of intervals (useful for simple for loops)

-      {

-        AI.Lattice! lattice = AbstractDomainBuilder.BuildIntervalsAbstractDomain().Lattice;

-        ApplyAbstractInterpretation(program, lattice);

-      }  

-    

-      program.InstrumentWithInvariants();

-

-      if (CommandLineOptions.Clo.Trace) {

-        DateTime end = DateTime.Now;

-        TimeSpan elapsed = end - start;

-        Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

-        Console.Out.Flush();

-      }

-    }

-  }

-

-	static void ApplyAbstractInterpretation (Program! program, AI.Lattice! lattice) 

-    {

-      AbstractionEngine engine = new AbstractionEngine(lattice);

-      engine.ComputeProgramInvariants(program);

-      callGraph = engine.CallGraph;

-    }

-    private static Cci.IGraphNavigator callGraph;

-    public static Cci.IGraphNavigator CallGraph {

-      get { return callGraph; } 

-    }

-    

-    

-}

-	 

-} // namespace

diff --git a/Source/AbsInt/AssemblyInfo.ssc b/Source/AbsInt/AssemblyInfo.ssc
deleted file mode 100644
index 6ed99a25..00000000
--- a/Source/AbsInt/AssemblyInfo.ssc
+++ /dev/null
@@ -1,4 +0,0 @@
-using System.Reflection;

-using System.Runtime.CompilerServices;

-

-[assembly: AssemblyKeyFile("..\\InterimKey.snk")]

diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs
index ad090f2b..7979f061 100644
--- a/Source/AbsInt/ExprFactories.cs
+++ b/Source/AbsInt/ExprFactories.cs
@@ -5,227 +5,313 @@
 //-----------------------------------------------------------------------------

 using Microsoft.Boogie;

 using AI = Microsoft.AbstractInterpretationFramework;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 

 namespace Microsoft.Boogie.AbstractInterpretation {

 

-    public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory

-    {

-        public AI.IFunApp! False {

-            get {

+  public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory {

+    public AI.IFunApp False {

+      get {

+        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-                return Expr.False;

-            }

-        }

-        public AI.IFunApp! True {

-            get {

-                return Expr.True;

-            }

-        }

+        return Expr.False;

+      }

+    }

+    public AI.IFunApp True {

+      get {

+        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-        public AI.IFunApp! Not(AI.IExpr! p) {

-            return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));

-        }

+        return Expr.True;

+      }

+    }

 

-        public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Or(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Implies(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Exists(AI.IFunction! p) {

-            return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

-        }

-        public AI.IFunApp! Exists(AI.AIType paramType, AI.FunctionBody! bodygen) {

-            // generate a fresh new variable

-            Variable! var = FreshBoundVariable(paramType);

-            Expr! expr = IExpr2Expr(bodygen(var));

-            return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

-        }

-        

-        public AI.IFunApp! Forall(AI.IFunction! p) {

-            return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

-        }

-        public AI.IFunApp! Forall(AI.AIType paramType, AI.FunctionBody! bodygen) {

-            // generate a fresh new variable

-            Variable! var = FreshBoundVariable(paramType);

-            Expr! expr = IExpr2Expr(bodygen(var));

-            return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

-        }

-        

-        private static int freshVarNum = 0;

-        private static Variable! FreshBoundVariable(AI.AIType paramType)

-        {

-          // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type

-          // to make this new variable?  For now, we use Type.Any.

-          Type! t = Type.Int;

-        /*

-          if (paramType is AI.Ref)

-            t = Type.Ref;

-          else if (paramType is AI.FieldName)

-            t = Type.Name;

-          else

-            System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */

-          assert false;

-          TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);

-          freshVarNum++;

-          return new BoundVariable(Token.NoToken, id);

-        }

+    public AI.IFunApp Not(AI.IExpr p) {

+      Contract.Requires(p != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));

     }

-    

-    public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory

-    {

-        public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

+

+    public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

+      Contract.Requires(p != null);

+      Contract.Requires(q != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

     }

-    

-    public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory

-    {

-        public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

 

-        public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

+    public AI.IFunApp Or(AI.IExpr p, AI.IExpr q) {

+      Contract.Requires(p != null);

+      Contract.Requires(q != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));

+    }

 

-        public AI.IFunApp! Null {

-            get {

-                assert false;       // don't know where to get null from

-            }

-        }

+    public AI.IFunApp Implies(AI.IExpr p, AI.IExpr q) {

+      Contract.Requires(p != null);

+      Contract.Requires(q != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));

     }

 

-    public class BoogieIntFactory : BoogieValueFactory, AI.IIntExprFactory {

-        public AI.IFunApp! Const(BigNum i) {

-            return new LiteralExpr(Token.NoToken, i);

-        }

+    public AI.IFunApp Exists(AI.IFunction p) {

+      Contract.Requires(p != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

     }

-    

-    public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {

-        public AI.IFunApp! AtMost(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IFunApp! Add(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IExpr! Term(Rational r, AI.IVariable var) {

-            if (var != null && r == Rational.ONE) {

-                return var;

-            } else {

-                Expr! product;

-                if (r.IsIntegral) {

-                    product = Expr.Literal(r.AsBigNum);

-                } else {

-                    product = Expr.Div(Expr.Literal(r.Numerator), Expr.Literal(r.Denominator));

-                }

-                if (var != null) {

-                    product = Expr.Mul(product, IExpr2Expr(var));

-                }

-                return product.IExpr;

-            }

-        }

+    public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) {

+      Contract.Requires(bodygen != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-        public AI.IFunApp! False {

-            get {

-                return Expr.False;

-            }

-        }

-        public AI.IFunApp! True {

-            get {

-                return Expr.True;

-            }

+      // generate a fresh new variable

+      Variable var = FreshBoundVariable(paramType);

+      Contract.Assert(var != null);

+      Expr expr = IExpr2Expr(bodygen(var));

+      Contract.Assert(expr != null);

+      return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

+    }

+

+    public AI.IFunApp Forall(AI.IFunction p) {

+      Contract.Requires(p != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

+    }

+    public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) {

+      Contract.Requires(bodygen != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      // generate a fresh new variable

+      Variable var = FreshBoundVariable(paramType);

+      Contract.Assert(var != null);

+      Expr expr = IExpr2Expr(bodygen(var));

+      Contract.Assert(expr != null);

+      return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

+    }

+

+    private static int freshVarNum = 0;

+    private static Variable FreshBoundVariable(AI.AIType paramType) {

+      Contract.Ensures(Contract.Result<Variable>() != null);

+

+      // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type

+      // to make this new variable?  For now, we use Type.Any.

+      Type t = Type.Int;

+      Contract.Assert(t != null);

+      /*

+        if (paramType is AI.Ref)

+          t = Type.Ref;

+        else if (paramType is AI.FieldName)

+          t = Type.Name;

+        else

+          System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

+      TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);

+      freshVarNum++;

+      return new BoundVariable(Token.NoToken, id);

+    }

+  }

+

+  public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory {

+    public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+    public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+  }

+

+  public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory {

+    public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+

+    public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+

+    public AI.IFunApp Null {

+      get {

+        Contract.Assert(false);       // don't know where to get null from\

+        throw new cce.UnreachableException();

+      }

+    }

+  }

+

+  public class BoogieIntFactory : BoogieValueFactory, AI.IIntExprFactory {

+    public AI.IFunApp Const(BigNum i) {

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      return new LiteralExpr(Token.NoToken, i);

+    }

+  }

+

+  public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {

+    public AI.IFunApp AtMost(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+    public AI.IFunApp Add(AI.IExpr e0, AI.IExpr e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+      return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));

+    }

+    public AI.IExpr Term(Rational r, AI.IVariable var) {

+      Contract.Ensures(Contract.Result<AI.IExpr>() != null);

+

+      if (var != null && r == Rational.ONE) {

+        return var;

+      } else {

+        Expr product;

+        if (r.IsIntegral) {

+          product = Expr.Literal(r.AsBigNum);

+        } else {

+          product = Expr.Div(Expr.Literal(r.Numerator), Expr.Literal(r.Denominator));

         }

-        public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

+        if (var != null) {

+          product = Expr.Mul(product, IExpr2Expr(var));

         }

+        return product.IExpr;

+      }

     }

 

-    public class BoogieTypeFactory : BoogieFactory, AI.ITypeExprFactory {

-        /// <summary>

-        /// Returns an expression denoting the top of the type hierarchy.

-        /// </summary>

-        public AI.IExpr! RootType {

-            get {

-                assert false;  // BUGBUG: TODO

-                throw new System.NotImplementedException();

-            }

-        }

+    public AI.IFunApp False {

+      get {

+        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-        /// <summary>

-        /// Returns true iff "t" denotes a type constant.

-        /// </summary>

-        [Pure]

-        public bool IsTypeConstant(AI.IExpr! t) 

-          ensures result == (t is Constant);  

-        {

-            return t is Constant;

-        }

+        return Expr.False;

+      }

+    }

+    public AI.IFunApp True {

+      get {

+        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-        /// <summary>

-        /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.

-        /// </summary>

-        [Pure]

-        public bool IsTypeEqual(AI.IExpr! t0, AI.IExpr! t1) {

-            Constant c0 = t0 as Constant;

-            Constant c1 = t1 as Constant;

-            return c0 != null && c1 != null && c0 == c1;

-        }

+        return Expr.True;

+      }

+    }

+    public AI.IFunApp And(AI.IExpr p, AI.IExpr q) {

+      Contract.Requires(p != null);

+      Contract.Requires(q != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

 

-        /// <summary>

-        /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.

-        /// </summary>

-        [Pure]

-        public bool IsSubType(AI.IExpr! t0, AI.IExpr! t1) {

-            assert false;  // BUGBUG: TODO

-        }

+      return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

+    }

+  }

 

-        /// <summary>

-        /// Returns the most derived supertype of both "t0" and "t1".  A precondition is

-        /// that "t0" and "t1" both represent types.

-        /// </summary>

-        public AI.IExpr! JoinTypes(AI.IExpr! t0, AI.IExpr! t1) {

-            assert false;  // BUGBUG: TODO

-        }

+  public class BoogieTypeFactory : BoogieFactory, AI.ITypeExprFactory {

+    /// <summary>

+    /// Returns an expression denoting the top of the type hierarchy.

+    /// </summary>

+    public AI.IExpr RootType {

+      get {

+        Contract.Assert(false);  // BUGBUG: TODO

+        throw new System.NotImplementedException();

+      }

+    }

 

-        public AI.IFunApp! IsExactlyA(AI.IExpr! e, AI.IExpr! type) {

-            //PM: We need this assume because Boogie does not yet allow us to use the

-            //PM: inherited precondition "requires IsTypeConstant(type)".

-            //PM: Note that that precondition is currently commented out.

-            assume type is Constant;

-            Constant theType = (Constant)type;

-            assert false;

-            Expr typeofExpr = new NAryExpr(Token.NoToken,

-                new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

-                                 )),

-                new ExprSeq(IExpr2Expr(e)));

-            return Expr.Eq(typeofExpr, Expr.Ident(theType));

-        }

+    /// <summary>

+    /// Returns true iff "t" denotes a type constant.

+    /// </summary>

+    [Pure]

+    public bool IsTypeConstant(AI.IExpr t) {

+      Contract.Requires(t != null);

+      Contract.Ensures(Contract.Result<bool>() == (t is Constant));

+      return t is Constant;

+    }

 

-        public AI.IFunApp! IsA(AI.IExpr! e, AI.IExpr! type) {

-            //PM: We need this assume because Boogie does not yet allow us to use the

-            //PM: inherited precondition "requires IsTypeConstant(type)".

-            //PM: Note that that precondition is currently commented out.

-            assume type is Constant;

-            assert false;

-            Expr typeofExpr = new NAryExpr(Token.NoToken,

-                new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

-                                 )),

-                new ExprSeq(IExpr2Expr(e)));

-            return new NAryExpr(Token.NoToken,

-                new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Subtype),

-                new ExprSeq(typeofExpr, IExpr2Expr(e)));

-        }

+    /// <summary>

+    /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.

+    /// </summary>

+    [Pure]

+    public bool IsTypeEqual(AI.IExpr t0, AI.IExpr t1) {

+      Contract.Requires(t0 != null);

+      Contract.Requires(t1 != null);

+      Constant c0 = t0 as Constant;

+      Constant c1 = t1 as Constant;

+      return c0 != null && c1 != null && c0 == c1;

+    }

+

+    /// <summary>

+    /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.

+    /// </summary>

+    [Pure]

+    public bool IsSubType(AI.IExpr t0, AI.IExpr t1) {

+      Contract.Requires(t0 != null);

+      Contract.Requires(t1 != null);

+

+      Contract.Assert(false);  // BUGBUG: TODO

+      throw new cce.UnreachableException();

+    }

+

+    /// <summary>

+    /// Returns the most derived supertype of both "t0" and "t1".  A precondition is

+    /// that "t0" and "t1" both represent types.

+    /// </summary>

+    public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) {

+      Contract.Requires(t0 != null);

+      Contract.Requires(t1 != null);

+      Contract.Ensures(Contract.Result<AI.IExpr>() != null);

+

+

+      Contract.Assert(false);  // BUGBUG: TODO

+      throw new cce.UnreachableException();

+    }

+

+    public AI.IFunApp IsExactlyA(AI.IExpr e, AI.IExpr type) {

+      //PM: We need this assume because Boogie does not yet allow us to use the

+      //PM: inherited precondition "requires IsTypeConstant(type)".

+      //PM: Note that that precondition is currently commented out.

+      Contract.Requires(e != null);

+      Contract.Requires(type != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      Contract.Assume(type is Constant);

+      Constant theType = (Constant)type;

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

+      Expr typeofExpr = new NAryExpr(Token.NoToken,

+          new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

+                           )),

+          new ExprSeq(IExpr2Expr(e)));

+      return Expr.Eq(typeofExpr, Expr.Ident(theType));

+    }

+

+    public AI.IFunApp IsA(AI.IExpr e, AI.IExpr type) {

+      //PM: We need this assume because Boogie does not yet allow us to use the

+      //PM: inherited precondition "requires IsTypeConstant(type)".

+      //PM: Note that that precondition is currently commented out.

+      Contract.Requires(e != null);

+      Contract.Requires(type != null);

+      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

+

+      Contract.Assume(type is Constant);

+      Contract.Assert(false);

+      throw new cce.UnreachableException();

+      Expr typeofExpr = new NAryExpr(Token.NoToken,

+          new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

+                           )),

+          new ExprSeq(IExpr2Expr(e)));

+      return new NAryExpr(Token.NoToken,

+          new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Subtype),

+          new ExprSeq(typeofExpr, IExpr2Expr(e)));

     }

+  }

 }

diff --git a/Source/AbsInt/ExprFactories.ssc b/Source/AbsInt/ExprFactories.ssc
deleted file mode 100644
index ad090f2b..00000000
--- a/Source/AbsInt/ExprFactories.ssc
+++ /dev/null
@@ -1,231 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using Microsoft.Boogie;

-using AI = Microsoft.AbstractInterpretationFramework;

-using Microsoft.Contracts;

-using Microsoft.Basetypes;

-

-namespace Microsoft.Boogie.AbstractInterpretation {

-

-    public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory

-    {

-        public AI.IFunApp! False {

-            get {

-

-                return Expr.False;

-            }

-        }

-        public AI.IFunApp! True {

-            get {

-                return Expr.True;

-            }

-        }

-

-        public AI.IFunApp! Not(AI.IExpr! p) {

-            return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p));

-        }

-

-        public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Or(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Implies(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q));

-        }

-        

-        public AI.IFunApp! Exists(AI.IFunction! p) {

-            return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

-        }

-        public AI.IFunApp! Exists(AI.AIType paramType, AI.FunctionBody! bodygen) {

-            // generate a fresh new variable

-            Variable! var = FreshBoundVariable(paramType);

-            Expr! expr = IExpr2Expr(bodygen(var));

-            return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

-        }

-        

-        public AI.IFunApp! Forall(AI.IFunction! p) {

-            return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;

-        }

-        public AI.IFunApp! Forall(AI.AIType paramType, AI.FunctionBody! bodygen) {

-            // generate a fresh new variable

-            Variable! var = FreshBoundVariable(paramType);

-            Expr! expr = IExpr2Expr(bodygen(var));

-            return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;

-        }

-        

-        private static int freshVarNum = 0;

-        private static Variable! FreshBoundVariable(AI.AIType paramType)

-        {

-          // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type

-          // to make this new variable?  For now, we use Type.Any.

-          Type! t = Type.Int;

-        /*

-          if (paramType is AI.Ref)

-            t = Type.Ref;

-          else if (paramType is AI.FieldName)

-            t = Type.Name;

-          else

-            System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */

-          assert false;

-          TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);

-          freshVarNum++;

-          return new BoundVariable(Token.NoToken, id);

-        }

-    }

-    

-    public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory

-    {

-        public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-    }

-    

-    public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory

-    {

-        public AI.IFunApp! Eq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-

-        public AI.IFunApp! Neq(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-

-        public AI.IFunApp! Null {

-            get {

-                assert false;       // don't know where to get null from

-            }

-        }

-    }

-

-    public class BoogieIntFactory : BoogieValueFactory, AI.IIntExprFactory {

-        public AI.IFunApp! Const(BigNum i) {

-            return new LiteralExpr(Token.NoToken, i);

-        }

-    }

-    

-    public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory {

-        public AI.IFunApp! AtMost(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IFunApp! Add(AI.IExpr! e0, AI.IExpr! e1) {

-            return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1));

-        }

-        public AI.IExpr! Term(Rational r, AI.IVariable var) {

-            if (var != null && r == Rational.ONE) {

-                return var;

-            } else {

-                Expr! product;

-                if (r.IsIntegral) {

-                    product = Expr.Literal(r.AsBigNum);

-                } else {

-                    product = Expr.Div(Expr.Literal(r.Numerator), Expr.Literal(r.Denominator));

-                }

-                if (var != null) {

-                    product = Expr.Mul(product, IExpr2Expr(var));

-                }

-                return product.IExpr;

-            }

-        }

-

-        public AI.IFunApp! False {

-            get {

-                return Expr.False;

-            }

-        }

-        public AI.IFunApp! True {

-            get {

-                return Expr.True;

-            }

-        }

-        public AI.IFunApp! And(AI.IExpr! p, AI.IExpr! q) {

-            return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q));

-        }

-    }

-

-    public class BoogieTypeFactory : BoogieFactory, AI.ITypeExprFactory {

-        /// <summary>

-        /// Returns an expression denoting the top of the type hierarchy.

-        /// </summary>

-        public AI.IExpr! RootType {

-            get {

-                assert false;  // BUGBUG: TODO

-                throw new System.NotImplementedException();

-            }

-        }

-

-        /// <summary>

-        /// Returns true iff "t" denotes a type constant.

-        /// </summary>

-        [Pure]

-        public bool IsTypeConstant(AI.IExpr! t) 

-          ensures result == (t is Constant);  

-        {

-            return t is Constant;

-        }

-

-        /// <summary>

-        /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.

-        /// </summary>

-        [Pure]

-        public bool IsTypeEqual(AI.IExpr! t0, AI.IExpr! t1) {

-            Constant c0 = t0 as Constant;

-            Constant c1 = t1 as Constant;

-            return c0 != null && c1 != null && c0 == c1;

-        }

-

-        /// <summary>

-        /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.

-        /// </summary>

-        [Pure]

-        public bool IsSubType(AI.IExpr! t0, AI.IExpr! t1) {

-            assert false;  // BUGBUG: TODO

-        }

-

-        /// <summary>

-        /// Returns the most derived supertype of both "t0" and "t1".  A precondition is

-        /// that "t0" and "t1" both represent types.

-        /// </summary>

-        public AI.IExpr! JoinTypes(AI.IExpr! t0, AI.IExpr! t1) {

-            assert false;  // BUGBUG: TODO

-        }

-

-        public AI.IFunApp! IsExactlyA(AI.IExpr! e, AI.IExpr! type) {

-            //PM: We need this assume because Boogie does not yet allow us to use the

-            //PM: inherited precondition "requires IsTypeConstant(type)".

-            //PM: Note that that precondition is currently commented out.

-            assume type is Constant;

-            Constant theType = (Constant)type;

-            assert false;

-            Expr typeofExpr = new NAryExpr(Token.NoToken,

-                new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

-                                 )),

-                new ExprSeq(IExpr2Expr(e)));

-            return Expr.Eq(typeofExpr, Expr.Ident(theType));

-        }

-

-        public AI.IFunApp! IsA(AI.IExpr! e, AI.IExpr! type) {

-            //PM: We need this assume because Boogie does not yet allow us to use the

-            //PM: inherited precondition "requires IsTypeConstant(type)".

-            //PM: Note that that precondition is currently commented out.

-            assume type is Constant;

-            assert false;

-            Expr typeofExpr = new NAryExpr(Token.NoToken,

-                new FunctionCall(new IdentifierExpr(Token.NoToken, "$typeof", Type.Int // Name

-                                 )),

-                new ExprSeq(IExpr2Expr(e)));

-            return new NAryExpr(Token.NoToken,

-                new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Subtype),

-                new ExprSeq(typeofExpr, IExpr2Expr(e)));

-        }

-    }

-}

diff --git a/Source/AbsInt/InterimKey.snk b/Source/AbsInt/InterimKey.snk
new file mode 100644
index 00000000..8fc79508
--- /dev/null
+++ b/Source/AbsInt/InterimKey.snk
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs
index 1ebd11b2..49958289 100644
--- a/Source/AbsInt/LoopInvariantsOnDemand.cs
+++ b/Source/AbsInt/LoopInvariantsOnDemand.cs
@@ -3,76 +3,80 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-namespace Microsoft.Boogie.AbstractInterpretation

-{

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using Microsoft.Contracts;

-using AI = Microsoft.AbstractInterpretationFramework;

-using Boogie = Microsoft.Boogie;

+namespace Microsoft.Boogie.AbstractInterpretation {

+  using System;

+  using System.Collections;

+  using System.Collections.Generic;

+  using System.Diagnostics.Contracts;

+  using AI = Microsoft.AbstractInterpretationFramework;

+  using Boogie = Microsoft.Boogie;

+

+

+

   /// <summary>

   /// A visitor of an abstract interpretation expression that collects the free variables 

   /// </summary>      

-  class FreeVariablesVisitor : AI.ExprVisitor 

-  {

-    [Peer] List<AI.IVariable!>! variables;

-    public List<AI.IVariable!>! FreeVariables 

-    {

-      get

-      {

+  class FreeVariablesVisitor : AI.ExprVisitor {

+    [Peer]

+    List<AI.IVariable> variables;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(cce.NonNullElements(variables));

+      Contract.Invariant(cce.NonNullElements(varNames));

+    }

+

+    public List<AI.IVariable> FreeVariables {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<AI.IVariable>>()));

+

         return this.variables;

-      }    

+      }

     }

 

-    List<string!>! varNames;    // used to check the consinstency!

+    List<string> varNames;    // used to check the consinstency!

 

-    public FreeVariablesVisitor() 

-    {

-      this.variables = new List<AI.IVariable!>(); 

-      this.varNames = new List<string!>();

+    public FreeVariablesVisitor() {

+      this.variables = new List<AI.IVariable>();

+      this.varNames = new List<string>();

     }

 

-    override public object Default(AI.IExpr! expr)

-    {

-      if (expr is AI.IVariable) 

-      {

-        if(!variables.Contains((AI.IVariable) expr)) 

-        {

-          this.variables.Add((AI.IVariable) expr);

-                      

-          assert ! this.varNames.Contains(expr.ToString());     // If we get there, we have an error: two variables with the same name but different identity  

-             

+    override public object Default(AI.IExpr expr) {

+      Contract.Requires(expr != null);

+      if (expr is AI.IVariable) {

+        if (!variables.Contains((AI.IVariable)expr)) {

+          this.variables.Add((AI.IVariable)expr);

+

+          Contract.Assert(!this.varNames.Contains(expr.ToString()));     // If we get there, we have an error: two variables with the same name but different identity  

+

           this.varNames.Add(expr.ToString());

         }

         return null;

-      }

-      else if (expr is AI.IFunApp)

-        return VisitFunApp((AI.IFunApp) expr);

+      } else if (expr is AI.IFunApp)

+        return VisitFunApp((AI.IFunApp)expr);

       else if (expr is AI.IFunction)

         return VisitFunction((AI.IFunction)expr);

-      else 

-      {

-        assert false;

+      else {

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

       }

     }

 

-    public override object VisitFunApp(AI.IFunApp! funapp)

-    {

-      foreach (AI.IExpr! arg in funapp.Arguments)

-      {

+    public override object VisitFunApp(AI.IFunApp funapp) {

+      Contract.Requires(funapp != null);

+      foreach (AI.IExpr arg in funapp.Arguments) {

+        Contract.Assert(arg != null);

         arg.DoVisit(this);

       }

       return true;

     }

-                

-    public override object VisitFunction(AI.IFunction! fun)

-    {

+

+    public override object VisitFunction(AI.IFunction fun) {

+      Contract.Requires(fun != null);

       fun.Body.DoVisit(this);

       this.variables.Remove(fun.Param);

       return true;

     }

 

-  } 

+  }

 

 }
\ No newline at end of file
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.ssc b/Source/AbsInt/LoopInvariantsOnDemand.ssc
deleted file mode 100644
index 1ebd11b2..00000000
--- a/Source/AbsInt/LoopInvariantsOnDemand.ssc
+++ /dev/null
@@ -1,78 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-namespace Microsoft.Boogie.AbstractInterpretation

-{

-using System;

-using System.Collections;

-using System.Collections.Generic;

-using Microsoft.Contracts;

-using AI = Microsoft.AbstractInterpretationFramework;

-using Boogie = Microsoft.Boogie;

-  /// <summary>

-  /// A visitor of an abstract interpretation expression that collects the free variables 

-  /// </summary>      

-  class FreeVariablesVisitor : AI.ExprVisitor 

-  {

-    [Peer] List<AI.IVariable!>! variables;

-    public List<AI.IVariable!>! FreeVariables 

-    {

-      get

-      {

-        return this.variables;

-      }    

-    }

-

-    List<string!>! varNames;    // used to check the consinstency!

-

-    public FreeVariablesVisitor() 

-    {

-      this.variables = new List<AI.IVariable!>(); 

-      this.varNames = new List<string!>();

-    }

-

-    override public object Default(AI.IExpr! expr)

-    {

-      if (expr is AI.IVariable) 

-      {

-        if(!variables.Contains((AI.IVariable) expr)) 

-        {

-          this.variables.Add((AI.IVariable) expr);

-                      

-          assert ! this.varNames.Contains(expr.ToString());     // If we get there, we have an error: two variables with the same name but different identity  

-             

-          this.varNames.Add(expr.ToString());

-        }

-        return null;

-      }

-      else if (expr is AI.IFunApp)

-        return VisitFunApp((AI.IFunApp) expr);

-      else if (expr is AI.IFunction)

-        return VisitFunction((AI.IFunction)expr);

-      else 

-      {

-        assert false;

-      }

-    }

-

-    public override object VisitFunApp(AI.IFunApp! funapp)

-    {

-      foreach (AI.IExpr! arg in funapp.Arguments)

-      {

-        arg.DoVisit(this);

-      }

-      return true;

-    }

-                

-    public override object VisitFunction(AI.IFunction! fun)

-    {

-      fun.Body.DoVisit(this);

-      this.variables.Remove(fun.Param);

-      return true;

-    }

-

-  } 

-

-}
\ No newline at end of file
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index 694811da..2890730b 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -3,12 +3,12 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-namespace Microsoft.Boogie

-{

+namespace Microsoft.Boogie {

   using System;

   using System.Collections.Generic;

-  using Microsoft.Contracts;

+  using System.Diagnostics.Contracts;

 

+  

   /// <summary>

   /// This class provides the functionality of traversing a program to determine which

   /// blocks are blocks where the widening operator may need to be applied.  Assumes

@@ -16,95 +16,82 @@ namespace Microsoft.Boogie
   /// the end.  Assumes the 'widenBlock' bits are initially false, and sets them

   /// appropriately.

   /// </summary>

-  public class WidenPoints 

-  {

+  public class WidenPoints {

     /// <summary>

     /// Compute the widen points of a program

     /// </summary>

-    public static void Compute(Program! program) 

-    {

-      expose (program)

-      {

-        foreach (Declaration m in program.TopLevelDeclarations) 

-        {

-          Implementation impl = m as Implementation;

-          if (impl != null) 

-          {

-            if (impl.Blocks != null && impl.Blocks.Count > 0) 

-            {

-              assume impl.IsConsistent;

-              expose (impl) {

-                Block start = impl.Blocks[0];

-                assume start != null;

-                assume start.IsConsistent;

-                Visit(start);

-          

-                // We reset the state...

-                foreach(Block b in impl.Blocks) {

-                  expose (b) {

-                    b.TraversingStatus = Block.VisitState.ToVisit;

-                  }

-                }

-              }

+    public static void Compute(Program program) {

+      Contract.Requires(program != null);

+      cce.BeginExpose(program);

+

+      foreach (Declaration m in program.TopLevelDeclarations) {

+        Implementation impl = m as Implementation;

+        if (impl != null) {

+          if (impl.Blocks != null && impl.Blocks.Count > 0) {

+            Contract.Assume(cce.IsConsistent(impl));

+            cce.BeginExpose(impl);

+            Block start = impl.Blocks[0];

+            Contract.Assume(start != null);

+            Contract.Assume(cce.IsConsistent(start));

+            Visit(start);

+

+            // We reset the state...

+            foreach (Block b in impl.Blocks) {

+              cce.BeginExpose(b);

+              b.TraversingStatus = Block.VisitState.ToVisit;

+              cce.EndExpose();

             }

+            cce.EndExpose();

           }

         }

       }

+      cce.EndExpose();

     }

 

-    static void Visit(Block! b) 

-    {

-      assume b.IsExposable;

-      if (b.TraversingStatus == Block.VisitState.BeingVisited) 

-      {

-        expose (b)

-        {

-          // we got here through a back-edge

-          b.widenBlock = true;

-        }

-      } 

-      else if(b.TraversingStatus == Block.VisitState.AlreadyVisited)

-      {

+    static void Visit(Block b) {

+      Contract.Requires(b != null);

+      Contract.Assume(cce.IsExposable(b));

+      if (b.TraversingStatus == Block.VisitState.BeingVisited) {

+        cce.BeginExpose(b);

+        // we got here through a back-edge

+        b.widenBlock = true;

+        cce.EndExpose();

+      } else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {

         // do nothing... we already saw this node

-      }

-      else if (b.TransferCmd is GotoCmd) 

-      {

-        assert b.TraversingStatus == Block.VisitState.ToVisit;    

-    

+      } else if (b.TransferCmd is GotoCmd) {

+        Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

+

         GotoCmd g = (GotoCmd)b.TransferCmd;

-        expose (b)

-        {

-          expose (g) {  //PM: required for the subsequent expose (g.labelTargets)

-            b.TraversingStatus = Block.VisitState.BeingVisited;

-           

-            // labelTargets is made non-null by Resolve, which we assume

-            // has already called in a prior pass.

-            assume g.labelTargets != null;

-            expose (g.labelTargets) {

-              foreach (Block succ in g.labelTargets) 

-//              invariant b.currentlyTraversed; 

-                //PM: The following loop invariant will work once properties are axiomatized

-                //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

+        cce.BeginExpose(b);

+

+        cce.BeginExpose(g);   //PM: required for the subsequent expose (g.labelTargets)

+        b.TraversingStatus = Block.VisitState.BeingVisited;

+

+        // labelTargets is made non-null by Resolve, which we assume

+        // has already called in a prior pass.

+        Contract.Assume(g.labelTargets != null);

+        cce.BeginExpose(g.labelTargets);

+        foreach (Block succ in g.labelTargets)

+        //              invariant b.currentlyTraversed; 

+        //PM: The following loop invariant will work once properties are axiomatized

+        //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

               {

-                assert succ != null;

-                Visit(succ);

-              }

-            }

+          Contract.Assert(succ != null);

+          Visit(succ);

+        }

+        cce.EndExpose();

 

-            assert b.TraversingStatus == Block.VisitState.BeingVisited;

-//            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

+        Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);

+        //            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

 

-            b.TraversingStatus = Block.VisitState.AlreadyVisited;

+        b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

-            //PM: The folowing assumption is needed because we cannot prove that a simple field update

-            //PM: leaves the value of a property unchanged.

-            assume (g.labelNames != null ==> g.labelNames.Length == g.labelTargets.Length);

-          }

-        }

-      }

-      else 

-      {

-        assert b.TransferCmd == null || b.TransferCmd is ReturnCmd;        // It must be a returnCmd;

+        //PM: The folowing assumption is needed because we cannot prove that a simple field update

+        //PM: leaves the value of a property unchanged.

+        Contract.Assume(g.labelNames == null || g.labelNames.Length == g.labelTargets.Length);

+        cce.EndExpose();

+      } else {

+        Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd);        // It must be a returnCmd;

       }

     }

 

@@ -115,21 +102,23 @@ namespace Microsoft.Boogie
     /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>

     /// <return> The blocks that are in the loop from block </return>

     /// </summary>

-    public static List<Block!> ComputeLoopBodyFrom(Block! block)

-      requires block.widenBlock;

-    {

-      assert rootBlock == null;

+    public static List<Block> ComputeLoopBodyFrom(Block block) {

+      Contract.Requires(block.widenBlock);

+      Contract.Requires(block != null);

+      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

+

+      Contract.Assert(rootBlock == null);

       rootBlock = block;

 

-      List<Block!> blocksInLoop = new List<Block!>();         // We use a list just because .net does not define a set      

-      List<Block!> visitingPath = new List<Block!>();         // The order is important, as we want paths

-             

-      blocksInLoop.Add(block);      

-              

+      List<Block/*!*/> blocksInLoop = new List<Block/*!*/>();         // We use a list just because .net does not define a set

+      List<Block/*!*/> visitingPath = new List<Block/*!*/>();         // The order is important, as we want paths

+

+      blocksInLoop.Add(block);

+

       DoDFSVisit(block, visitingPath, blocksInLoop);

-      

+

       visitingPath.Add(block);

-      

+

 

       rootBlock = null;   // We reset the invariant

 

@@ -141,42 +130,43 @@ namespace Microsoft.Boogie
     /// <param name = "block"> The block to visit </param>

     /// <param name = "path"> The path we are visiting so far </param>

     /// </summary>

-    private static void DoDFSVisit(Block! block, List<Block!>! path, List<Block!>! blocksInPath)

-    {

-        #region case 1. We visit the root => We are done, "path" is a path inside the loop

-        if(block == rootBlock && path.Count > 1)

-        {

-          blocksInPath.AddRange(path);      // Add all the blocks in this path 

-        }

+    private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath) {

+      Contract.Requires(block != null);

+      Contract.Requires(cce.NonNullElements(path));

+      Contract.Requires(cce.NonNullElements(path));

+      #region case 1. We visit the root => We are done, "path" is a path inside the loop

+      if (block == rootBlock && path.Count > 1) {

+        blocksInPath.AddRange(path);      // Add all the blocks in this path 

+      }

 

-        #endregion

-        #region case 2. We visit a node that ends with a return => "path" is not inside the loop

-        if(block.TransferCmd is ReturnCmd)

-        {

-          return;

-        }

-        #endregion

-        #region case 3. We visit a node with successors => continue the exploration of its successors

-        {

-          assert block.TransferCmd is GotoCmd;

-          GotoCmd! successors = (GotoCmd) block.TransferCmd;

-          

-          if (successors.labelTargets != null)

-          foreach (Block! nextBlock in successors.labelTargets)

-          {

-            if(path.Contains(nextBlock))      // If the current path has already seen the block, just skip it 

+      #endregion

+      #region case 2. We visit a node that ends with a return => "path" is not inside the loop

+      if (block.TransferCmd is ReturnCmd) {

+        return;

+      }

+      #endregion

+      #region case 3. We visit a node with successors => continue the exploration of its successors

+      {

+        Contract.Assert(block.TransferCmd is GotoCmd);

+        GotoCmd successors = (GotoCmd)block.TransferCmd;

+        Contract.Assert(successors != null);

+

+        if (successors.labelTargets != null)

+          foreach (Block nextBlock in successors.labelTargets) {

+            Contract.Assert(nextBlock != null);

+            if (path.Contains(nextBlock))      // If the current path has already seen the block, just skip it 

               continue;

-                                              // Otherwise we perform the DFS visit

+            // Otherwise we perform the DFS visit

             path.Add(nextBlock);

             DoDFSVisit(nextBlock, path, blocksInPath);

-            

-            assert nextBlock == path[path.Count-1];

-            path.RemoveAt(path.Count-1);

+

+            Contract.Assert(nextBlock == path[path.Count - 1]);

+            path.RemoveAt(path.Count - 1);

           }

 

-        }

+      }

 

-        #endregion

-    }      

- }   

+      #endregion

+    }

+  }

 }

diff --git a/Source/AbsInt/Traverse.ssc b/Source/AbsInt/Traverse.ssc
deleted file mode 100644
index 694811da..00000000
--- a/Source/AbsInt/Traverse.ssc
+++ /dev/null
@@ -1,182 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-namespace Microsoft.Boogie

-{

-  using System;

-  using System.Collections.Generic;

-  using Microsoft.Contracts;

-

-  /// <summary>

-  /// This class provides the functionality of traversing a program to determine which

-  /// blocks are blocks where the widening operator may need to be applied.  Assumes

-  /// all 'currentlyTraversed' bits to be initially false, and leaves them that way in

-  /// the end.  Assumes the 'widenBlock' bits are initially false, and sets them

-  /// appropriately.

-  /// </summary>

-  public class WidenPoints 

-  {

-    /// <summary>

-    /// Compute the widen points of a program

-    /// </summary>

-    public static void Compute(Program! program) 

-    {

-      expose (program)

-      {

-        foreach (Declaration m in program.TopLevelDeclarations) 

-        {

-          Implementation impl = m as Implementation;

-          if (impl != null) 

-          {

-            if (impl.Blocks != null && impl.Blocks.Count > 0) 

-            {

-              assume impl.IsConsistent;

-              expose (impl) {

-                Block start = impl.Blocks[0];

-                assume start != null;

-                assume start.IsConsistent;

-                Visit(start);

-          

-                // We reset the state...

-                foreach(Block b in impl.Blocks) {

-                  expose (b) {

-                    b.TraversingStatus = Block.VisitState.ToVisit;

-                  }

-                }

-              }

-            }

-          }

-        }

-      }

-    }

-

-    static void Visit(Block! b) 

-    {

-      assume b.IsExposable;

-      if (b.TraversingStatus == Block.VisitState.BeingVisited) 

-      {

-        expose (b)

-        {

-          // we got here through a back-edge

-          b.widenBlock = true;

-        }

-      } 

-      else if(b.TraversingStatus == Block.VisitState.AlreadyVisited)

-      {

-        // do nothing... we already saw this node

-      }

-      else if (b.TransferCmd is GotoCmd) 

-      {

-        assert b.TraversingStatus == Block.VisitState.ToVisit;    

-    

-        GotoCmd g = (GotoCmd)b.TransferCmd;

-        expose (b)

-        {

-          expose (g) {  //PM: required for the subsequent expose (g.labelTargets)

-            b.TraversingStatus = Block.VisitState.BeingVisited;

-           

-            // labelTargets is made non-null by Resolve, which we assume

-            // has already called in a prior pass.

-            assume g.labelTargets != null;

-            expose (g.labelTargets) {

-              foreach (Block succ in g.labelTargets) 

-//              invariant b.currentlyTraversed; 

-                //PM: The following loop invariant will work once properties are axiomatized

-                //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);

-              {

-                assert succ != null;

-                Visit(succ);

-              }

-            }

-

-            assert b.TraversingStatus == Block.VisitState.BeingVisited;

-//            System.Diagnostics.Debug.Assert(b.currentlyTraversed);

-

-            b.TraversingStatus = Block.VisitState.AlreadyVisited;

-

-            //PM: The folowing assumption is needed because we cannot prove that a simple field update

-            //PM: leaves the value of a property unchanged.

-            assume (g.labelNames != null ==> g.labelNames.Length == g.labelTargets.Length);

-          }

-        }

-      }

-      else 

-      {

-        assert b.TransferCmd == null || b.TransferCmd is ReturnCmd;        // It must be a returnCmd;

-      }

-    }

-

-    static private Block rootBlock = null;         // The root point we have to consider

-

-    /// <summary>

-    /// Compute the blocks in the body loop. 

-    /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>

-    /// <return> The blocks that are in the loop from block </return>

-    /// </summary>

-    public static List<Block!> ComputeLoopBodyFrom(Block! block)

-      requires block.widenBlock;

-    {

-      assert rootBlock == null;

-      rootBlock = block;

-

-      List<Block!> blocksInLoop = new List<Block!>();         // We use a list just because .net does not define a set      

-      List<Block!> visitingPath = new List<Block!>();         // The order is important, as we want paths

-             

-      blocksInLoop.Add(block);      

-              

-      DoDFSVisit(block, visitingPath, blocksInLoop);

-      

-      visitingPath.Add(block);

-      

-

-      rootBlock = null;   // We reset the invariant

-

-      return blocksInLoop;

-    }

-

-    /// <summary>

-    /// Perform the Depth-first search of the so to find the loop

-    /// <param name = "block"> The block to visit </param>

-    /// <param name = "path"> The path we are visiting so far </param>

-    /// </summary>

-    private static void DoDFSVisit(Block! block, List<Block!>! path, List<Block!>! blocksInPath)

-    {

-        #region case 1. We visit the root => We are done, "path" is a path inside the loop

-        if(block == rootBlock && path.Count > 1)

-        {

-          blocksInPath.AddRange(path);      // Add all the blocks in this path 

-        }

-

-        #endregion

-        #region case 2. We visit a node that ends with a return => "path" is not inside the loop

-        if(block.TransferCmd is ReturnCmd)

-        {

-          return;

-        }

-        #endregion

-        #region case 3. We visit a node with successors => continue the exploration of its successors

-        {

-          assert block.TransferCmd is GotoCmd;

-          GotoCmd! successors = (GotoCmd) block.TransferCmd;

-          

-          if (successors.labelTargets != null)

-          foreach (Block! nextBlock in successors.labelTargets)

-          {

-            if(path.Contains(nextBlock))      // If the current path has already seen the block, just skip it 

-              continue;

-                                              // Otherwise we perform the DFS visit

-            path.Add(nextBlock);

-            DoDFSVisit(nextBlock, path, blocksInPath);

-            

-            assert nextBlock == path[path.Count-1];

-            path.RemoveAt(path.Count-1);

-          }

-

-        }

-

-        #endregion

-    }      

- }   

-}

diff --git a/Source/AbsInt/cce.cs b/Source/AbsInt/cce.cs
new file mode 100644
index 00000000..c8d7a4ab
--- /dev/null
+++ b/Source/AbsInt/cce.cs
@@ -0,0 +1,62 @@
+using System;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Text;

+using Microsoft.Boogie;

+

+  /// <summary>

+    /// A class containing static methods to extend the functionality of Code Contracts

+    /// </summary>

+

+public static class cce {

+  [Pure]

+  public static T NonNull<T>(T t) {

+    Contract.Assert(t != null);

+    return t;

+  }

+  [Pure]

+  public static bool NonNullElements<T>(IEnumerable<T> collection) {

+    return collection != null && Contract.ForAll(collection, c => c != null);

+  }

+  [Pure]

+  public static bool NonNullElements(VariableSeq collection) {

+    return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

+  }

+

+  public class UnreachableException : Exception {

+    public UnreachableException() {

+    }

+  }

+

+  [Pure]

+  public static void BeginExpose(object o) {

+  }

+  [Pure]

+  public static void EndExpose() {

+  }

+

+  public static bool IsPeerConsistent(this object o) {

+    return true;

+  }

+

+  public static bool IsConsistent(this object o) {

+    return true;

+  }

+

+  public static bool IsExposable(this object o) {

+    return true;

+  }

+  public static class Owner {

+    [Pure]

+    public static bool Same(object o, object p) {

+      return true;

+    }

+  }

+}

+

+public class PeerAttribute : System.Attribute {

+}

+public class RepAttribute : System.Attribute {

+}

+public class CapturedAttribute : System.Attribute {

+}
\ No newline at end of file
diff --git a/Source/AbsInt/version.cs b/Source/AbsInt/version.cs
new file mode 100644
index 00000000..2804c330
--- /dev/null
+++ b/Source/AbsInt/version.cs
@@ -0,0 +1,8 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System.Reflection;

+[assembly: AssemblyVersion("2.0.0.0")]

+[assembly: AssemblyFileVersion("2.0.0.0")]