diff options
Diffstat (limited to 'Source/Concurrency/TypeCheck.cs')
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 254f058d..8c738727 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -286,31 +286,37 @@ namespace Microsoft.Boogie inAtomicSpecification = false;
return ret;
}
- int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", int.MaxValue);
- assertionPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
+ foreach (int phaseNum in OwickiGries.FindPhaseNums(ensures.Attributes))
{
- Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");
+ assertionPhaseNums.Add(phaseNum);
+ if (phaseNum > enclosingProcPhaseNum)
+ {
+ Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");
+ }
}
return ensures;
}
public override Requires VisitRequires(Requires requires)
{
- int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", int.MaxValue);
- assertionPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
+ foreach (int phaseNum in OwickiGries.FindPhaseNums(requires.Attributes))
{
- Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");
+ assertionPhaseNums.Add(phaseNum);
+ if (phaseNum > enclosingProcPhaseNum)
+ {
+ Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");
+ }
}
return requires;
}
public override Cmd VisitAssertCmd(AssertCmd node)
{
- int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", int.MaxValue);
- assertionPhaseNums.Add(phaseNum);
- if (phaseNum > enclosingProcPhaseNum)
+ foreach (int phaseNum in OwickiGries.FindPhaseNums(node.Attributes))
{
- Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");
+ assertionPhaseNums.Add(phaseNum);
+ if (phaseNum > enclosingProcPhaseNum)
+ {
+ Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");
+ }
}
return node;
}
|