renamed og to civl

1 files changed, 57 insertions, 0 deletions

diff --git a/Test/civl/bar.bpl b/Test/civl/bar.bpl
new file mode 100644
index 00000000..4eef8378
--- /dev/null
+++ b/Test/civl/bar.bpl
@@ -0,0 +1,57 @@
+// RUN: %boogie -noinfer "%s" > "%t"

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

+var {:layer 0,1} g:int;

+

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

+{

+  yield;

+  call Incr();

+  yield;

+}

+

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

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

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

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

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

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

+{

+  yield;

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

+}

+

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

+{

+  call PC();

+}

+

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

+{

+  yield;

+  call Set(3);

+  call PC();

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

+}

+

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

+{

+  yield;

+  while (*)

+  {

+    async call PB();

+    yield;

+    async call PE();

+    yield;

+    async call PD();

+    yield;

+  }

+  yield;

+}