renamed :phase to :layer

1 files changed, 16 insertions, 16 deletions

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 1e98fa6d..9eb11495 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"

 type X;

 const nil: X;

-var {:phase 1} l: X;

-var {:phase 1} x: int;

+var {:layer 1} l: X;

+var {:layer 1} x: int;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -12,9 +12,9 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
 }

 

 procedure Allocate() returns ({:linear "tid"} xls: X);

-ensures {:phase 1} xls != nil;

+ensures {:layer 1} xls != nil;

 

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

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

 {

     var {:linear "tid"} tid: X;

     var val: int;

@@ -29,17 +29,17 @@ procedure {:yields} {:phase 1} main()
     }

     yield;

 }

-procedure {:yields} {:phase 0,1} Lock(tid: X);

+procedure {:yields} {:layer 0,1} Lock(tid: X);

 ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|;

 

-procedure {:yields} {:phase 0,1} Unlock();

+procedure {:yields} {:layer 0,1} Unlock();

 ensures {:atomic} |{A: l := nil; return true; }|;

 

-procedure {:yields} {:phase 0,1} Set(val: int);

+procedure {:yields} {:layer 0,1} Set(val: int);

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

 

-procedure {:yields} {:phase 1} foo({:linear_in "tid"} tid': X, val: int)

-requires {:phase 1} tid' != nil;

+procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)

+requires {:layer 1} tid' != nil;

 {

     var {:linear "tid"} tid: X;

     tid := tid';

@@ -49,19 +49,19 @@ requires {:phase 1} tid' != nil;
     call tid := Yield(tid);

     call Set(val);

     call tid := Yield(tid);

-    assert {:phase 1} x == val;

+    assert {:layer 1} x == val;

     call tid := Yield(tid);

     call Unlock();

     yield;

 }

 

-procedure {:yields} {:phase 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

-requires {:phase 1} tid' != nil;

-ensures {:phase 1} tid == tid';

-ensures {:phase 1} old(l) == tid ==> old(l) == l && old(x) == x;

+procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)

+requires {:layer 1} tid' != nil;

+ensures {:layer 1} tid == tid';

+ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x;

 {

     tid := tid';

     yield;

-    assert {:phase 1} tid != nil;

-    assert {:phase 1} (old(l) == tid ==> old(l) == l && old(x) == x);

+    assert {:layer 1} tid != nil;

+    assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x);

 }
\ No newline at end of file