diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
| commit | 47d88acd5e49ea9f68dd93bc2eb8dca85036b7ca (patch) | |
| tree | ae9fe1fd8987d740c38c4989aa91957257d60d3b /Test/og/t1.bpl | |
| parent | 4024e730fe78f4f210b497041ca083b1464426b5 (diff) | |
fixed bug reported by Akash
Diffstat (limited to 'Test/og/t1.bpl')
| -rw-r--r-- | Test/og/t1.bpl | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl new file mode 100644 index 00000000..01451ac9 --- /dev/null +++ b/Test/og/t1.bpl @@ -0,0 +1,58 @@ +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 x == mapconstbool(true);
+ assert g == 0;
+
+ yield;
+ assume tid_child != 0;
+ async call B(tid_child, x);
+
+ yield;
+ assert x == mapconstbool(true);
+ assert g == 0;
+
+ 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;
+}
|