simplified yield type chcking and added treiber stack (not fully done)

1 files changed, 2 insertions, 8 deletions

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 90357d4c..86c382d8 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -7,12 +7,10 @@ procedure {:yields} {:phase 2} main()
     yield;

     while (*)

     {

-        yield;

-

         async call Customer();

-

         yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 2} Customer()

@@ -20,16 +18,12 @@ procedure {:yields} {:phase 2} Customer()
     yield;

     while (*) 

     {

-    	yield;

-

         call Enter();

-

     	yield;

-

     	call Leave();

-

         yield;

     }

+    yield;

 }

 

 procedure {:yields} {:phase 1,2} Enter()