1 files changed, 78 insertions, 0 deletions
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.ssc b/Source/AbsInt/LoopInvariantsOnDemand.ssc
new file mode 100644
index 00000000..1ebd11b2
--- /dev/null
+++ b/Source/AbsInt/LoopInvariantsOnDemand.ssc
@@ -0,0 +1,78 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using AI = Microsoft.AbstractInterpretationFramework;
+using Boogie = Microsoft.Boogie;
+  /// <summary>
+  /// A visitor of an abstract interpretation expression that collects the free variables 
+  /// </summary>      
+  class FreeVariablesVisitor : AI.ExprVisitor 
+  {
+    [Peer] List<AI.IVariable!>! variables;
+    public List<AI.IVariable!>! FreeVariables 
+    {
+      get
+      {
+        return this.variables;
+      }    
+    }
+
+    List<string!>! varNames;    // used to check the consinstency!
+
+    public FreeVariablesVisitor() 
+    {
+      this.variables = new List<AI.IVariable!>(); 
+      this.varNames = new List<string!>();
+    }
+
+    override public object Default(AI.IExpr! expr)
+    {
+      if (expr is AI.IVariable) 
+      {
+        if(!variables.Contains((AI.IVariable) expr)) 
+        {
+          this.variables.Add((AI.IVariable) expr);
+                      
+          assert ! this.varNames.Contains(expr.ToString());     // If we get there, we have an error: two variables with the same name but different identity  
+             
+          this.varNames.Add(expr.ToString());
+        }
+        return null;
+      }
+      else if (expr is AI.IFunApp)
+        return VisitFunApp((AI.IFunApp) expr);
+      else if (expr is AI.IFunction)
+        return VisitFunction((AI.IFunction)expr);
+      else 
+      {
+        assert false;
+      }
+    }
+
+    public override object VisitFunApp(AI.IFunApp! funapp)
+    {
+      foreach (AI.IExpr! arg in funapp.Arguments)
+      {
+        arg.DoVisit(this);
+      }
+      return true;
+    }
+                
+    public override object VisitFunction(AI.IFunction! fun)
+    {
+      fun.Body.DoVisit(this);
+      this.variables.Remove(fun.Param);
+      return true;
+    }
+
+  } 
+
+}
+\ No newline at end of file