updated the linear type system based on Chris' design with linear, linear_in, linear_out

1 files changed, 7 insertions, 2 deletions

diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index faa1a65d..ff6cdded 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -2,12 +2,17 @@
 // RUN: %diff "%s.expect" "%t"

 const GcTid:int;

 

-procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)

+procedure {:yields} {:phase 100} Initialize({:linear "tid"} tid:int)

 requires{:phase 100} tid == GcTid;

 {

     yield;

     assert{:phase 100} tid == GcTid;

 

+    call GarbageCollect(tid);

+

+    yield;

+    assert{:phase 100} tid == GcTid;

+

     async call GarbageCollect(tid);

 

     yield;

@@ -22,7 +27,7 @@ requires{:phase 100} tid == GcTid;
     assert{:phase 100} tid == GcTid;

 }

 

-procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)

+procedure {:yields} {:phase 100} GarbageCollect({:linear "tid"} tid:int)

 requires{:phase 100} tid == GcTid;

 {

     yield;