Did more refactoring and addressed several todos.

15 files changed, 190 insertions, 94 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index e3bc3bfe..0146ad75 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -110,7 +110,7 @@ namespace Microsoft.Boogie
         }

         public override Program VisitProgram(Program node)

         {

-            foreach (GlobalVariable g in program.GlobalVariables())

+            foreach (GlobalVariable g in program.GlobalVariables)

             {

                 string domainName = FindDomainName(g);

                 if (domainName != null)

@@ -620,7 +620,7 @@ namespace Microsoft.Boogie
                 var domainName = FindDomainName(v);

                 domainNameToScope[domainName].Add(v);

             }

-            foreach (Variable v in program.GlobalVariables())

+            foreach (Variable v in program.GlobalVariables)

             {

                 var domainName = FindDomainName(v);

                 if (domainName == null) continue;

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index dcc59878..d98d9e1f 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -508,7 +508,7 @@ namespace Microsoft.Boogie
             ensures.Add(ensureCheck);

             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);

             impl.Proc = proc;

@@ -551,7 +551,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

@@ -599,7 +599,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

@@ -633,7 +633,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             impl.Proc = proc;

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index baea905a..69e6b318 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -201,7 +201,7 @@ namespace Microsoft.Boogie
                 }

                 procMap[node] = proc;

                 proc.Modifies = new List<IdentifierExpr>();

-                moverTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));

+                moverTypeChecker.program.GlobalVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

             }

             return procMap[node];

         }

@@ -297,7 +297,7 @@ namespace Microsoft.Boogie
             this.yieldingProcs = duplicator.yieldingProcs;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

-            foreach (Variable g in program.GlobalVariables())

+            foreach (Variable g in program.GlobalVariables)

             {

                 globalMods.Add(Expr.Ident(g));

             }

@@ -756,9 +756,9 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

                 }

                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

-                frame = new HashSet<Variable>(program.GlobalVariables());

+                frame = new HashSet<Variable>(program.GlobalVariables);

                 HashSet<Variable> introducedVars = new HashSet<Variable>();

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in program.GlobalVariables)

                 {

                     if (moverTypeChecker.hidePhaseNums[v] <= actionInfo.phaseNum || moverTypeChecker.introducePhaseNums[v] > actionInfo.phaseNum)

                     {

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index cd636946..96b03ad9 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -351,7 +351,7 @@ namespace Microsoft.Boogie
             this.canAccessAuxVars = false;

             this.minPhaseNum = int.MaxValue;

             this.maxPhaseNum = -1;

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

             {

                 List<int> phaseNums = FindIntAttributes(g.Attributes, "phase");

                 this.introducePhaseNums[g] = 0;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 38a83b12..30333259 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -295,44 +295,13 @@ namespace Microsoft.Boogie {
   }

 

   public class Program : Absy {

-    [Rep]

-    private List<Declaration/*!*/>/*!*/ topLevelDeclarations;

-

-    public IEnumerable<Declaration> TopLevelDeclarations

-    {

-      get

-      {

-        return topLevelDeclarations;

-      }

-    }

-

-    public void AddTopLevelDeclaration(Declaration decl)

-    {

-      topLevelDeclarations.Add(decl);

-    }

-

-    public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

-    {

-      topLevelDeclarations.AddRange(decls);

-    }

-

-    public void RemoveTopLevelDeclarations(Predicate<Declaration> match)

-    {

-      topLevelDeclarations.RemoveAll(match);

-    }

-

-    public void ClearTopLevelDeclarations()

-    {

-      topLevelDeclarations.Clear();

-    }

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));

-      Contract.Invariant(globals == null || cce.NonNullElements(globals));

+      Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));

     }

-

-

+    

     public Program()

       : base(Token.NoToken) {

       this.topLevelDeclarations = new List<Declaration>();

@@ -472,35 +441,164 @@ namespace Microsoft.Boogie {
       }

     }

 

+    [Rep]

+    private List<Declaration/*!*/>/*!*/ topLevelDeclarations;

+

+    public IEnumerable<Declaration> TopLevelDeclarations

+    {

+      get

+      {

+        return topLevelDeclarations;

+      }

+    }

+

+    public void AddTopLevelDeclaration(Declaration decl)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.Add(decl);

+      this.globalVariablesCache = null;

+    }

+

+    public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.AddRange(decls);

+      this.globalVariablesCache = null;

+    }

+

+    public void RemoveTopLevelDeclarations(Predicate<Declaration> match)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.RemoveAll(match);

+      this.globalVariablesCache = null;

+    }

+

+    public void ClearTopLevelDeclarations()

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.Clear();

+      this.globalVariablesCache = null;

+    }

