diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-04-30 20:53:02 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-04-30 20:53:02 -0700 |
| commit | 4024e730fe78f4f210b497041ca083b1464426b5 (patch) | |
| tree | 023cb8a9a572fefe9f1c18a11a22c66a1de4549f | |
| parent | 77aeb920de2c3cd22a1296700305539f28f6761c (diff) | |
add another test file
| -rw-r--r-- | Test/og/akash.bpl | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl new file mode 100644 index 00000000..dca4f5f7 --- /dev/null +++ b/Test/og/akash.bpl @@ -0,0 +1,53 @@ +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+
+var g: int;
+var h: int;
+
+procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
+{
+ var {:linear "1"} x: [int]bool;
+ var {:linear "2"} y: [int]bool;
+ var {:linear "tid"} tid_child: int;
+ assume tid_in == tid_out;
+ assume x == mapconstbool(true);
+ assume y == mapconstbool(true);
+
+ g := 0;
+ yield;
+ assert g == 0 && x == mapconstbool(true);
+
+ yield;
+ assume tid_child != 0;
+ async call B(tid_child, x);
+
+ yield;
+ h := 0;
+
+ yield;
+ assert h == 0 && y == mapconstbool(true);
+
+ yield;
+ async call C(tid_child, y);
+}
+
+procedure B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool)
+requires x_in != mapconstbool(false);
+{
+ var {:linear "tid"} tid_out: int;
+ var {:linear "1"} x: [int]bool;
+ assume tid_in == tid_out;
+ assume x_in == x;
+
+ g := 1;
+}
+
+procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool)
+requires y_in != mapconstbool(false);
+{
+ var {:linear "tid"} tid_out: int;
+ var {:linear "2"} y: [int]bool;
+ assume tid_in == tid_out;
+ assume y_in == y;
+
+ h := 1;
+}
\ No newline at end of file |