diff options
| author |  qadeer <unknown> | 2013-12-24 20:52:24 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-24 20:52:24 -0800 |
| commit | 0b396a7572daddd3f5dc1873c4507f92c078d6bb (patch) | |
| tree | e33b94bd4b5046dbe0bce0799c1c41e37e1e74c7 /Source/Concurrency/TypeCheck.cs | |
| parent | 7469e1902162ccfa08a5cf07660a7acfff43136a (diff) | |
more bug fixes
updates to DeviceCache.bpl to make it verify
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;
}
|