From 882a965c3d212a2d79825e0d06200758ce3b9db4 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 11 Feb 2015 17:29:22 -0800
Subject: moved some things around

---
 Test/og/Program4.bpl | 41 ++++++++++++++++++++++-------------------
 Test/og/Program5.bpl | 36 +++++++++++++++++++-----------------
 2 files changed, 41 insertions(+), 36 deletions(-)

(limited to 'Test')

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 7767e179..7f2f9c44 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -1,27 +1,8 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 type Tid; 
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
-
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
-{
-  MapConstBool(false)[x := true]
-}
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
-{
-  x
-}
-
 var {:layer 0,1} a:[Tid]int;
 
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
-{
-    yield;
-    call tid := AllocateLow();
-    yield;
-}
-
 procedure {:yields} {:layer 1} main() { 
     var {:linear "tid"} tid:Tid;
 
@@ -49,6 +30,13 @@ ensures {:layer 1} a[tid] == old(a)[tid] + 1;
     assert {:layer 1} a[tid] == t + 1; 
 }
 
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+{
+    yield;
+    call tid := AllocateLow();
+    yield;
+}
+
 procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
 ensures {:atomic}
 |{A:
@@ -63,3 +51,18 @@ ensures {:atomic}
 
 procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
 ensures {:atomic} |{ A: return true; }|;
+
+
+
+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+
+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+{
+  x
+}
+
diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 55e4219f..7ede3124 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -2,20 +2,6 @@
 // RUN: %diff "%s.expect" "%t"
 type Tid;
 const unique nil: Tid;
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
-
-var {:layer 0} Color:int;
-var {:layer 0} lock:Tid;
-
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
-{
-  MapConstBool(false)[x := true]
-}
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
-{
-  x
-}
 
 function {:inline} UNALLOC():int { 0 }
 function {:inline} WHITE():int { 1 }
@@ -33,7 +19,7 @@ ensures {:layer 2} Color >= old(Color);
   assert {:layer 2} Color >= old(Color);
 }
 
-procedure {:yields} {:layer 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)
+procedure {:yields} {:layer 2,3} WriteBarrier({:linear "tid"} tid:Tid)
 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 
                      B: assume White(Color); Color := GRAY(); return true; 
                      C: return true;}|;
@@ -42,11 +28,11 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
   yield;
   call colorLocal := GetColorNoLock();
   call YieldColorOnlyGetsDarker();
-  if (White(colorLocal)) { call MidWriteBarrier(tid); }
+  if (White(colorLocal)) { call WriteBarrierSlow(tid); }
   yield;
 }
 
-procedure {:yields} {:layer 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)
+procedure {:yields} {:layer 1,2} WriteBarrierSlow({:linear "tid"} tid:Tid)
 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 
                      B: assume White(Color); Color := GRAY(); return true; 
                      C: return true; }|;
@@ -75,3 +61,19 @@ procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns
 procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int);
   ensures {:atomic} |{A: col := Color; return true;}|;
 
+
+
+function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
+function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+
+var {:layer 0} Color:int;
+var {:layer 0} lock:Tid;
+
+function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+{
+  MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+{
+  x
+}
-- 
cgit v1.2.3