simplified yield type chcking and added treiber stack (not fully done)

1 files changed, 5 insertions, 1 deletions

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 6130b69b..c936cab7 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -36,10 +36,14 @@ ensures {:phase 1} a[tid] == old(a)[tid] + 1;
 { 

     var t:int;

 

+    yield;

+    assert {:phase 1} a[tid] == old(a)[tid];

     call t := Read(tid); 

     yield;

-    assert {:phase 1} t == a[tid]; 

+    assert {:phase 1} a[tid] == t; 

     call Write(tid, t + 1); 

+    yield;

+    assert {:phase 1} a[tid] == t + 1; 

 }

 

 procedure {:yields} {:phase 0,1} Read({:cnst "tid"} tid: Tid) returns (val: int);