diff options
author | Shaz Qadeer <qadeer@microsoft.com> | 2015-09-27 23:22:01 -0700 |
---|---|---|
committer | Shaz Qadeer <qadeer@microsoft.com> | 2015-09-27 23:22:01 -0700 |
commit | 661de7cd7c192b40d01823f52fb91f23b06e6e58 (patch) | |
tree | 0923b1b2248b1560d52da02cd812c3de35c3cd98 /Source | |
parent | e7a15ef3363e69b24b70f0e5de5cecc56d501a2b (diff) |
a bug fix
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Concurrency/TypeCheck.cs | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 79424303..0e257f30 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -379,24 +379,23 @@ namespace Microsoft.Boogie if (!procToAtomicProcedureInfo.ContainsKey(callCmd.Proc)) return true; var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc]; - if (atomicProcedureInfo.isPure) + if (callCmd.Proc.Modifies.Count > 0) + { + return enclosingProcLayerNum == layerNum; + } + if (callCmd.Outs.Count == 0) { return true; } - else if (callCmd.Proc.Modifies.Count == 0) + var outputVar = callCmd.Outs[0].Decl; + var localVariableInfo = localVarToLocalVariableInfo[outputVar]; + if (localVariableInfo.isGhost) { - if (callCmd.Outs.Count == 0) - return true; - var outputVar = callCmd.Outs[0].Decl; - Debug.Assert(localVarToLocalVariableInfo.ContainsKey(outputVar)); - if (localVarToLocalVariableInfo[outputVar].isGhost) - { - return localVarToLocalVariableInfo[outputVar].layer == layerNum; - } - else - { - return enclosingProcLayerNum == layerNum; - } + return localVariableInfo.layer == layerNum; + } + if (atomicProcedureInfo.isPure) + { + return localVariableInfo.layer <= layerNum; } else { |