From df1cd695daffb01a590a7310dbee1b6594de2ecd Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 23 Nov 2011 11:26:34 -0800
Subject: fixed bug in the inlineDepth option for houdini small clean up in the
 inlining implementation

---
 Source/Houdini/Houdini.cs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'Source/Houdini')

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) {
-- 
cgit v1.2.3