From 69f00af6f384f422d0ccafece7cffc98dc5cbefa Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 20 May 2015 12:16:36 -0700
Subject: added more specifications

---
 Test/civl/Program5.bpl | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'Test/civl')

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;
-- 
cgit v1.2.3