diff options
Diffstat (limited to 'Test/civl/perm.bpl')
-rw-r--r-- | Test/civl/perm.bpl | 96 |
1 files changed, 48 insertions, 48 deletions
diff --git a/Test/civl/perm.bpl b/Test/civl/perm.bpl index 5bc75324..5d6e0d21 100644 --- a/Test/civl/perm.bpl +++ b/Test/civl/perm.bpl @@ -1,49 +1,49 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var {:layer 0,1} x: int;
-function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
-
-function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;
-
-function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
-{
- x
-}
-
-procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
- requires {:layer 1} permVar_in == ch_mapconstbool(true);
- requires {:layer 1} x == 0;
-{
- var {:linear "Perm"} permVar_out: [int]bool;
-
- permVar_out := permVar_in;
-
- yield;
- assert {:layer 1} x == 0;
- assert {:layer 1} permVar_out == ch_mapconstbool(true);
-
- async call foo(permVar_out);
- yield;
-}
-
-procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool)
- requires {:layer 1} permVar_in != ch_mapconstbool(false);
- requires {:layer 1} permVar_in[1];
- requires {:layer 1} x == 0;
-{
- var {:linear "Perm"} permVar_out: [int]bool;
- permVar_out := permVar_in;
-
- yield;
- assert {:layer 1} permVar_out[1];
- assert {:layer 1} x == 0;
-
- call Incr();
-
- yield;
- assert {:layer 1} permVar_out[1];
- assert {:layer 1} x == 1;
-}
-
-procedure {:yields} {:layer 0,1} Incr();
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x: int; +function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool; + +function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool; + +function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool +{ + x +} + +procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in == ch_mapconstbool(true); + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + + permVar_out := permVar_in; + + yield; + assert {:layer 1} x == 0; + assert {:layer 1} permVar_out == ch_mapconstbool(true); + + async call foo(permVar_out); + yield; +} + +procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in != ch_mapconstbool(false); + requires {:layer 1} permVar_in[1]; + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 0; + + call Incr(); + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 1; +} + +procedure {:yields} {:layer 0,1} Incr(); ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file |