diff options
Diffstat (limited to 'Test/civl/Program4.bpl')
-rw-r--r-- | Test/civl/Program4.bpl | 136 |
1 files changed, 68 insertions, 68 deletions
diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index 7f2f9c44..68c2a5f3 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -1,68 +1,68 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type Tid;
-var {:layer 0,1} a:[Tid]int;
-
-procedure {:yields} {:layer 1} main() {
- var {:linear "tid"} tid:Tid;
-
- yield;
- while (true) {
- call tid := Allocate();
- async call P(tid);
- yield;
- }
- yield;
-}
-
-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid)
-ensures {:layer 1} a[tid] == old(a)[tid] + 1;
-{
- var t:int;
-
- yield;
- assert {:layer 1} a[tid] == old(a)[tid];
- call t := Read(tid);
- yield;
- assert {:layer 1} a[tid] == t;
- call Write(tid, t + 1);
- yield;
- assert {:layer 1} a[tid] == t + 1;
-}
-
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
-{
- yield;
- call tid := AllocateLow();
- yield;
-}
-
-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
-ensures {:atomic}
-|{A:
- val := a[tid]; return true;
-}|;
-
-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
-ensures {:atomic}
-|{A:
- a[tid] := val; return true;
-}|;
-
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
-ensures {:atomic} |{ A: return true; }|;
-
-
-
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
-
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
-{
- MapConstBool(false)[x := true]
-}
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
-{
- x
-}
-
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +var {:layer 0,1} a:[Tid]int; + +procedure {:yields} {:layer 1} main() { + var {:linear "tid"} tid:Tid; + + yield; + while (true) { + call tid := Allocate(); + async call P(tid); + yield; + } + yield; +} + +procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) +ensures {:layer 1} a[tid] == old(a)[tid] + 1; +{ + var t:int; + + yield; + assert {:layer 1} a[tid] == old(a)[tid]; + call t := Read(tid); + yield; + assert {:layer 1} a[tid] == t; + call Write(tid, t + 1); + yield; + assert {:layer 1} a[tid] == t + 1; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +{ + yield; + call tid := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); +ensures {:atomic} +|{A: + val := a[tid]; return true; +}|; + +procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); +ensures {:atomic} +|{A: + a[tid] := val; return true; +}|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); +ensures {:atomic} |{ A: return true; }|; + + + +function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; +function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; + +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +{ + x +} + |