From 84819ceb711f1ae83327e2006df9bb1003ccd65e Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 18 Dec 2014 20:59:10 -0800
Subject: changed type checking of yield procedures so that they can only call
 other yielding procedures

---
 Source/Concurrency/TypeCheck.cs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'Source/Concurrency')

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 22aae914..8eb93e09 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -453,6 +453,10 @@ namespace Microsoft.Boogie
                     Error(node, "The callee is not available in the caller procedure");
                 }
             }
+            else
+            {
+                Error(node, "Yielding procedure can call only a yielding procedure");
+            }
             return base.VisitCallCmd(node);
         }
 
@@ -517,7 +521,7 @@ namespace Microsoft.Boogie
                 {
                     Error(node, "Shared variable can be accessed only in atomic actions or specifications");
                 }
-                else
+                else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
                 {
                     if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
                     {
@@ -528,6 +532,10 @@ namespace Microsoft.Boogie
                         maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
                     }
                 }
+                else
+                {
+                    Error(node, "Accessed shared variable must have layer annotation");
+                }
             }
             else if (node.Decl is LocalVariable && auxVars.Contains(node.Decl) && !canAccessAuxVars)
             {
-- 
cgit v1.2.3