diff options
Diffstat (limited to 'Test/og/multiset.bpl')
| -rw-r--r-- | Test/og/multiset.bpl | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 161171bf..5bb056f3 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -41,7 +41,7 @@ ensures {:left 0} |{ A: procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
-ensures {:both 0} |{ A:
+ensures {:both 0,1} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tidIn;
assert tidIn != nil && tidIn != done;
@@ -52,7 +52,7 @@ ensures {:both 0} |{ A: procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
-ensures {:both 0} |{ A:
+ensures {:both 0,1} |{ A:
assert x != null;
assert owner[j] == nil;
assert 0 <= j && j < max;
@@ -78,20 +78,6 @@ ensures {:left 0} |{ A: return true;
}|;
-
-
-
-procedure {:yields} getValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, valid_j:bool);
-ensures {:both 0} |{ A:
- assert 0 <= j && j < max;
- assert lock[j] == tidIn;
- assert tidIn != nil && tidIn != done;
- tidOut := tidIn;
- valid_j := valid[j];
- return true;
- }|;
-
-
procedure {:yields} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:both 0} |{ A:
assert 0 <= j && j < max;
|