Did more refactoring and addressed several todos.

3 files changed, 10 insertions, 10 deletions

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)

             {