diff options
Diffstat (limited to 'Test/civl/parallel5.bpl')
-rw-r--r-- | Test/civl/parallel5.bpl | 118 |
1 files changed, 59 insertions, 59 deletions
diff --git a/Test/civl/parallel5.bpl b/Test/civl/parallel5.bpl index 87afc888..6d3deb8e 100644 --- a/Test/civl/parallel5.bpl +++ b/Test/civl/parallel5.bpl @@ -1,59 +1,59 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var {:layer 0,1} a:[int]int;
-
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
-{
- yield;
- call tid := AllocateLow();
- yield;
-}
-
-function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
-function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
-{
- MapConstBool(false)[x := true]
-}
-
-procedure {:yields} {:layer 0,1} Write(idx: int, val: int);
-ensures {:atomic} |{A: a[idx] := val; return true; }|;
-
-procedure {:yields} {:layer 1} main()
-{
- var {:linear "tid"} i: int;
- var {:linear "tid"} j: int;
- call i := Allocate();
- call j := Allocate();
- par i := t(i) | Yield(j);
- par i := u(i) | j := u(j);
-}
-
-procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
-{
- i := i';
-
- yield;
- call Write(i, 42);
- call Yield(i);
- assert {:layer 1} a[i] == 42;
-}
-
-procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
-{
- i := i';
-
- yield;
- call Write(i, 42);
- yield;
- assert {:layer 1} a[i] == 42;
-}
-
-procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int)
-ensures {:layer 1} old(a)[i] == a[i];
-{
- yield;
- assert {:layer 1} old(a)[i] == a[i];
-}
-
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
-ensures {:atomic} |{ A: return true; }|;
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:[int]int; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 0,1} Write(idx: int, val: int); +ensures {:atomic} |{A: a[idx] := val; return true; }|; + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | Yield(j); + par i := u(i) | j := u(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + call Yield(i); + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + yield; + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) +ensures {:layer 1} old(a)[i] == a[i]; +{ + yield; + assert {:layer 1} old(a)[i] == a[i]; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; |