summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2015-05-27 16:05:37 -0700
committerGravatar qadeer <qadeer@microsoft.com>2015-05-27 16:05:37 -0700
commit7e286186df1932c299c1acb3a62310d4bfd36172 (patch)
treefdde0114e12210d856b79499b94b9f1817723662 /Test
parent53cd63deeb418ce49c7c26f7613cb83e8e77e919 (diff)
bug fix in pop
Diffstat (limited to 'Test')
-rw-r--r--Test/civl/treiber-stack.bpl6
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);