diff options
author | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
---|---|---|
committer | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
commit | 36e016acf963b7c19d59640b11b4a40f2072943e (patch) | |
tree | 31a45e868059d0ffe54fc3d212261245ff97886a /Test/og/perm.bpl | |
parent | 121071b9f87d23eaeba176897b9655cd540fb694 (diff) |
checkpoint
Diffstat (limited to 'Test/og/perm.bpl')
-rw-r--r-- | Test/og/perm.bpl | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl index 8b77ce1b..6d07ca75 100644 --- a/Test/og/perm.bpl +++ b/Test/og/perm.bpl @@ -1,4 +1,4 @@ -var x: int;
+var {:phase 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;
@@ -12,44 +12,44 @@ procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
-procedure {:entrypoint} {:yields} mainE({:linear "Perm"} permVar_in: [int]bool)
- free requires permVar_in == ch_mapconstbool(true);
- free requires permVar_in[0];
- modifies x;
+procedure {:yields} {:phase 1} mainE({:linear "Perm"} permVar_in: [int]bool)
+ free requires {:phase 1} permVar_in == ch_mapconstbool(true);
+ free requires {:phase 1} permVar_in[0];
+ free requires {:phase 1} x == 0;
{
var {:linear "Perm"} permVar_out: [int]bool;
var {:linear "Perm"} permVarOut2: [int]bool;
permVar_out := permVar_in;
- assume x == 0;
-
yield;
- assert x == 0;
- assert permVar_out[0];
- assert permVar_out == ch_mapconstbool(true);
+ assert {:phase 1} x == 0;
+ assert {:phase 1} permVar_out[0];
+ assert {:phase 1} permVar_out == ch_mapconstbool(true);
call permVar_out, permVarOut2 := Split(permVar_out);
async call foo(permVarOut2);
+ yield;
}
-procedure {:yields} {:stable} foo({:linear "Perm"} permVar_in: [int]bool)
- free requires permVar_in != ch_mapconstbool(false);
- free requires permVar_in[1];
- requires x == 0;
- modifies x;
+procedure {:yields} {:phase 1} foo({:linear "Perm"} permVar_in: [int]bool)
+ free requires {:phase 1} permVar_in != ch_mapconstbool(false);
+ free requires {:phase 1} permVar_in[1];
+ requires {:phase 1} x == 0;
{
var {:linear "Perm"} permVar_out: [int]bool;
permVar_out := permVar_in;
yield;
- assert permVar_out[1];
- assert x == 0;
+ assert {:phase 1} permVar_out[1];
+ assert {:phase 1} x == 0;
- x := x + 1;
+ call Incr();
yield;
- assert permVar_out[1];
- assert x == 1;
+ assert {:phase 1} permVar_out[1];
+ assert {:phase 1} x == 1;
}
+procedure {:yields} {:phase 0,1} Incr();
+ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file |