diff options
author | qadeer <unknown> | 2013-12-11 14:01:40 -0800 |
---|---|---|
committer | qadeer <unknown> | 2013-12-11 14:01:40 -0800 |
commit | 42b80a61e83e8d569700340ee9ad8f8aa3a270a8 (patch) | |
tree | c1d45493a0e3c645a7d30060a5c6053ca2141714 /Test | |
parent | 614648876bd81d6683a9d94207bb514a615202fb (diff) |
fixes to type checking code
Diffstat (limited to 'Test')
-rw-r--r-- | Test/og/lock.bpl | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 0b250b6d..4e4e6dec 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -23,7 +23,7 @@ procedure {:yields} {:stable} Customer() }
procedure {:yields} Enter()
-ensures {:atomic 0} |{ A: assume !b; b := true; return true; }|;
+ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
{
var status: bool;
L:
@@ -41,12 +41,12 @@ ensures {:atomic 0} |{ A: assume !b; b := true; return true; }|; goto L;
}
-procedure CAS(prev: bool, next: bool) returns (status: bool);
-ensures {:atomic -1} |{
+procedure {:yields} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic 0} |{
A: goto B, C;
B: assume b == prev; b := next; status := true; return true;
C: status := false; return true;
}|;
procedure {:yields} Leave();
-ensures {:atomic -1} |{ A: b := false; return true; }|;
+ensures {:atomic 0} |{ A: b := false; return true; }|;
|