From 75b7f29830013051c14990d515d4948cdf917148 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 17 Dec 2014 10:26:33 -0800
Subject: some refactoring to separate the concept of shared variables under
 refinement checking with all global variables

---
 Source/Concurrency/MoverCheck.cs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Source/Concurrency/MoverCheck.cs')

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 1dd350de..b10cd6cd 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)));
+            moverTypeChecker.SharedVariables.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)));
+            moverTypeChecker.SharedVariables.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)));
+            moverTypeChecker.SharedVariables.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)));
+            moverTypeChecker.SharedVariables.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;
-- 
cgit v1.2.3