From fc8b7c37c9778fb66efca51cb8e3d2990f218e91 Mon Sep 17 00:00:00 2001
From: stasiran <unknown>
Date: Thu, 16 Jan 2014 14:01:08 -0800
Subject: yields with invariants factored out into Yield12

---
 Test/og/multiset.bpl | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

(limited to 'Test')

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index a2a3c62b..48960e98 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -176,10 +176,7 @@ ensures {:atomic 2}  |{ var r:int;
  {
 
         var {:linear "tid"} tidTmp: X;
-        yield;
-        assert {:phase 1} Inv(valid, elt, owner);
-        assert {:phase 2} Inv(valid, elt, owner);
-        // par YieldInv();
+        par Yield12();
         tidTmp := tidIn;
         call i, tidTmp := FindSlot(x, tidTmp);
         
@@ -200,8 +197,6 @@ ensures {:atomic 2}  |{ var r:int;
 	call tidTmp := release(i, tidTmp);
 	result := true; 
         tidOut := tidTmp;
-        // yield;
-        // assert {:phase 2} Inv(valid, elt, owner);
         par YieldInv();
 	return;
 }
@@ -244,9 +239,7 @@ ensures {:atomic 2}  |{ var rx:int;
  {
 
         var {:linear "tid"} tidTmp: X;
-        yield;
-        assert {:phase 1} Inv(valid, elt, owner);
-        assert {:phase 2} Inv(valid, elt, owner);
+        par Yield12();
 
         tidTmp := tidIn;
 
@@ -256,9 +249,7 @@ ensures {:atomic 2}  |{ var rx:int;
 	{
 	 	result := false;
                 tidOut := tidTmp;
-                yield;
-                assert {:phase 1} Inv(valid, elt, owner);
-                assert {:phase 2} Inv(valid, elt, owner);
+                par Yield12();
 		return;
 	}
 
@@ -273,9 +264,7 @@ ensures {:atomic 2}  |{ var rx:int;
                 call tidTmp := release(i,tidTmp);  
 		result := false;
                 tidOut := tidTmp;
-                yield;
-                assert {:phase 1} Inv(valid, elt, owner);
-                assert {:phase 2} Inv(valid, elt, owner);
+                par Yield12();
 		return;
 	}
 
@@ -293,9 +282,7 @@ ensures {:atomic 2}  |{ var rx:int;
 	call tidTmp := release(i, tidTmp);
 	result := true; 
         tidOut := tidTmp;
-        yield;
-        assert {:phase 1} Inv(valid, elt, owner);
-        assert {:phase 2} Inv(valid, elt, owner);
+        par Yield12();
 	return;
 }
 
@@ -314,6 +301,14 @@ ensures {:phase 2} Inv(valid, elt, owner);
         assert {:phase 2} Inv(valid, elt, owner);
 }
 
+procedure {:yields} {:stable} Yield12()
+requires {:phase 1} {:phase 2} Inv(valid, elt, owner);
+ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);
+{
+        yield;
+        assert {:phase 1}  {:phase 2} Inv(valid, elt, owner);
+}
+
 
 
 function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)
-- 
cgit v1.2.3