diff options
author | qadeer <unknown> | 2014-11-14 22:18:15 -0800 |
---|---|---|
committer | qadeer <unknown> | 2014-11-14 22:18:15 -0800 |
commit | 72d74c23e9c5cc1903f2646af6a7d778cfde53f3 (patch) | |
tree | 42b738427237ff44692051f028fb92a427c3cd1b /Test/og/new1.bpl | |
parent | 0339351e985c455e7ecf290be54aa5361fe7ae8f (diff) |
renamed :phase to :layer
Diffstat (limited to 'Test/og/new1.bpl')
-rw-r--r-- | Test/og/new1.bpl | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index 537a5f4b..3faa9156 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t"
function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
-var {:phase 1} g:int;
+var {:layer 1} g:int;
function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
{
@@ -13,25 +13,25 @@ procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:l requires Permissions == mapconstbool(true);
ensures xls == mapconstbool(true);
-procedure {:yields} {:phase 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
-requires {:phase 1} permVar_in[0] && g == 0;
+procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
+requires {:layer 1} permVar_in[0] && g == 0;
{
var {:linear "Perm"} permVar_out: [int]bool;
permVar_out := permVar_in;
yield;
- assert {:phase 1} permVar_out[0];
- assert {:phase 1} g == 0;
+ assert {:layer 1} permVar_out[0];
+ assert {:layer 1} g == 0;
call IncrG();
yield;
- assert {:phase 1} permVar_out[0];
- assert {:phase 1} g == 1;
+ assert {:layer 1} permVar_out[0];
+ assert {:layer 1} g == 1;
}
-procedure {:yields} {:phase 1} Main({:linear_in "Perm"} Permissions: [int]bool)
-requires {:phase 0,1} Permissions == mapconstbool(true);
+procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)
+requires {:layer 0,1} Permissions == mapconstbool(true);
{
var {:linear "Perm"} permVar_out: [int]bool;
@@ -42,8 +42,8 @@ requires {:phase 0,1} Permissions == mapconstbool(true); yield;
}
-procedure {:yields} {:phase 0,1} SetG(val:int);
+procedure {:yields} {:layer 0,1} SetG(val:int);
ensures {:atomic} |{A: g := val; return true; }|;
-procedure {:yields} {:phase 0,1} IncrG();
+procedure {:yields} {:layer 0,1} IncrG();
ensures {:atomic} |{A: g := g + 1; return true; }|;
|