summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-11-09 10:41:46 -0800
committerGravatar qadeer <unknown>2014-11-09 10:41:46 -0800
commit0339351e985c455e7ecf290be54aa5361fe7ae8f (patch)
tree749bb04efc97ef75b2296dee90df80219fc27bf1 /Source
parent10bc14d4b152db1d98d989d629563a244b6e4272 (diff)
a fix to type checking
Diffstat (limited to 'Source')
-rw-r--r--Source/Concurrency/TypeCheck.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 96b03ad9..657e3b06 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -466,13 +466,13 @@ namespace Microsoft.Boogie
numAtomicActions++;
}
}
- if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
+ if (maxCalleePhaseNum < enclosingProcPhaseNum && !isLeftMover && !isRightMover && node.CallCmds.Count > 1)
{
- Error(node, "The procedures in the parallel call must be all right mover or all left mover");
+ Error(node, "The callees in the parallel call must be all right movers or all left movers");
}
if (maxCalleePhaseNum == enclosingProcPhaseNum && numAtomicActions > 0)
{
- Error(node, "At phase {0}, either no callee is an atomic action or no callee phase equals the phase of the enclosing procedure");
+ Error(node, "If some callee in the parallel call has the same phase as the enclosing procedure, then no callee can be an atomic action");
}
return base.VisitParCallCmd(node);
}