checkpoint

1 files changed, 31 insertions, 12 deletions

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 920fc32c..22751d29 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,36 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

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

-modifies g;

+procedure {:yields} {:phase 1} PB()

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == old(g);

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

+procedure {:yields} {:phase 1} PC()

+ensures {:phase 1} g == old(g);

 {

   yield;

-  assert g == old(g);

+  assert {:phase 1} g == old(g);

 }

 

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

+procedure {:yields} {:phase 1} PE()

 {

   call PC();

 }

 

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

+procedure {:yields} {:phase 1} PD()

 {

-  g := 3;

+  yield;

+  call Set(3);

   call PC();

-  assert g == 3;

+  assert {:phase 1} g == 3;

 }

 

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

+procedure {:yields} {:phase 1} Main2()

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }