diff options
| author |  wuestholz <unknown> | 2013-12-09 09:42:51 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-09 09:42:51 +0100 |
| commit | 8c029eac9244b10bf0bdf3451d91af74f0acc419 (patch) | |
| tree | d1b43bd96cfd2df2ad0f09718346c80b7e0168ca | |
| parent | 38c16e74324b992e8f35779373e9d4702669e5e3 (diff) | |
Expose certain program transformations in the execution engine to invoke them from Dafny.
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 45 |
1 files changed, 31 insertions, 14 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 0f188ec0..a53fa06f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -476,22 +476,11 @@ namespace Microsoft.Boogie }
}
- // Eliminate dead variables
- Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ EliminateDeadVariables(program);
- // Collect mod sets
- if (CommandLineOptions.Clo.DoModSetAnalysis)
- {
- Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
- }
+ CollectModSets(program);
- // Coalesce blocks
- if (CommandLineOptions.Clo.CoalesceBlocks)
- {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Coalescing blocks...");
- Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
- }
+ CoalesceBlocks(program);
if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
@@ -525,6 +514,32 @@ namespace Microsoft.Boogie }
+ public static void CoalesceBlocks(Program program)
+ {
+ if (CommandLineOptions.Clo.CoalesceBlocks)
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+ }
+
+
+ public static void CollectModSets(Program program)
+ {
+ if (CommandLineOptions.Clo.DoModSetAnalysis)
+ {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+ }
+
+
+ public static void EliminateDeadVariables(Program program)
+ {
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ }
+
+
public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true)
{
Contract.Requires(program != null);
@@ -687,6 +702,7 @@ namespace Microsoft.Boogie return PipelineOutcome.ResolvedAndTypeChecked;
}
+
public static void Inline(Program program)
{
Contract.Requires(program != null);
@@ -726,6 +742,7 @@ namespace Microsoft.Boogie }
}
+
/// <summary>
/// Given a resolved and type checked Boogie program, infers invariants for the program
/// and then attempts to verify it. Returns:
|