fixed bug in the inlineDepth option for houdini

small clean up in the inlining implementation

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) {