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-set.bpl | |
parent | b2ed78d44c2b79dd0ed070012ee0d310fb7a4ad0 (diff) |
handling old() in stable assertions
bug fix in linear
Diffstat (limited to 'Test/og/linear-set.bpl')
-rw-r--r-- | Test/og/linear-set.bpl | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl new file mode 100644 index 00000000..1a0cde42 --- /dev/null +++ b/Test/og/linear-set.bpl @@ -0,0 +1,68 @@ +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]bool;
+
+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]bool, {:linear "x"} xls': [X]bool)
+requires tidls' != None() && xls' == All();
+{
+ var {:linear "tid"} tidls: [X]bool;
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} lsChild: [X]bool;
+ 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 != None());
+ call {:async} thread(lsChild, xls1);
+ havoc lsChild;
+ assume (lsChild != None());
+ call {:async} thread(lsChild, xls2);
+}
+
+procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
+requires tidls' != None() && xls' != None();
+{
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} tidls: [X]bool;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ assume l == None();
+ l := tidls;
+ assert {:yield} tidls != None() && xls != None();
+ x := 0;
+ assert {:yield} tidls != None() && xls != None();
+ assert x == 0;
+ assert {:yield} tidls != None() && xls != None();
+ l := None();
+}
|