diff options
| -rw-r--r-- | Test/civl/treiber-stack.bpl | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index e1c509ab..286c7dd1 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -82,15 +82,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret assert {:expand} {:layer 1} Inv(TopOfStack, Stack);
}
-procedure {:yields} {:layer 1} pop()
+procedure {:yields} {:layer 1} pop() returns (t: Node)
requires {:layer 1} Inv(TopOfStack, Stack);
ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ var t: Node;
- A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
+ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
{
var g: bool;
var x: Node;
- var t: Node;
yield;
assert {:layer 1} Inv(TopOfStack, Stack);
|