added more specifications

1 files changed, 6 insertions, 2 deletions

diff --git a/Test/civl/Program5.bpl b/Test/civl/Program5.bpl
index 7ede3124..d728b845 100644
--- a/Test/civl/Program5.bpl
+++ b/Test/civl/Program5.bpl
@@ -22,20 +22,24 @@ ensures {:layer 2} Color >= old(Color);
 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;}|;

+                     C: assume !White(Color); return true;}|;

+requires {:layer 2} Color >= WHITE();

+ensures {:layer 2} Color >= GRAY();

 {

   var colorLocal:int;

   yield;

+  assert {:layer 2} Color >= WHITE();

   call colorLocal := GetColorNoLock();

   call YieldColorOnlyGetsDarker();

   if (White(colorLocal)) { call WriteBarrierSlow(tid); }

   yield;

+  assert {:layer 2} Color >= GRAY();

 }

 

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

+                     C: assume !White(Color); return true; }|;

 {

        var colorLocal:int;

        yield;