Updated to Staged Houdini

1 files changed, 18 insertions, 14 deletions

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index c429e199..70e33581 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie {
         dependsOnNonTransitive.AddEdge(descriptor, descriptor);

       }

 

-      foreach (var Proc in NonInlinedProcedures()) {

+      foreach (var Proc in prog.NonInlinedProcedures()) {

 

         List<Variable> parameters = new List<Variable>();

         parameters.AddRange(Proc.InParams);

@@ -152,7 +152,7 @@ namespace Microsoft.Boogie {
         }

       }

 

-      foreach (var Impl in NonInlinedImplementations()) {

+      foreach (var Impl in prog.NonInlinedImplementations()) {

 

         List<Variable> locals = new List<Variable>();

         locals.AddRange(Impl.LocVars);

@@ -163,16 +163,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private IEnumerable<Procedure> NonInlinedProcedures() {

-      return prog.Procedures.

-        Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);

-    }

-

-    private IEnumerable<Implementation> NonInlinedImplementations() {

-      return prog.Implementations.

-        Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);

-    }

-

     private List<VariableDescriptor> ComputeDependencyChain(VariableDescriptor source, VariableDescriptor target, HashSet<VariableDescriptor> visited) {

       if(source.Equals(target)) {

         return new List<VariableDescriptor> { target };

@@ -259,7 +249,7 @@ namespace Microsoft.Boogie {
       }

 

       ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks);

-      foreach (var Impl in NonInlinedImplementations()) {

+      foreach (var Impl in prog.NonInlinedImplementations()) {

 

         if (CommandLineOptions.Clo.Trace) {

           Console.WriteLine("Variable dependence analysis: Analysing " + Impl.Name);

@@ -345,7 +335,7 @@ namespace Microsoft.Boogie {
 

     private Dictionary<Block, HashSet<VariableDescriptor>> ComputeControllingVariables(Dictionary<Block, HashSet<Block>> GlobalCtrlDep) {

       Dictionary<Block, HashSet<VariableDescriptor>> result = new Dictionary<Block, HashSet<VariableDescriptor>>();

-      foreach (var Impl in NonInlinedImplementations()) {

+      foreach (var Impl in prog.NonInlinedImplementations()) {

         foreach (var b in Impl.Blocks) {

           result[b] = GetControlDependencyVariables(Impl.Name, b);

         }

@@ -639,4 +629,18 @@ namespace Microsoft.Boogie {
 

   }

 

+  public static class Helper {

+

+    public static IEnumerable<Procedure> NonInlinedProcedures(this Program prog) {

+      return prog.Procedures.

+        Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);

+    }

+

+    public static IEnumerable<Implementation> NonInlinedImplementations(this Program prog) {

+      return prog.Implementations.

+        Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);

+    }

+

+  }

+

 }