diff options
Diffstat (limited to 'Test/linear/async-bug.bpl')
-rw-r--r-- | Test/linear/async-bug.bpl | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl index ad7020ad..4692f267 100644 --- a/Test/linear/async-bug.bpl +++ b/Test/linear/async-bug.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const GcTid:int;
-
-procedure {:yields} {:layer 100} Initialize({:linear "tid"} tid:int)
-requires{:layer 100} tid == GcTid;
-{
- yield;
- assert{:layer 100} tid == GcTid;
-
- call GarbageCollect(tid);
-
- yield;
- assert{:layer 100} tid == GcTid;
-
- async call GarbageCollect(tid);
-
- yield;
- assert{:layer 100} tid == GcTid;
-
- async call GarbageCollect(tid);
-
- yield;
- assert{:layer 100} tid == GcTid;
-
- yield;
- assert{:layer 100} tid == GcTid;
-}
-
-procedure {:yields} {:layer 100} GarbageCollect({:linear "tid"} tid:int)
-requires{:layer 100} tid == GcTid;
-{
- yield;
- assert{:layer 100} tid == GcTid;
-}
-
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const GcTid:int; + +procedure {:yields} {:layer 100} Initialize({:linear "tid"} tid:int) +requires{:layer 100} tid == GcTid; +{ + yield; + assert{:layer 100} tid == GcTid; + + call GarbageCollect(tid); + + yield; + assert{:layer 100} tid == GcTid; + + async call GarbageCollect(tid); + + yield; + assert{:layer 100} tid == GcTid; + + async call GarbageCollect(tid); + + yield; + assert{:layer 100} tid == GcTid; + + yield; + assert{:layer 100} tid == GcTid; +} + +procedure {:yields} {:layer 100} GarbageCollect({:linear "tid"} tid:int) +requires{:layer 100} tid == GcTid; +{ + yield; + assert{:layer 100} tid == GcTid; +} + |