Did some refactoring of the Dafny drivers.

1 files changed, 52 insertions, 38 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 9e93eb1e..98d44b72 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -21,6 +21,7 @@ namespace DafnyLanguage
     readonly string _programText;

     readonly string _filename;

     Dafny.Program _program;

+

     List<DafnyError> _errors = new List<DafnyError>();

     public List<DafnyError> Errors { get { return _errors; } }

 

@@ -219,48 +220,86 @@ namespace DafnyLanguage
       return oc;

     }

 

-    static void EliminateDeadVariablesAndInline(Bpl.Program program) {

+    /// <summary>

+    /// Resolves and type checks the given Boogie program.

+    /// Returns:

+    ///  - Done if no errors occurred, and command line specified no resolution or no type checking.

+    ///  - ResolutionError if a resolution error occurred

+    ///  - TypeCheckingError if a type checking error occurred

+    ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

+    /// </summary>

+    static PipelineOutcome BoogieResolveAndTypecheck(Bpl.Program program) {

+      Contract.Requires(program != null);

+      // ---------- Resolve ------------------------------------------------------------

+      int errorCount = program.Resolve();

+      if (errorCount != 0) {

+        return PipelineOutcome.ResolutionError;

+      }

+

+      // ---------- Type check ------------------------------------------------------------

+      errorCount = program.Typecheck();

+      if (errorCount != 0) {

+        return PipelineOutcome.TypeCheckingError;

+      }

+

+      return PipelineOutcome.ResolvedAndTypeChecked;

+    }

+

+    static void EliminateDeadVariablesAndInline(Bpl.Program program)

+    {

       Contract.Requires(program != null);

       // Eliminate dead variables

       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

 

       // Collect mod sets

-      if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis) {

+      if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis)

+      {

         Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

       }

 

       // Coalesce blocks

-      if (Bpl.CommandLineOptions.Clo.CoalesceBlocks) {

+      if (Bpl.CommandLineOptions.Clo.CoalesceBlocks)

+      {

         Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

       }

 

       // Inline

       var TopLevelDeclarations = program.TopLevelDeclarations;

 

-      if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None) {

+      if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None)

+      {

         bool inline = false;

-        foreach (var d in TopLevelDeclarations) {

-          if (d.FindExprAttribute("inline") != null) {

+        foreach (var d in TopLevelDeclarations)

+        {

+          if (d.FindExprAttribute("inline") != null)

+          {

             inline = true;

           }

         }

-        if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0) {

-          foreach (var d in TopLevelDeclarations) {

+        if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0)

+        {

+          foreach (var d in TopLevelDeclarations)

+          {

             var impl = d as Bpl.Implementation;

-            if (impl != null) {

+            if (impl != null)

+            {

               impl.OriginalBlocks = impl.Blocks;

               impl.OriginalLocVars = impl.LocVars;

             }

           }

-          foreach (var d in TopLevelDeclarations) {

+          foreach (var d in TopLevelDeclarations)

+          {

             var impl = d as Bpl.Implementation;

-            if (impl != null && !impl.SkipVerification) {

+            if (impl != null && !impl.SkipVerification)

+            {

               Bpl.Inliner.ProcessImplementation(program, impl);

             }

           }

-          foreach (var d in TopLevelDeclarations) {

+          foreach (var d in TopLevelDeclarations)

+          {

             var impl = d as Bpl.Implementation;

-            if (impl != null) {

+            if (impl != null)

+            {

               impl.OriginalBlocks = null;

               impl.OriginalLocVars = null;

             }

@@ -270,31 +309,6 @@ namespace DafnyLanguage
     }

 

     /// <summary>

-    /// Resolves and type checks the given Boogie program.

-    /// Returns:

-    ///  - Done if no errors occurred, and command line specified no resolution or no type checking.

-    ///  - ResolutionError if a resolution error occurred

-    ///  - TypeCheckingError if a type checking error occurred

-    ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

-    /// </summary>

-    static PipelineOutcome BoogieResolveAndTypecheck(Bpl.Program program) {

-      Contract.Requires(program != null);

-      // ---------- Resolve ------------------------------------------------------------

-      int errorCount = program.Resolve();

-      if (errorCount != 0) {

-        return PipelineOutcome.ResolutionError;

-      }

-

-      // ---------- Type check ------------------------------------------------------------

-      errorCount = program.Typecheck();

-      if (errorCount != 0) {

-        return PipelineOutcome.TypeCheckingError;

-      }

-

-      return PipelineOutcome.ResolvedAndTypeChecked;

-    }

-

-    /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

     ///  - Done if command line specified no verification