From 661de7cd7c192b40d01823f52fb91f23b06e6e58 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 27 Sep 2015 23:22:01 -0700 Subject: a bug fix --- Source/Concurrency/TypeCheck.cs | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'Source/Concurrency') 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 { -- cgit v1.2.3