diff options
| author |  allydonaldson <unknown> | 2013-04-30 15:36:09 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-04-30 15:36:09 +0100 |
| commit | 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 (patch) | |
| tree | 4a22b414e8a17fa68a34279280142120fc1b203d /Source/BoogieDriver/BoogieDriver.cs | |
| parent | 98cab336f54799e105af45d06ec60e29cfca4fd5 (diff) | |
Staged Houdini
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -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 9d1038f5..4531b9bb 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) {
|