checkpoint

1 files changed, 17 insertions, 11 deletions

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 307d55c8..b173ecd4 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: int;

+var {:phase 2} b: int;

 

-procedure {:yields} {:entrypoint} main()

+procedure {:yields} {:phase 2} main()

 {

     while (*)

     {

+        yield;

+

         async call Customer();

+

+        yield;

     }

 }

 

-procedure {:yields} {:stable} Customer()

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

 {

     while (*) 

     {

@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;

 

     	call Leave();

+

+        yield;

     }

 

     yield;

 }

 

-procedure {:yields} Enter() 

-ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;

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

+ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

     while (true) { 

@@ -46,15 +52,15 @@ ensures {:atomic 1} |{ A: assume b == 0; b := 1; return true; }|;
     }

 }

 

-procedure {:yields} Read() returns (val: int);

-ensures {:atomic 0} |{ A: val := b; return true; }|;

+procedure {:yields} {:phase 0,2} Read() returns (val: int);

+ensures {:atomic} |{ A: val := b; return true; }|;

 

-procedure {:yields} CAS(prev: int, next: int) returns (_old: int);

-ensures {:atomic 0} |{ 

+procedure {:yields} {:phase 0,2} CAS(prev: int, next: int) returns (_old: int);

+ensures {:atomic} |{ 

 A: _old := b; goto B, C; 

 B: assume _old == prev; b := next; return true; 

 C: assume _old != prev; return true; 

 }|;

 

-procedure {:yields} Leave();

-ensures {:atomic 0} |{ A: b := 0; return true; }|;

+procedure {:yields} {:phase 0,2} Leave();

+ensures {:atomic} |{ A: b := 0; return true; }|;