diff options
Diffstat (limited to 'Source/Houdini/Houdini.cs')
-rw-r--r-- | Source/Houdini/Houdini.cs | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 2c202022..ed3d1afc 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -261,6 +261,7 @@ namespace Microsoft.Boogie.Houdini { this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
this.houdiniConstants = CollectExistentialConstants();
+ Inline();
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
@@ -277,6 +278,22 @@ namespace Microsoft.Boogie.Houdini { this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
+ private void Inline() {
+ if (CommandLineOptions.Clo.InlineDepth < 0)
+ return;
+ foreach (Implementation impl in callGraph.Nodes) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ foreach (Implementation impl in callGraph.Nodes) {
+ Inliner.ProcessImplementationForHoudini(program, impl);
+ }
+ foreach (Implementation impl in callGraph.Nodes) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
foreach (Declaration decl in program.TopLevelDeclarations) {
|