renamed :phase to :layer

1 files changed, 7 insertions, 7 deletions

diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 354821e7..7f0dde84 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,8 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

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

-var {:phase 2} b: int;

+var {:layer 2} b: int;

 

-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 == 0; b := 1; return true; }|;

 {

     var _old, curr: int;

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

 }

 

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

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

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

 

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

+procedure {:yields} {:layer 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} {:phase 0,2} Leave();

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

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