some bugs fixed on yiledtypechecker

1 files changed, 37 insertions, 49 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index ed64162a..5affd182 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -141,6 +141,18 @@ namespace Microsoft.Boogie
 

     public class MoverTypeChecker : StandardVisitor

     {

+        public int FindPhaseNumber(Procedure proc)

+        {

+            if (procToActionInfo.ContainsKey(proc))

+                return procToActionInfo[proc].phaseNum;

+            else

+                return int.MaxValue;

+        }

+        public HashSet<Variable> QedGlobalVariables()

+        {

+            return qedGlobalVariables;

+        }

+

         CheckingContext checkingContext;

         public int errorCount;

         HashSet<Variable> qedGlobalVariables;

@@ -149,36 +161,6 @@ namespace Microsoft.Boogie
         public Program program;

         public HashSet<int> assertionPhaseNums;

         bool inAtomicSpecification;

-        CallCmd callCmd;

-

-        public MoverTypeChecker(Program program)

-        {

-            this.qedGlobalVariables = new HashSet<Variable>();

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

-            {

-                if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))

-                {

-                    this.qedGlobalVariables.Add(g);

-                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

-                }

-            }

-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

-            this.assertionPhaseNums = new HashSet<int>();

-            this.errorCount = 0;

-            this.checkingContext = new CheckingContext(null);

-            this.program = program;

-            this.enclosingProcPhaseNum = int.MaxValue;

-            this.inAtomicSpecification = false;

-            this.callCmd = null;

-        }

-

-        public int FindPhaseNumber(Procedure proc)

-        {

-            if (procToActionInfo.ContainsKey(proc))

-                return procToActionInfo[proc].phaseNum;

-            else

-                return int.MaxValue;

-        }

 

         public void TypeCheck()

         {

@@ -211,6 +193,25 @@ namespace Microsoft.Boogie
 #endif

         }

 

+        public MoverTypeChecker(Program program)

+        {

+            this.qedGlobalVariables = new HashSet<Variable>();

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

+            {

+                if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))

+                {

+                    this.qedGlobalVariables.Add(g);

+                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);

+                }

+            }

+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

+            this.assertionPhaseNums = new HashSet<int>();

+            this.errorCount = 0;

+            this.checkingContext = new CheckingContext(null);

+            this.program = program;

+            this.enclosingProcPhaseNum = int.MaxValue;

+            this.inAtomicSpecification = false;

+        }

         public override Implementation VisitImplementation(Implementation node)

         {

             enclosingProcPhaseNum = FindPhaseNumber(node.Proc);

@@ -220,7 +221,7 @@ namespace Microsoft.Boogie
         {

             enclosingProcPhaseNum = FindPhaseNumber(node);

             return base.VisitProcedure(node);

-        } 

+        }

         public override Cmd VisitCallCmd(CallCmd node)

         {

             if (!node.IsAsync)

@@ -235,10 +236,7 @@ namespace Microsoft.Boogie
                     Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

                 }

             }

-            callCmd = node;

-            Cmd ret = base.VisitCallCmd(node);

-            callCmd = null;

-            return ret;

+            return base.VisitCallCmd(node);

         }

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

@@ -248,9 +246,6 @@ namespace Microsoft.Boogie
                 int calleePhaseNum = FindPhaseNumber(iter.Proc);

                 if (calleePhaseNum > maxCalleePhaseNum)

                     maxCalleePhaseNum = calleePhaseNum;

-                callCmd = iter;

-                base.VisitCallCmd(iter);

-                callCmd = null;

             }

 

             if (enclosingProcPhaseNum > maxCalleePhaseNum)

@@ -275,20 +270,13 @@ namespace Microsoft.Boogie
         {

             if (node.Decl is GlobalVariable)

             {

-                if (callCmd != null && procToActionInfo.ContainsKey(callCmd.Proc))

+                if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))

                 {

-                    Error(node, "Cannot access global variable in call to atomic action");

+                    Error(node, "Cannot access non-qed global variable in atomic action");

                 }

-                else

+                else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))

                 {

-                    if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))

-                    {

-                        Error(node, "Cannot access non-qed global variable in atomic action");

-                    }

-                    else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))

-                    {

-                        Error(node, "Cannot access qed global variable in ordinary code");

-                    }

+                    Error(node, "Cannot access qed global variable in ordinary code");

                 }

             }

             return base.VisitIdentifierExpr(node);