diff options
| author |  wuestholz <unknown> | 2013-06-03 17:46:40 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-03 17:46:40 -0700 |
| commit | ab50e74e3122f19916d9010a5fba88de78b1c4df (patch) | |
| tree | d1d3a70b76f31b428d600ff8a0380bc15647ef1a /Source/DafnyDriver | |
| parent | e2668d447fb277cd11e114579c1a27de185aaec0 (diff) | |
Did some refactoring of the Dafny drivers.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 67 |
1 files changed, 1 insertions, 66 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:
|