diff options
| author |  qadeer <unknown> | 2014-12-15 11:33:23 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-12-15 11:33:23 -0800 |
| commit | 41c1ea3efbbf1b5d7758ab334ab456462300f555 (patch) | |
| tree | ed21768d494420a36f0d1e5d2d062dbead813c1a /Source/Concurrency | |
| parent | a7f872a71b1be2b9677add91c8366ee27e345856 (diff) | |
1. made variable introduction layer explicit in the test cases
2. if a single layer is specified for a global variable, that layer is the introduction layer
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 39d75119..b8c94dc8 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -272,16 +272,16 @@ namespace Microsoft.Boogie {
if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
- int layerNum = int.MaxValue;
+ int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error
int availableUptoLayerNum = int.MaxValue;
List<int> attrs = FindLayers(proc.Attributes);
if (attrs.Count == 1)
{
- layerNum = attrs[0];
+ createdAtLayerNum = attrs[0];
}
else if (attrs.Count == 2)
{
- layerNum = attrs[0];
+ createdAtLayerNum = attrs[0];
availableUptoLayerNum = attrs[1];
}
else
@@ -312,7 +312,7 @@ namespace Microsoft.Boogie enclosingImpl = null;
base.VisitEnsures(e);
canAccessSharedVars = false;
- if (maxLayerNum <= layerNum && availableUptoLayerNum <= minLayerNum)
+ if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum)
{
// ok
}
@@ -321,11 +321,11 @@ namespace Microsoft.Boogie Error(e, "A variable being accessed is hidden before this action becomes unavailable");
}
- procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, layerNum, availableUptoLayerNum);
+ procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
}
if (!procToActionInfo.ContainsKey(proc))
{
- procToActionInfo[proc] = new ActionInfo(proc, layerNum, availableUptoLayerNum);
+ procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
}
}
if (errorCount > 0) return;
@@ -357,11 +357,11 @@ namespace Microsoft.Boogie this.hideLayerNums[g] = int.MaxValue;
if (layerNums.Count == 0)
{
- // ok
+ Error(g, "Too few layer numbers");
}
else if (layerNums.Count == 1)
{
- this.hideLayerNums[g] = layerNums[0];
+ this.introduceLayerNums[g] = layerNums[0];
}
else if (layerNums.Count == 2)
{
|