some refactoring of QED stuff

1 files changed, 10 insertions, 10 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index f6510bee..7bf74e9c 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -99,7 +99,7 @@ COPY_TO_BUFFER:
 }

 

 procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

-ensures {:right} {:phase 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; return true; }|;

+ensures {:right 0} |{ A: assert ghostLock == tid' && tid' != nil; tid := tid'; return true; }|;

 {

     var j: int;

     tid := tid';

@@ -129,28 +129,28 @@ requires 0 <= start && 0 <= bytesRead && (bytesRead == 0 || start + bytesRead <=
 }

 

 procedure {:yields} ReadCurrsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := currsize; return true; }|;

 

 procedure {:yields} ReadNewsize({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, val: int);

-ensures {:right} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

+ensures {:right -1} |{A: assert tid' != nil; assert lock == tid' || ghostLock == tid'; tid := tid'; val := newsize; return true; }|;

 

 procedure {:yields} WriteNewsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == nil; tid := tid'; newsize := val; ghostLock := tid; return true; }|;

 

 procedure {:yields} WriteCurrsize({:linear "tid"} tid': X, val: int) returns ({:linear "tid"} tid: X);

-ensures {:atomic} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

+ensures {:atomic -1} |{A: assert tid' != nil; assert lock == tid' && ghostLock == tid'; tid := tid'; currsize := val; ghostLock := nil; return true; }|;

 

 procedure {:yields} ReadCacheEntry(index: int);

-ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;

+ensures {:atomic -1} |{ A: assert 0 <= index && index < currsize; return true; }|;

 

 procedure {:yields} WriteCacheEntry({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X);

-ensures {:right} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

+ensures {:right -1} |{ A: assert tid' != nil; assert currsize <= index && ghostLock == tid'; tid := tid'; return true; }|;

 

 procedure {:yields} acquire({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:right} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;

+ensures {:right -1} |{ A: assert tid' != nil; tid := tid'; assume lock == nil; lock := tid; return true; }|;

 

 procedure {:yields} release({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);

-ensures {:left} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;

+ensures {:left -1} |{ A: assert tid' != nil; assert lock == tid'; tid := tid'; lock := nil; return true; }|;

 

 procedure {:yields} Skip();

-ensures {:both} |{ A: return true; }|;
\ No newline at end of file
+ensures {:both -1} |{ A: return true; }|;
\ No newline at end of file