From 72d74c23e9c5cc1903f2646af6a7d778cfde53f3 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 14 Nov 2014 22:18:15 -0800
Subject: renamed :phase to :layer

---
 Test/og/perm.bpl | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'Test/og/perm.bpl')

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 4df74778..66ae5285 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:phase 1} x: int;
+var {:layer 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;
@@ -14,10 +14,10 @@ procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xl
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
 
 
-procedure {:yields} {:phase 1} mainE({:linear_in "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;
+procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
+   free requires {:layer 1} permVar_in == ch_mapconstbool(true);
+   free requires {:layer 1} permVar_in[0];
+   free requires {:layer 1} x == 0;
 {
     var {:linear "Perm"} permVar_out: [int]bool;
     var {:linear "Perm"} permVarOut2: [int]bool;
@@ -25,33 +25,33 @@ procedure {:yields} {:phase 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
     permVar_out := permVar_in;
 
     yield;
-    assert {:phase 1} x == 0;
-    assert {:phase 1} permVar_out[0];
-    assert {:phase 1} permVar_out == ch_mapconstbool(true);
+    assert {:layer 1} x == 0;
+    assert {:layer 1} permVar_out[0];
+    assert {:layer 1} permVar_out == ch_mapconstbool(true);
 
     call permVar_out, permVarOut2 := Split(permVar_out);
     async call foo(permVarOut2);
     yield;
 }
 
-procedure {:yields} {:phase 1} foo({:linear_in "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;
+procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 
+  free requires {:layer 1} permVar_in != ch_mapconstbool(false);
+  free requires {:layer 1} permVar_in[1];
+  requires {:layer 1} x == 0;
 {
   var {:linear "Perm"} permVar_out: [int]bool;
   permVar_out := permVar_in;
   
   yield;
-  assert {:phase 1} permVar_out[1];
-  assert {:phase 1} x == 0;
+  assert {:layer 1} permVar_out[1];
+  assert {:layer 1} x == 0;
 
   call Incr();
 
   yield;
-  assert {:phase 1} permVar_out[1];
-  assert {:phase 1} x == 1;
+  assert {:layer 1} permVar_out[1];
+  assert {:layer 1} x == 1;
 }
 
-procedure {:yields} {:phase 0,1} Incr();
+procedure {:yields} {:layer 0,1} Incr();
 ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file
-- 
cgit v1.2.3