some clean up

4 files changed, 39 insertions, 61 deletions

diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
index e4380655..a3fbf231 100644
--- a/Test/og/Program2.bpl
+++ b/Test/og/Program2.bpl
@@ -2,6 +2,14 @@
 // RUN: %diff "%s.expect" "%t"

 var {:phase 1} x:int;

 

+procedure {:yields} {:phase 1} yield_x(n: int)

+requires {:phase 1} x >= n; 

+ensures {:phase 1} x >= n; 

+{

+    yield;

+    assert {:phase 1} x >= n;

+}

+

 procedure {:yields} {:phase 1} p() 

 requires {:phase 1} x >= 5; 

 ensures {:phase 1} x >= 8; 

@@ -27,11 +35,3 @@ ensures {:atomic}
 |{A:

   x := x + val; return true;

 }|;

-

-procedure {:yields} {:phase 1} yield_x(n: int)

-requires {:phase 1} x >= n; 

-ensures {:phase 1} x >= n; 

-{

-    yield;

-    assert {:phase 1} x >= n;

-}
\ No newline at end of file
diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
index e2c55c8e..0933afe8 100644
--- a/Test/og/Program3.bpl
+++ b/Test/og/Program3.bpl
@@ -2,6 +2,13 @@
 // RUN: %diff "%s.expect" "%t"

 var {:phase 1} x:int;

 

+procedure {:yields} {:phase 1} yield_x()

+ensures {:phase 1} x >= old(x); 

+{

+    yield;

+    assert {:phase 1} x >= old(x);

+}

+

 procedure {:yields} {:phase 1} p() 

 requires {:phase 1} x >= 5; 

 ensures {:phase 1} x >= 8; 

@@ -27,10 +34,3 @@ ensures {:atomic}
 |{A:

   x := x + val; return true;

 }|;

-

-procedure {:yields} {:phase 1} yield_x()

-ensures {:phase 1} x >= old(x); 

-{

-    yield;

-    assert {:phase 1} x >= old(x);

-}
\ No newline at end of file
diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index d189ee44..5005f77c 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,11 +13,9 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x

 }

 

-var {:linear "tid"} {:phase 1} alloc:[Tid]bool; 

 var {:phase 1} a:[Tid]int;

 

 procedure Allocate() returns ({:linear "tid"} tid:Tid); 

-modifies alloc; 

 

 procedure {:yields} {:phase 1} main() { 

     var {:linear "tid"} tid:Tid;

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 09ff8d4e..51d5fe3c 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -26,27 +26,6 @@ function {:inline} White(i:int) returns(bool) { i == 1 }
 function {:inline} Gray(i:int) returns(bool) { i == 2 }

 function {:inline} Black(i:int) returns(bool) { i >= 3 }

 

-procedure {:yields} {:phase 0,1} AcquireLock({:linear "tid"} tid: Tid);

-  ensures {:right} |{ A: assert tid != nil; 

-                         assume lock == nil; 

-                         lock := tid; 

-                         return true; }|;

-

-procedure {:yields} {:phase 0,1} ReleaseLock({:linear "tid"} tid: Tid);

-  ensures {:left} |{ A: assert tid != nil;

-                         assert lock == tid; 

-                         lock := nil; 

-                         return true; }|;

-

-procedure {:yields} {:phase 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

-  ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;

-

-procedure {:yields} {:phase 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

-  ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

-

-procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

-  ensures {:atomic} |{A: col := Color; return true;}|;

-

 procedure {:yields} {:phase 2} YieldColorOnlyGetsDarker()

 ensures {:phase 2} Color >= old(Color);

 {

@@ -54,44 +33,45 @@ ensures {:phase 2} Color >= old(Color);
   assert {:phase 2} Color >= old(Color);

 }

 

-

 procedure {:yields} {:phase 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

-ensures {:atomic} |{ A: assert tid != nil;

-                        goto B, C; 

-                     B: assume White(Color);

-                        Color := GRAY();

-                        return true; 

+ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

+                     B: assume White(Color); Color := GRAY(); return true; 

                      C: return true;}|;

 {

   var colorLocal:int;

-

   yield;

-

   call colorLocal := GetColorNoLock();

   call YieldColorOnlyGetsDarker();

-  if (White(colorLocal)) {

-       call MidWriteBarrier(tid);

-  }

-

+  if (White(colorLocal)) { call MidWriteBarrier(tid); }

   yield;

 }

 

 procedure {:yields} {:phase 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

-ensures {:atomic} |{ A: assert tid != nil;

-                        goto B, C; 

-                     B: assume White(Color);

-                        Color := GRAY();

-                        return true; 

-                     C: return true;}|;

+ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

+                     B: assume White(Color); Color := GRAY(); return true; 

+                     C: return true; }|;

 {

        var colorLocal:int;

-

        yield;

        call AcquireLock(tid);

        call colorLocal := GetColorLocked(tid);

-       if (White(colorLocal)) {

-           call SetColorLocked(tid, GRAY());

-       } 

+       if (White(colorLocal)) { call SetColorLocked(tid, GRAY()); } 

        call ReleaseLock(tid);

        yield;

-}
\ No newline at end of file
+}

+

+procedure {:yields} {:phase 0,1} AcquireLock({:linear "tid"} tid: Tid);

+  ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

+

+procedure {:yields} {:phase 0,1} ReleaseLock({:linear "tid"} tid: Tid);

+  ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;

+

+procedure {:yields} {:phase 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); 

+  ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;

+

+procedure {:yields} {:phase 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

+  ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

+

+procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

+  ensures {:atomic} |{A: col := Color; return true;}|;

+