diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-30 12:43:15 -0800 |
| commit | 06055fdd22eeb9015d215e71996e4714c183ef19 (patch) | |
| tree | bdd9aa1ee6667426903f7721abc8d84f1873da83 /Test/og/linear-set2.bpl | |
| parent | b2ed78d44c2b79dd0ed070012ee0d310fb7a4ad0 (diff) | |
handling old() in stable assertions
bug fix in linear
Diffstat (limited to 'Test/og/linear-set2.bpl')
| -rw-r--r-- | Test/og/linear-set2.bpl | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl new file mode 100644 index 00000000..a91100b6 --- /dev/null +++ b/Test/og/linear-set2.bpl @@ -0,0 +1,69 @@ +function {:inline} Subset(a: [X]bool, b: [X]bool) : bool
+{
+ MapImp(a, b) == MapConstBool(true)
+}
+
+function {:inline} In(a: X, b: [X]bool) : bool
+{
+ b[a]
+}
+
+function {:inline} None() : [X]bool
+{
+ MapConstBool(false)
+}
+
+function {:inline} All() : [X]bool
+{
+ MapConstBool(true)
+}
+
+var x: int;
+var l: X;
+const nil: X;
+
+procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+
+procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires tidls' != nil && xls' == All();
+{
+ var {:linear "tid"} tidls: X;
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} lsChild: X;
+ var {:linear "x"} xls1: [X]bool;
+ var {:linear "x"} xls2: [X]bool;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ x := 42;
+ assert {:yield} xls == All();
+ assert x == 42;
+ call xls1, xls2 := Split(xls);
+ havoc lsChild;
+ assume (lsChild != nil);
+ call {:async} thread(lsChild, xls1);
+ havoc lsChild;
+ assume (lsChild != nil);
+ call {:async} thread(lsChild, xls2);
+}
+
+procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires tidls' != nil && xls' != None();
+{
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} tidls: X;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ assume l == nil;
+ l := tidls;
+ assert {:yield} tidls != nil && xls != None();
+ x := 0;
+ assert {:yield} tidls != nil && xls != None();
+ assert x == 0;
+ assert {:yield} tidls != nil && xls != None();
+ l := nil;
+}
|