diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/linear/list.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/linear/list.bpl')
-rw-r--r-- | Test/linear/list.bpl | 100 |
1 files changed, 50 insertions, 50 deletions
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl index 804cb7e2..e4fa23f6 100644 --- a/Test/linear/list.bpl +++ b/Test/linear/list.bpl @@ -1,50 +1,50 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type X;
-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
-
-function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool
-{
- xs
-}
-
-var head: X;
-var tail: X;
-var {:linear "Mem"} D: [X]bool;
-var Next:[X]X;
-const nil: X;
-
-procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
-ensures M == MapConstBool(false)[x := true];
-
-procedure Join({:linear_in "Mem"} A: [X]bool);
-modifies D;
-ensures MapOr(old(D), A) == D;
-
-procedure one()
-requires D[head] && D[tail];
-requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
-ensures D[head] && D[tail];
-ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
-ensures head != tail;
-{
- var x: X;
- var {:linear "Mem"} M: [X]bool;
-
- call x, M := malloc();
- call Join(M);
- Next[tail] := x;
- tail := x;
- Next[tail] := nil;
-}
-
-procedure two()
-requires head != tail;
-requires D[head] && D[tail];
-requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
-ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
-ensures D[head] && D[tail];
-{
- head := Next[head];
-}
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var head: X; +var tail: X; +var {:linear "Mem"} D: [X]bool; +var Next:[X]X; +const nil: X; + +procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool); +ensures M == MapConstBool(false)[x := true]; + +procedure Join({:linear_in "Mem"} A: [X]bool); +modifies D; +ensures MapOr(old(D), A) == D; + +procedure one() +requires D[head] && D[tail]; +requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail); +ensures D[head] && D[tail]; +ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail); +ensures head != tail; +{ + var x: X; + var {:linear "Mem"} M: [X]bool; + + call x, M := malloc(); + call Join(M); + Next[tail] := x; + tail := x; + Next[tail] := nil; +} + +procedure two() +requires head != tail; +requires D[head] && D[tail]; +requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail); +ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail); +ensures D[head] && D[tail]; +{ + head := Next[head]; +} |