diff options
Diffstat (limited to 'Test/og/parallel1.bpl')
| -rw-r--r-- | Test/og/parallel1.bpl | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index cb3502b4..ecddc9fc 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -1,26 +1,27 @@ var g:int;
-procedure PB()
+procedure {:yields} {:stable} PB()
+modifies g;
{
g := g + 1;
}
-procedure PC()
- ensures g == 3;
+procedure {:yields} {:stable} PC()
+ensures g == 3;
{
g := 3;
yield;
assert g == 3;
}
-procedure PD()
+procedure {:yields} {:stable} PD()
{
call PC();
assert g == 3;
yield;
}
-procedure{:entrypoint} Main()
+procedure {:entrypoint} {:yields} Main()
{
while (true)
{
|