diff options
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 6a141fac..c12ba47d 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -195,11 +195,23 @@ namespace Microsoft.Boogie { PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);
CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
}
+
LinearSetTransform linearTransform = new LinearSetTransform(program);
linearTransform.Transform();
EliminateDeadVariablesAndInline(program);
+ if (CommandLineOptions.Clo.StagedHoudini > 0) {
+ var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);
+ candidateDependenceAnalyser.Analyse();
+ candidateDependenceAnalyser.ApplyStages();
+ if (CommandLineOptions.Clo.Trace) {
+ candidateDependenceAnalyser.dump();
+ }
+ PrintBplFile("staged.bpl", program, false, false);
+ Environment.Exit(0);
+ }
+
int errorCount, verified, inconclusives, timeOuts, outOfMemories;
oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
|