a fix regarding the checking of assertions in atomic specs at call sites

2 files changed, 6 insertions, 7 deletions

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index a9238cbb..025fb80c 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -15,7 +15,6 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
 procedure {:stable} {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && tid == tid' && old(currsize) <= currsize;

-ensures {:both 2} |{ A: return true; }|;

 {

    tid := tid';

 }

@@ -23,7 +22,6 @@ ensures {:both 2} |{ A: return true; }|;
 procedure {:stable} {:yields} YieldToWriteCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid' && tid' != nil;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil && tid == tid' && old(currsize) == currsize && old(newsize) == newsize;

-ensures {:both 2} |{ A: return true; }|;

 {

     tid := tid';

 }

@@ -110,7 +108,7 @@ COPY_TO_BUFFER:
 procedure {:yields} WriteCache({:linear "tid"} tid': X, index: int) returns ({:linear "tid"} tid: X)

 requires {:phase 1} Inv(ghostLock, currsize, newsize);

 requires {:phase 1} ghostLock == tid' && tid' != nil;

-ensures {:phase 1} tid == tid';

+ensures {:phase 1} tid == tid' && ghostLock == tid;

 ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize;

 {

     var j: int;

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 0e64f6b2..316c09c6 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -11,9 +11,6 @@ var {:qed} s: int;
 var {:qed} cs: X;

 var {:qed} T: [int]bool;

 

-procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:phase 1} {:phase 2} xl != nil;

-

 function Inv1(tickets: [int]bool, ticket: int): (bool)

 {

     tickets == RightOpen(ticket)

@@ -24,8 +21,11 @@ function Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
     if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)

 }

 

+procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

+ensures {:phase 1} {:phase 2} xl != nil;

+

 procedure {:yields} {:entrypoint} main({:linear "tid"} xls':[X]bool)

-requires {:phase 1} {:phase 2} xls' == mapconstbool(true);

+requires {:phase 3} xls' == mapconstbool(true);

 {

     var {:linear "tid"} tid: X;

     var {:linear "tid"} xls: [X]bool;

@@ -48,6 +48,7 @@ requires {:phase 1} {:phase 2} xls' == mapconstbool(true);
 procedure {:yields} {:stable} Customer({:linear "tid"} tid': X)

 requires {:phase 1} Inv1(T, t);

 requires {:phase 2} tid' != nil && Inv2(T, s, cs);

+requires {:phase 3} true;

 {

     var {:linear "tid"} tid: X;

     tid := tid';