diff options
author | 2013-08-07 16:57:02 -0700 | |
---|---|---|
committer | 2013-08-07 16:57:02 -0700 | |
commit | 2fd1db9218ebc55ad0f26c5f3faddcdf4eef2c85 (patch) | |
tree | ee58fbfdd972b0bdf5b5883e6c894da623fc1a60 /Test/og/linear-set2.bpl | |
parent | a9c60110139c15ec65c50360763c75014b9eef82 (diff) |
cleaned up the OG code
enabled it to be always on
Diffstat (limited to 'Test/og/linear-set2.bpl')
-rw-r--r-- | Test/og/linear-set2.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index ac4a2e21..565cc82b 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -23,7 +23,7 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); procedure Allocate() returns ({:linear "tid"} xls: X);
ensures xls != nil;
-procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
requires tidls' != nil && xls' == All();
{
var {:linear "tid"} tidls: X;
@@ -46,7 +46,7 @@ requires tidls' != nil && xls' == All(); async call thread(lsChild, xls2);
}
-procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
requires tidls' != nil && xls' != None();
{
var {:linear "x"} xls: [X]bool;
|