Did more refactoring and addressed several todos.

4 files changed, 11 insertions, 11 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;