+

+    bool topLevelDeclarationsAreFrozen;

+    public bool TopLevelDeclarationsAreFrozen { get { return topLevelDeclarationsAreFrozen; } }

+    public void FreezeTopLevelDeclarations()

+    {

+      topLevelDeclarationsAreFrozen = true;

+    }

+

+    Dictionary<string, Implementation> implementationsCache;

     public IEnumerable<Implementation> Implementations

     {

       get

       {

-        return TopLevelDeclarations.OfType<Implementation>();

+        if (implementationsCache != null)

+        {

+          return implementationsCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Implementation>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          implementationsCache = result.ToDictionary(p => p.Id);

+        }

+        return result;

+      }

+    }

+

+    public Implementation FindImplementation(string id)

+    {

+      Implementation result = null;

+      if (implementationsCache != null && implementationsCache.TryGetValue(id, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Implementations.FirstOrDefault(i => i.Id == id);

       }

     }

 

+    IEnumerable<Axiom> axiomsCache;

     public IEnumerable<Axiom> Axioms

     {

       get

       {

-        return TopLevelDeclarations.OfType<Axiom>();

+        if (axiomsCache != null)

+        {

+          return axiomsCache;

+        }

+        var result = TopLevelDeclarations.OfType<Axiom>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          axiomsCache = result;

+        }

+        return result;

       }

     }

 

+    Dictionary<string, Procedure> proceduresCache;

     public IEnumerable<Procedure> Procedures

     {

       get

       {

-        return TopLevelDeclarations.OfType<Procedure>();

+        if (proceduresCache != null)

+        {

+          return proceduresCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Procedure>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          proceduresCache = result.ToDictionary(p => p.Name);

+        }

+        return result;

+      }

+    }

+

+    public Procedure FindProcedure(string name)

+    {

+      Procedure result = null;

+      if (proceduresCache != null && proceduresCache.TryGetValue(name, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Procedures.FirstOrDefault(p => p.Name == name);

       }

     }

 

+    Dictionary<string, Function> functionsCache;

     public IEnumerable<Function> Functions

     {

       get

       {

-        return TopLevelDeclarations.OfType<Function>();

+        if (functionsCache != null)

+        {

+          return functionsCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Function>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          functionsCache = result.ToDictionary(f => f.Name);

+        }

+        return result;

+      }

+    }

+

+    public Function FindFunction(string name)

+    {

+      Function result = null;

+      if (functionsCache != null && functionsCache.TryGetValue(name, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Functions.FirstOrDefault(f => f.Name == name);

       }

     }

     

@@ -520,6 +618,21 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private List<GlobalVariable/*!*/> globalVariablesCache = null;

+    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<GlobalVariable>>()));

+

+        if (globalVariablesCache == null)

+        {

+          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>().ToList();

+        }

+        return globalVariablesCache;

+      }

+    }

+

     public IEnumerable<Block> Blocks()

     {

       return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);

@@ -1110,18 +1223,6 @@ namespace Microsoft.Boogie {
       return visitor.VisitProgram(this);

     }

 

-    private List<GlobalVariable/*!*/> globals = null;

-    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));

-      if (globals != null)

-        return globals;

-      globals = new List<GlobalVariable/*!*/>();

-      foreach (var gvar in TopLevelDeclarations.OfType<GlobalVariable>()) {

-        globals.Add(gvar);

-      }

-      return globals;

-    }

