diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/civl/linear-set.bpl | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/civl/linear-set.bpl')
-rw-r--r-- | Test/civl/linear-set.bpl | 210 |
1 files changed, 105 insertions, 105 deletions
diff --git a/Test/civl/linear-set.bpl b/Test/civl/linear-set.bpl index e481291a..de7f72f4 100644 --- a/Test/civl/linear-set.bpl +++ b/Test/civl/linear-set.bpl @@ -1,105 +1,105 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type X;
-function {:builtin "MapConst"} MapConstInt(int) : [X]int;
-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
-
-function {:inline} None() : [X]bool
-{
- MapConstBool(false)
-}
-
-function {:inline} All() : [X]bool
-{
- MapConstBool(true)
-}
-
-function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
-{
- xs
-}
-
-var {:layer 0,1} x: int;
-var {:layer 0,1} l: [X]bool;
-
-
-procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)
-ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
-{
- yield;
- call xls1, xls2 := SplitLow(xls);
- yield;
-}
-
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool)
-{
- yield;
- call xls := AllocateLow();
- yield;
-}
-
-procedure {:yields} {:layer 0,1} Set(v: int);
-ensures {:atomic} |{A: x := v; return true; }|;
-
-procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool);
-ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;
-
-procedure {:yields} {:layer 0,1} Unlock();
-ensures {:atomic} |{A: l := None(); return true; }|;
-
-procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
-ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;
-
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool);
-ensures {:atomic} |{ A: return true; }|;
-
-procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
-requires {:layer 1} tidls' != None() && xls' == All();
-{
- var {:linear "tid"} tidls: [X]bool;
- var {:linear "x"} xls: [X]bool;
- var {:linear "tid"} lsChild: [X]bool;
- var {:linear "x"} xls1: [X]bool;
- var {:linear "x"} xls2: [X]bool;
-
- tidls := tidls';
- xls := xls';
- yield;
- call Set(42);
- yield;
- assert {:layer 1} xls == All();
- assert {:layer 1} x == 42;
- call xls1, xls2 := Split(xls);
- call lsChild := Allocate();
- assume (lsChild != None());
- yield;
- async call thread(lsChild, xls1);
- call lsChild := Allocate();
- assume (lsChild != None());
- yield;
- async call thread(lsChild, xls2);
- yield;
-}
-
-procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
-requires {:layer 1} tidls' != None() && xls' != None();
-{
- var {:linear "x"} xls: [X]bool;
- var {:linear "tid"} tidls: [X]bool;
-
- tidls := tidls';
- xls := xls';
-
- yield;
- call Lock(tidls);
- yield;
- assert {:layer 1} tidls != None() && xls != None();
- call Set(0);
- yield;
- assert {:layer 1} tidls != None() && xls != None();
- assert {:layer 1} x == 0;
- assert {:layer 1} tidls != None() && xls != None();
- call Unlock();
- yield;
-}
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstInt(int) : [X]int; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} None() : [X]bool +{ + MapConstBool(false) +} + +function {:inline} All() : [X]bool +{ + MapConstBool(true) +} + +function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var {:layer 0,1} x: int; +var {:layer 0,1} l: [X]bool; + + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool) +{ + yield; + call xls := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} |{A: x := v; return true; }|; + +procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool); +ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := None(); return true; }|; + +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' == All(); +{ + var {:linear "tid"} tidls: [X]bool; + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} lsChild: [X]bool; + var {:linear "x"} xls1: [X]bool; + var {:linear "x"} xls2: [X]bool; + + tidls := tidls'; + xls := xls'; + yield; + call Set(42); + yield; + assert {:layer 1} xls == All(); + assert {:layer 1} x == 42; + call xls1, xls2 := Split(xls); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls1); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls2); + yield; +} + +procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' != None(); +{ + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} tidls: [X]bool; + + tidls := tidls'; + xls := xls'; + + yield; + call Lock(tidls); + yield; + assert {:layer 1} tidls != None() && xls != None(); + call Set(0); + yield; + assert {:layer 1} tidls != None() && xls != None(); + assert {:layer 1} x == 0; + assert {:layer 1} tidls != None() && xls != None(); + call Unlock(); + yield; +} |