diff options
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 67 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 67 |
2 files changed, 3 insertions, 131 deletions
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:
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index ed28d4de..bf953c8e 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -211,7 +211,7 @@ namespace DafnyLanguage PipelineOutcome oc = BoogieResolveAndTypecheck(program);
if (oc == PipelineOutcome.ResolvedAndTypeChecked) {
- EliminateDeadVariablesAndInline(program);
+ ExecutionEngine.EliminateDeadVariablesAndInline(program);
return BoogieInferAndVerify(program, er);
}
return oc;
@@ -241,70 +241,7 @@ namespace DafnyLanguage 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)
- {
- Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
- }
-
- // Coalesce blocks
- if (Bpl.CommandLineOptions.Clo.CoalesceBlocks)
- {
- Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
- }
-
- // Inline
- var TopLevelDeclarations = program.TopLevelDeclarations;
-
- if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None)
- {
- bool inline = false;
- foreach (var d in TopLevelDeclarations)
- {
- if (d.FindExprAttribute("inline") != null)
- {
- inline = true;
- }
- }
- if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0)
- {
- foreach (var d in TopLevelDeclarations)
- {
- var impl = d as Bpl.Implementation;
- if (impl != null)
- {
- impl.OriginalBlocks = impl.Blocks;
- impl.OriginalLocVars = impl.LocVars;
- }
- }
- foreach (var d in TopLevelDeclarations)
- {
- var impl = d as Bpl.Implementation;
- if (impl != null && !impl.SkipVerification)
- {
- Bpl.Inliner.ProcessImplementation(program, impl);
- }
- }
- foreach (var d in TopLevelDeclarations)
- {
- var impl = d as Bpl.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:
|