-

     private int invariantGenerationCounter = 0;

 

     public Constant MakeExistentialBoolean(int StageId) {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index e6cf3e9d..e9975fe5 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -987,7 +987,7 @@ namespace Microsoft.Boogie {
       }

       // Return default: all globals and out params

       HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

-      foreach (Variable/*!*/ v in prog.GlobalVariables()) {

+      foreach (Variable/*!*/ v in prog.GlobalVariables) {

         Contract.Assert(v != null);

         lv.Add(v);

       }

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

       // Return default: all globals and in params

       HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

-      foreach (Variable/*!*/ v in prog.GlobalVariables()) {

+      foreach (Variable/*!*/ v in prog.GlobalVariables) {

         Contract.Assert(v != null);

         lv.Add(v);

       }

@@ -1275,7 +1275,7 @@ Contract.Assert(b != null);
 //Set<Variable!> lv = cfg.weightBefore[b].getLiveVars();

 b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];

 //foreach(GlobalVariable/*!*/

-      /* v in program.GlobalVariables()){Contract.Assert(v != null);

+      /* v in program.GlobalVariables){Contract.Assert(v != null);

 //  b.liveVarsBefore.Add(v);

 //}

 }

@@ -1482,7 +1482,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) {

           LiteralExpr le = (LiteralExpr)predicateCmd.Expr;

           if (le.IsFalse) {

-            var globals = prog.GlobalVariables();

+            var globals = prog.GlobalVariables;

             Contract.Assert(cce.NonNullElements(globals));

             foreach (Variable/*!*/ v in globals) {

               Contract.Assert(v != null);

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 6dd030e8..b275288a 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -640,8 +640,7 @@ namespace Microsoft.Boogie {
           var funCall = nAryExpr.Fun as FunctionCall;

           if (funCall != null)

           {

-            // TODO(wuestholz): Maybe we should speed up this lookup.

-            funCall.Func = Program.Functions.FirstOrDefault(f => f.Name == funCall.FunctionName);

+            funCall.Func = Program.FindFunction(funCall.FunctionName);

           }

         }

         return result;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index fc2608b7..7472ec3d 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -108,7 +108,7 @@ namespace Microsoft.Boogie {
         {

             DistinguishPrefix(v.Name);

         }

-        foreach (var v in program.GlobalVariables())

+        foreach (var v in program.GlobalVariables)

         {

             DistinguishPrefix(v.Name);

         }

diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 4fd574a4..d4d4db21 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -594,7 +594,7 @@ namespace VC {
       {

         List<Cmd> cc = new List<Cmd>();

         // where clauses of global variables

-        foreach (var gvar in program.GlobalVariables()) {

+        foreach (var gvar in program.GlobalVariables) {

           if (gvar.TypedIdent.WhereExpr != null) {

             Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

             cc.Add(c);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 11558750..b5f4f87b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -875,7 +875,6 @@ namespace Microsoft.Boogie
       Implementation[] stablePrioritizedImpls = null;

       if (0 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        // TODO(wuestholz): Maybe we should speed up this lookup.

         OtherDefinitionAxiomsCollector.Collect(program.Axioms);

         DependencyCollector.Collect(program);

         stablePrioritizedImpls = impls.OrderByDescending(

@@ -992,6 +991,7 @@ namespace Microsoft.Boogie
 

       if (1 < CommandLineOptions.Clo.VerifySnapshots && programId != null)

       {

+        program.FreezeTopLevelDeclarations();

         programCache.Set(programId, program, policy);

       }

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 93ca9cb7..67d6dde5 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -193,8 +193,7 @@ namespace Microsoft.Boogie
 

     private static void SetAssertionChecksums(Implementation implementation, Program program)

     {

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.FindImplementation(implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;

@@ -203,8 +202,7 @@ namespace Microsoft.Boogie
 

     private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

     {

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);

+      var implPrevSnap = program.FindImplementation(implementation.Id);

       if (implPrevSnap != null)

       {

         implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

@@ -215,8 +213,7 @@ namespace Microsoft.Boogie
     {

       var result = base.VisitCallCmd(node);

 

-      // TODO(wuestholz): Maybe we should speed up this lookup.

-      var oldProc = programInCachedSnapshot.Procedures.FirstOrDefault(p => p.Name == node.Proc.Name);

+      var oldProc = programInCachedSnapshot.FindProcedure(node.Proc.Name);

       if (oldProc != null

           && oldProc.DependencyChecksum != node.Proc.DependencyChecksum

           && node.AssignedAssumptionVariable == null)

@@ -326,7 +323,6 @@ namespace Microsoft.Boogie
     {

       Contract.Requires(oldProc != null && newProg != null);

 

-      // TODO(wuestholz): Maybe we should speed up this lookup.

       var funcs = newProg.Functions;

       return oldProc.DependenciesCollected

              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index d9961a64..6920ade3 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2359,7 +2359,7 @@ namespace Microsoft.Boogie.Houdini {
                 return Expr.True;

 

             var vars = new Dictionary<string, Expr>();

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

                 vars.Add(g.Name, Expr.Ident(g));

             foreach (var v in proc.InParams.OfType<Variable>())

                 vars.Add(v.Name, Expr.Ident(v));

@@ -2441,7 +2441,7 @@ namespace Microsoft.Boogie.Houdini {
                         var forold = new Dictionary<string, Expr>();

                         var always = new Dictionary<string, Expr>();

                         int i = 0;

-                        foreach (var g in program.GlobalVariables())

+                        foreach (var g in program.GlobalVariables)

                         {

                             forold.Add(g.Name, expr.Args[i]);

                             always.Add(g.Name, expr.Args[i]);

@@ -2742,7 +2742,7 @@ namespace Microsoft.Boogie.Houdini {
             var ret = new Dictionary<string, VCExpr>();

 

             var cnt = 0;

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

             {

                 ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]);

                 cnt++;

@@ -2757,7 +2757,7 @@ namespace Microsoft.Boogie.Houdini {
 

             // Fill up values of globals that are not modified

             cnt = 0;

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

             {

                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }

 

@@ -2784,7 +2784,7 @@ namespace Microsoft.Boogie.Houdini {
             var implVars = impl2EndStateVars[impl.Name];

 

             var cnt = 0;

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

             {

                 ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model));

                 cnt++;

@@ -2799,7 +2799,7 @@ namespace Microsoft.Boogie.Houdini {
 

             // Fill up values of globals that are not modified

             cnt = 0;

-            foreach (var g in program.GlobalVariables())

+            foreach (var g in program.GlobalVariables)

             {

                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }

 

@@ -2869,7 +2869,7 @@ namespace Microsoft.Boogie.Houdini {
         private void attachEnsures(Implementation impl)

         {

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

-            foreach (Variable v in vcgen.program.GlobalVariables())

+            foreach (Variable v in vcgen.program.GlobalVariables)

             {

                 functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));

             }

@@ -2891,7 +2891,7 @@ namespace Microsoft.Boogie.Houdini {
             prover.Context.DeclareFunction(function, "");

 

             List<Expr> exprs = new List<Expr>();

-            foreach (Variable v in vcgen.program.GlobalVariables())

+            foreach (Variable v in vcgen.program.GlobalVariables)

             {

                 Contract.Assert(v != null);

                 exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index ee33253f..4b4e970e 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -195,7 +195,7 @@ namespace Microsoft.Boogie
             {

                 // in flat mode, all live globals should be in live set

 #if false

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in program.GlobalVariables)

                 {

                     vars.Add(v);

                     names.Add(v.ToString());

@@ -214,7 +214,7 @@ namespace Microsoft.Boogie
             }

             else

             {

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in program.GlobalVariables)

                 {

                     vars.Add(v);

                     names.Add("@old_" + v.ToString());

@@ -296,7 +296,7 @@ namespace Microsoft.Boogie
             List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

-            foreach (Variable v in program.GlobalVariables())

+            foreach (Variable v in program.GlobalVariables)

             {

                 vars.Add(v);

                 exprs.Add(new IdentifierExpr(Token.NoToken, v));

@@ -340,7 +340,7 @@ namespace Microsoft.Boogie
             List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in program.GlobalVariables)

                 {

                     vars.Add(v);

                     exprs.Add(new OldExpr(Token.NoToken,new IdentifierExpr(Token.NoToken, v)));

@@ -480,7 +480,7 @@ namespace Microsoft.Boogie
                 List<Variable> interfaceVars = new List<Variable>();

                 Expr assertExpr = new LiteralExpr(Token.NoToken, true);

                 Contract.Assert(assertExpr != null);

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in program.GlobalVariables)

                 {

                     Contract.Assert(v != null);

                     interfaceVars.Add(v);

@@ -657,7 +657,7 @@ namespace Microsoft.Boogie
                     }

                     else if (mode == Mode.Corral || proc.FindExprAttribute("inline") != null || proc is LoopProcedure)

                     {

-                        foreach (Variable v in program.GlobalVariables())

+                        foreach (Variable v in program.GlobalVariables)

                         {

                             Contract.Assert(v != null);

                             exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 5eed14fd..a9745b3c 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -210,7 +210,7 @@ namespace VC {
       impl = implementation;

 

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

-      foreach (Variable v in vcgen.program.GlobalVariables()) {

+      foreach (Variable v in vcgen.program.GlobalVariables) {

         functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));

       }

       foreach (Variable v in impl.InParams) {

@@ -228,7 +228,7 @@ namespace VC {
       vcgen.prover.Context.DeclareFunction(function, "");

 

       List<Expr> exprs = new List<Expr>();

-      foreach (Variable v in vcgen.program.GlobalVariables()) {

+      foreach (Variable v in vcgen.program.GlobalVariables) {

         Contract.Assert(v != null);

         exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

       }

@@ -310,7 +310,7 @@ namespace VC {
       }

 

       interfaceExprVars = new List<VCExprVar>();

-      foreach (Variable v in program.GlobalVariables()) {

+      foreach (Variable v in program.GlobalVariables) {

         interfaceExprVars.Add(translator.LookupVariable(v));

       }

       foreach (Variable v in impl.InParams) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 758430bd..d7320ef1 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2600,7 +2600,7 @@ namespace VC {
         // where clauses of global variables

         lock (program.TopLevelDeclarations)

         {

-          foreach (var gvar in program.GlobalVariables())

+          foreach (var gvar in program.GlobalVariables)

           {

             if (gvar != null && gvar.TypedIdent.WhereExpr != null)

             {