From bf65ebf6145df56f3198dbed788f6dd3058f3507 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 19 Sep 2014 15:55:19 -0700
Subject: a bug fix in Houdini (also AbsHoudini)

---
 Source/Houdini/AbstractHoudini.cs | 24 ----------------
 Source/Houdini/Houdini.cs         | 59 +--------------------------------------
 2 files changed, 1 insertion(+), 82 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 31b38e8a..d4466ca5 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -696,18 +696,6 @@ namespace Microsoft.Boogie.Houdini {
 
             var callGraph = BuildCallGraph();
 
-            foreach (Implementation impl in callGraph.Nodes)
-            {
-                InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
-                inlineRequiresVisitor.Visit(impl);
-            }
-
-            foreach (Implementation impl in callGraph.Nodes)
-            {
-                FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
-                freeRequiresVisitor.Visit(impl);
-            }
-
             foreach (Implementation impl in callGraph.Nodes)
             {
                 InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
@@ -2511,18 +2499,6 @@ namespace Microsoft.Boogie.Houdini {
 
             var callGraph = BuildCallGraph();
 
-            foreach (Implementation impl in callGraph.Nodes)
-            {
-                InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
-                inlineRequiresVisitor.Visit(impl);
-            }
-
-            foreach (Implementation impl in callGraph.Nodes)
-            {
-                FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
-                freeRequiresVisitor.Visit(impl);
-            }
-
             foreach (Implementation impl in callGraph.Nodes)
             {
                 InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 6bb2d4db..e91d0528 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -246,53 +246,6 @@ namespace Microsoft.Boogie.Houdini {
     }
   }
 
-  public class InlineRequiresVisitor : StandardVisitor {
-    public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
-      List<Cmd> newCmdSeq = new List<Cmd>();
-      for (int i = 0, n = cmdSeq.Count; i < n; i++) {
-        Cmd cmd = cmdSeq[i];
-        CallCmd callCmd = cmd as CallCmd;
-        if (callCmd != null) {
-          newCmdSeq.AddRange(InlineRequiresForCallCmd(callCmd));
-        }
-        else {
-          newCmdSeq.Add((Cmd)this.Visit(cmd));
-        }
-      }
-      return newCmdSeq;
-    }
-    private List<Cmd> InlineRequiresForCallCmd(CallCmd node) {
-      Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
-      for (int i = 0; i < node.Proc.InParams.Count; i++) {
-        substMap.Add(node.Proc.InParams[i], node.Ins[i]);
-      }
-      Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);
-      List<Cmd> cmds = new List<Cmd>();
-      foreach (Requires requires in node.Proc.Requires) {
-        if (requires.Free) continue;
-        Requires requiresCopy = new Requires(false, Substituter.Apply(substitution, requires.Condition));
-        cmds.Add(new AssertRequiresCmd(node, requiresCopy));
-      }
-      cmds.Add(node);
-      return cmds;
-    }
-  }
-
-  public class FreeRequiresVisitor : StandardVisitor {
-    public override Requires VisitRequires(Requires requires) {
-      if (requires.Free)
-        return base.VisitRequires(requires);
-      else 
-        return new Requires(true, requires.Condition);
-    }
-
-    public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
-      node.Requires = base.VisitRequires(node.Requires);
-      node.Expr = this.VisitExpr(node.Expr);
-      return node;
-    }
-  }
-
   public class InlineEnsuresVisitor : ReadOnlyVisitor {
       public override Ensures VisitEnsures(Ensures ensures)
       {
@@ -398,19 +351,9 @@ namespace Microsoft.Boogie.Houdini {
     }
 
     protected void Inline() {
-      if (CommandLineOptions.Clo.InlineDepth < 0)
+      if (CommandLineOptions.Clo.InlineDepth <= 0)
         return;
 
-      foreach (Implementation impl in callGraph.Nodes) {
-        InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
-        inlineRequiresVisitor.Visit(impl);
-      }
-
-      foreach (Implementation impl in callGraph.Nodes) {
-        FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
-        freeRequiresVisitor.Visit(impl);
-      }
-
       foreach (Implementation impl in callGraph.Nodes) {
         InlineEnsuresVisitor inlineEnsuresVisitor = new InlineEnsuresVisitor();
         inlineEnsuresVisitor.Visit(impl);
-- 
cgit v1.2.3