fixes to type checking code

2 files changed, 26 insertions, 12 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 8f8638d6..b3b3b34a 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -19,7 +19,8 @@ namespace Microsoft.Boogie
         CheckingContext checkingContext;

         public int errorCount;

         HashSet<Variable> globalVariables;

-        bool insideYield;

+        bool globalVarAccessAllowed;

+        bool visitingProcedure;

         int phaseNumEnclosingProc;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

@@ -57,25 +58,27 @@ namespace Microsoft.Boogie
 

         public MoverTypeChecker(Program program)

         {

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

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

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

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

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

             this.program = program;

+            this.visitingProcedure = false;

+            this.phaseNumEnclosingProc = int.MaxValue;

         }

         public override Block VisitBlock(Block node)

         {

-            insideYield = false;

+            globalVarAccessAllowed = false;

             return base.VisitBlock(node);

         }

         public override Cmd VisitHavocCmd(HavocCmd node)

         {

-            insideYield = false;

+            globalVarAccessAllowed = false;

             return base.VisitHavocCmd(node);

         }

         public override Cmd VisitAssignCmd(AssignCmd node)

         {

-            insideYield = false;

+            globalVarAccessAllowed = false;

             return base.VisitAssignCmd(node);

         }

         public override Implementation VisitImplementation(Implementation node)

@@ -85,12 +88,15 @@ namespace Microsoft.Boogie
         }

         public override Procedure VisitProcedure(Procedure node)

         {

+            visitingProcedure = true;

             phaseNumEnclosingProc = FindPhaseNumber(node);

-            return base.VisitProcedure(node);

+            Procedure ret = base.VisitProcedure(node);

+            visitingProcedure = false;

+            return ret;

         } 

         public override Cmd VisitCallCmd(CallCmd node)

         {

-            insideYield = false;

+            globalVarAccessAllowed = false;

             if (!node.IsAsync && node.InParallelWith == null) {

 

                 int calleePhaseNum = FindPhaseNumber(node.Proc);

@@ -103,16 +109,16 @@ namespace Microsoft.Boogie
         }

         public override YieldCmd VisitYieldCmd(YieldCmd node)

         {

-            insideYield = true;

+            globalVarAccessAllowed = true;

             return base.VisitYieldCmd(node);

         }

-        public override Variable VisitVariable(Variable node)

+        public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

-            if (!insideYield && globalVariables.Contains(node))

+            if (!visitingProcedure && !globalVarAccessAllowed && globalVariables.Contains(node.Decl))

             {

                 Error(node, "Cannot access global variable");

             }

-            return base.VisitVariable(node);

+            return base.VisitIdentifierExpr(node);

         }

         public override Ensures VisitEnsures(Ensures ensures)

         {

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 1776f64e..d1651ff4 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2358,6 +2358,11 @@ namespace Microsoft.Boogie {
             QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||

             QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||

             QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;

+      if (isAtomicSpecification && !tc.Yields)

+      {

+          tc.Error(this, "atomic specification allowed only in a yielding procedure");

+          return;

+      }

       bool oldYields = tc.Yields;

       tc.Yields = isAtomicSpecification;

       this.Condition.Typecheck(tc);

@@ -2520,10 +2525,13 @@ namespace Microsoft.Boogie {
         Contract.Assert(e != null);

         e.Typecheck(tc);

       }

+      bool oldYields = tc.Yields;

+      tc.Yields = QKeyValue.FindBoolAttribute(Attributes, "yields");

       foreach (Ensures/*!*/ e in Ensures) {

         Contract.Assert(e != null);

         e.Typecheck(tc);

       }

+      tc.Yields = oldYields;

     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {