renamed og to civl

1 files changed, 46 insertions, 0 deletions

diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl
new file mode 100644
index 00000000..74d16acf
--- /dev/null
+++ b/Test/civl/ghost.bpl
@@ -0,0 +1,46 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var {:layer 0} x: int;
+
+procedure {:yields} {:layer 0,1} Incr();
+ensures {:right} |{ A: x := x + 1; return true; }|;
+
+procedure ghost(y: int) returns (z: int)
+requires y == 1;
+ensures z == 2;
+{
+  z := y + 1;
+}
+
+procedure {:yields} {:layer 1,2} Incr2() 
+ensures {:right} |{ A: x := x + 2; return true; }|;
+{
+  var {:ghost} a: int;
+  var {:ghost} b: int;
+
+  yield;
+  call a := ghost(1);
+  assert {:layer 1} a == 2;
+  par Incr() | Incr();
+  yield;
+}
+
+procedure ghost_0() returns (z: int)
+ensures z == x;
+{
+  z := x;
+}
+
+procedure {:yields} {:layer 1,2} Incr2_0() 
+ensures {:right} |{ A: x := x + 2; return true; }|;
+{
+  var {:ghost} a: int;
+  var {:ghost} b: int;
+
+  yield;
+  call a := ghost_0();
+  par Incr() | Incr();
+  call b := ghost_0();
+  assert {:layer 1} b == a + 2;
+  yield;
+}