renamed :phase to :layer

1 files changed, 6 insertions, 6 deletions

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 86c382d8..db563cce 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-var {:phase 2} b: bool;

+var {:layer 2} b: bool;

 

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

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

 {

     yield;

     while (*)

@@ -13,7 +13,7 @@ procedure {:yields} {:phase 2} main()
     yield;

 }

 

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

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

 {

     yield;

     while (*) 

@@ -26,7 +26,7 @@ procedure {:yields} {:phase 2} Customer()
     yield;

 }

 

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

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

 ensures {:atomic} |{ A: assume !b; b := true; return true; }|;

 {

     var status: bool;

@@ -46,12 +46,12 @@ ensures {:atomic} |{ A: assume !b; b := true; return true; }|;
 	goto L;

 }

 

-procedure {:yields} {:phase 0,2} CAS(prev: bool, next: bool) returns (status: bool);

+procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool);

 ensures {:atomic} |{ 

 A: goto B, C; 

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

 C: status := false; return true; 

 }|;

 

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

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

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