From 1c9a1f276a7e878831f2e557cbc3d24a2910e815 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 9 Jun 2014 21:01:31 +0100
Subject: Added mechanism for getting the variables referenced by a loop (not
 just the modified vars)

---
 Source/VCGeneration/VC.cs | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 7575cf28..53868e1d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2299,6 +2299,29 @@ namespace VC {
       return varsToHavoc;
     }
 
+    public static IEnumerable<Variable> VarsReferencedInLoop(Graph<Block> g, Block header)
+    {
+      HashSet<Variable> referencedVars = new HashSet<Variable>();
+      foreach (Block backEdgeNode in cce.NonNull(g.BackEdgeNodes(header)))
+      {
+        Contract.Assert(backEdgeNode != null);
+        foreach (Block b in g.NaturalLoops(header, backEdgeNode))
+        {
+          Contract.Assert(b != null);
+          foreach (Cmd c in b.Cmds)
+          {
+            Contract.Assert(c != null);
+            var Collector = new VariableCollector();
+            Collector.Visit(c);
+            foreach(var v in Collector.usedVars) {
+              referencedVars.Add(v);
+            }
+          }
+        }
+      }
+      return referencedVars;
+    }
+
     private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
 
       // K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
-- 
cgit v1.2.3