From 033f25a8791a36b74925033368fcea946a2290de Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Thu, 22 Jan 2015 09:19:28 +0000
Subject: Fixes to StagedHoudini

---
 Source/Core/InterProceduralReachabilityGraph.cs | 39 +++++++++++++++++--------
 1 file changed, 27 insertions(+), 12 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index b477e7de..d75a4b7d 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -12,8 +12,8 @@ namespace Microsoft.Boogie
   public interface IInterproceduralReachabilityGraph {
 
     bool MayReach(Block src, Block dst);
-    void dump();
 
+    void dump();
 
     Block GetNewEntryBlock(string p);
 
@@ -58,7 +58,15 @@ namespace Microsoft.Boogie
           }
         }
       }
-      
+
+      foreach(var n in nodes) {
+        // If there are disconnected nodes, put them into the
+        // graph as self-loops so that every node is represented in
+        // the graph
+        if(!reachabilityGraph.Nodes.Contains(n)) {
+          reachabilityGraph.AddEdge(n, n);
+        }
+      }
     }
 
     private IEnumerable<Block> OriginalProgramBlocks()
@@ -142,10 +150,9 @@ namespace Microsoft.Boogie
         newProcedureExitNodes[impl.Name] = newExit;
         foreach (Block b in impl.Blocks)
         {
-          List<List<Cmd>> partition = PartitionCmdsAccordingToPredicate(b.Cmds, Item => Item is CallCmd);
           Block prev = null;
           int i = 0;
-          foreach (List<Cmd> cmds in partition)
+          foreach (List<Cmd> cmds in SeparateCallCmds(b.Cmds))
           {
             Block newBlock;
             if (prev == null)
@@ -190,16 +197,24 @@ namespace Microsoft.Boogie
       #endregion
     }
 
-    public static List<List<Cmd>> PartitionCmdsAccordingToPredicate(List<Cmd> Cmds, Func<Cmd, bool> Predicate) {
+    private static List<List<Cmd>> SeparateCallCmds(List<Cmd> Cmds) {
       List<List<Cmd>> result = new List<List<Cmd>>();
-      List<Cmd> current = new List<Cmd>();
-      result.Add(current);
-      foreach(Cmd cmd in Cmds) {
-        if(Predicate(cmd) && current.Count > 0) {
-           current = new List<Cmd>();
-           result.Add(current);
+      int currentIndex = 0;
+      while(currentIndex < Cmds.Count) {
+        if(Cmds[currentIndex] is CallCmd) {
+          result.Add(new List<Cmd> { Cmds[currentIndex] });
+          currentIndex++;
+        } else {
+          List<Cmd> nonCallCmds = new List<Cmd>();
+          while(currentIndex < Cmds.Count && !(Cmds[currentIndex] is CallCmd)) {
+            nonCallCmds.Add(Cmds[currentIndex]);
+            currentIndex++;
+          }
+          result.Add(nonCallCmds);
         }
-        current.Add(cmd);
+      }
+      if(result.Count == 0) {
+        result.Add(new List<Cmd>());
       }
       return result;
     }
-- 
cgit v1.2.3