From ab50e74e3122f19916d9010a5fba88de78b1c4df Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 3 Jun 2013 17:46:40 -0700
Subject: Did some refactoring of the Dafny drivers.

---
 Source/DafnyDriver/DafnyDriver.cs | 67 +--------------------------------------
 1 file changed, 1 insertion(+), 66 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 152e43bb..2891ec2b 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -184,7 +184,7 @@ namespace Microsoft.Dafny
           return oc;
 
         case PipelineOutcome.ResolvedAndTypeChecked:
-          EliminateDeadVariablesAndInline(program);
+          ExecutionEngine.EliminateDeadVariablesAndInline(program);
           return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
 
         default:
@@ -236,71 +236,6 @@ namespace Microsoft.Dafny
     }
 
 
-    // TODO(wuestholz): Use the definition in the Boogie driver.
-    static void EliminateDeadVariablesAndInline(Bpl.Program program)
-    {
-      Contract.Requires(program != null);
-      // Eliminate dead variables
-      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
-
-      // Collect mod sets
-      if (CommandLineOptions.Clo.DoModSetAnalysis)
-      {
-        Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
-      }
-
-      // Coalesce blocks
-      if (CommandLineOptions.Clo.CoalesceBlocks)
-      {
-        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
-      }
-
-      // Inline
-      var TopLevelDeclarations = program.TopLevelDeclarations;
-
-      if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None)
-      {
-        bool inline = false;
-        foreach (var d in TopLevelDeclarations)
-        {
-          if (d.FindExprAttribute("inline") != null)
-          {
-            inline = true;
-          }
-        }
-        if (inline && CommandLineOptions.Clo.StratifiedInlining == 0)
-        {
-          foreach (var d in TopLevelDeclarations)
-          {
-            var impl = d as Implementation;
-            if (impl != null)
-            {
-              impl.OriginalBlocks = impl.Blocks;
-              impl.OriginalLocVars = impl.LocVars;
-            }
-          }
-          foreach (var d in TopLevelDeclarations)
-          {
-            var impl = d as Implementation;
-            if (impl != null && !impl.SkipVerification)
-            {
-              Inliner.ProcessImplementation(program, impl);
-            }
-          }
-          foreach (var d in TopLevelDeclarations)
-          {
-            var impl = d as Implementation;
-            if (impl != null)
-            {
-              impl.OriginalBlocks = null;
-              impl.OriginalLocVars = null;
-            }
-          }
-        }
-      }
-    }
-
-
     /// <summary>
     /// Given a resolved and type checked Boogie program, infers invariants for the program
     /// and then attempts to verify it.  Returns:
-- 
cgit v1.2.3