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/civl/FlanaganQadeer.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/civl/FlanaganQadeer.bpl')
-rw-r--r-- | Test/civl/FlanaganQadeer.bpl | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/Test/civl/FlanaganQadeer.bpl b/Test/civl/FlanaganQadeer.bpl new file mode 100644 index 00000000..97df7ce2 --- /dev/null +++ b/Test/civl/FlanaganQadeer.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; +var {:layer 0,1} l: X; +var {:layer 0,1} x: int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} tid: X; + var val: int; + + yield; + while (*) + { + call tid := Allocate(); + havoc val; + async call foo(tid, val); + yield; + } + yield; +} +procedure {:yields} {:layer 0,1} Lock(tid: X); +ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := nil; return true; }|; + +procedure {:yields} {:layer 0,1} Set(val: int); +ensures {:atomic} |{A: x := val; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; + +procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int) +requires {:layer 1} tid' != nil; +{ + var {:linear "tid"} tid: X; + tid := tid'; + + yield; + call Lock(tid); + call tid := Yield(tid); + call Set(val); + call tid := Yield(tid); + assert {:layer 1} x == val; + call tid := Yield(tid); + call Unlock(); + yield; +} + +procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X) +requires {:layer 1} tid' != nil; +ensures {:layer 1} tid == tid'; +ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x; +{ + tid := tid'; + yield; + assert {:layer 1} tid != nil; + assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x); +}
\ No newline at end of file |