some clean up

1 files changed, 24 insertions, 44 deletions

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;}|;

+