From cbbced423ed4887ea78628066bc57c4aa36997d1 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 8 Oct 2015 20:53:09 -0700 Subject: removed an extraneous warning --- Source/Concurrency/CivlTypeChecker.cs | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'Source') diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 430c0d2c..b0ea678c 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -874,16 +874,9 @@ namespace Microsoft.Boogie if (node.Proc.Modifies.Count > 0) { var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc]; - if (procToActionInfo[enclosingImpl.Proc] is AtomicActionInfo) + if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) { - if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum)) - { - Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee"); - } - } - else - { - Error(node, "Enclosing implementation must refine an atomic action"); + Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee"); } introducedLocalVarsUpperBound = enclosingProcLayerNum; } -- cgit v1.2.3