diff options
| author |  qadeer <unknown> | 2014-12-18 20:59:10 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-12-18 20:59:10 -0800 |
| commit | 84819ceb711f1ae83327e2006df9bb1003ccd65e (patch) | |
| tree | 93c6a25cac65ef702793fe7508eddf89df2e737e /Source/Concurrency | |
| parent | 86cb1bc74ca8b0242131145ce9d4cbab085c02fd (diff) | |
changed type checking of yield procedures so that they can only call other yielding procedures
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 10 |
1 files changed, 9 insertions, 1 deletions
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)
{
|