Get rid of some CCI dependencies in Driver

4 files changed, 4 insertions, 108 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index b4798299..33b9146c 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -19,7 +19,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics.Contracts;

   using System.Diagnostics;

   using VC;

-  using Cci = System.Compiler;

   using AI = Microsoft.AbstractInterpretationFramework;

   using BoogiePL = Microsoft.Boogie;

 

@@ -64,19 +63,8 @@ namespace Microsoft.Boogie {
         Console.WriteLine("--------------------");

       }

 

-      SelectPlatform(CommandLineOptions.Clo);

-

       Helpers.ExtraTraceInformation("Becoming sentient");

 

-      // Make sure the Spec# runtime is initialized.

-      // This happens when the static constructor for the Runtime type is executed.

-      // Otherwise, if a reference happens to get chased to it, it is loaded twice

-      // and then the types in it do not get unique representations.

-      if (System.Type.GetType("Mono.Runtime") == null) {  // MONO

-        Cci.AssemblyNode a = Microsoft.SpecSharp.Runtime.RuntimeAssembly;

-        Contract.Assert(a != null);

-      }

-

       foreach (string file in CommandLineOptions.Clo.Files) {

         Contract.Assert(file != null);

         string extension = Path.GetExtension(file);

@@ -144,57 +132,6 @@ namespace Microsoft.Boogie {
       Console.ForegroundColor = col;

     }

 

-    public static void SelectPlatform(CommandLineOptions options) {

-      Contract.Requires(options != null);

-      if (options.TargetPlatformLocation != null) {

-        // Make sure static constructor runs before we start setting locations, etc.

-        System.Compiler.SystemTypes.Clear();

-

-        switch (options.TargetPlatform) {

-          case CommandLineOptions.PlatformType.v1:

-            Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation);

-            break;

-          case CommandLineOptions.PlatformType.v11:

-            Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation);

-            break;

-          case CommandLineOptions.PlatformType.v2:

-            Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation);

-            break;

-          case CommandLineOptions.PlatformType.cli1:

-            Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation);

-            break;

-        }

-

-        if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0) {

-          System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation;

-        }

-        System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll";

-

-        System.Compiler.SystemTypes.Initialize(true, true);

-      }

-    }

-

-    static string GetErrorLine(Cci.ErrorNode node) {

-      Contract.Requires(node != null);

-      Contract.Requires(node.SourceContext.Document == null || (node.SourceContext.Document.Name != null));

-      

-      Contract.Ensures(Contract.Result<string>() != null);

-      string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture);

-      string kind;

-      if (message.Contains("(trace position)")) {

-        kind = "Related information";

-      } else {

-        kind = "Error";

-      }

-      if (node.SourceContext.Document != null) {

-        return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(cce.NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message);

-      } else {

-        return string.Format("{0}: {1}", kind, message);

-      }

-

-

-    }

-

     enum FileType {

       Unknown,

       Cil,

@@ -202,26 +139,6 @@ namespace Microsoft.Boogie {
       Dafny

     };

 

-    class ErrorReporter {

-      public Cci.ErrorNodeList errors = new Cci.ErrorNodeList();

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(errors != null);

-      }

-

-      public int errorsReported;

-

-      public void ReportErrors() {

-        //sort the portion of the array that will be reported to make output more deterministic

-        errors.Sort(errorsReported, errors.Count - errorsReported);

-        for (; errorsReported < errors.Count; errorsReported++) {

-          Cci.ErrorNode error = errors[errorsReported];

-          if (error != null)

-            ErrorWriteLine(GetErrorLine(error));

-        }

-      }

-    }

-

     static void ProcessFiles(List<string> fileNames) {

       Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {

@@ -242,7 +159,7 @@ namespace Microsoft.Boogie {
         //BoogiePL.Errors.count = 0;

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

-        oc = InferAndVerify(program, null, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+        oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

         switch (oc) {

           case PipelineOutcome.Done:

           case PipelineOutcome.VerificationCompleted:

@@ -513,7 +430,6 @@ namespace Microsoft.Boogie {
     ///    parameters contain meaningful values

     /// </summary>

     static PipelineOutcome InferAndVerify(Program program,

-                                           ErrorReporter errorReporter,

                                            out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {

       Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

@@ -649,13 +565,8 @@ namespace Microsoft.Boogie {
                 errorCount++;

               } //else {

               Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

-              if (errorReporter != null) {

-                //                assert translatedProgram != null;

-                //                ErrorReporting h = new ErrorReporting();

-                //                h.errorReportingWithTrace(translatedProgram, errors, impl);

 

-                errorReporter.ReportErrors();

-              } else {

+              {

                 // BP1xxx: Parsing errors

                 // BP2xxx: Name resolution errors

                 // BP3xxx: Typechecking errors

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 9d288d6f..635f3bfe 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -99,23 +99,7 @@
   </PropertyGroup>

   <ItemGroup>

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

-    <Reference Include="Microsoft.SpecSharp, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.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.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

   </ItemGroup>

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 4eafdbbb..694ddc00 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -4,6 +4,7 @@ using Graphing;
 using PureCollections;

 using System.Diagnostics.Contracts;

 

+

 namespace Microsoft.Boogie {

   public class UnusedVarEliminator : VariableCollector {

     public static void Eliminate(Program program) {

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 85e0c963..445c2cfb 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -594,7 +594,7 @@ namespace Microsoft.Boogie {
       : base(s) {

     }

   }

-  public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException {

+  public class UnexpectedProverOutputException : ProverException {

     public UnexpectedProverOutputException(string s)

       : base(s) {

     }