diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c index 62b5a62cd..e392a023f 100644 --- a/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c +++ b/FreeRTOS/Test/VeriFast/queue/prvUnlockQueue.c @@ -32,12 +32,14 @@ * decrementing `cTxLock` and `cRxLock`. */ static void prvUnlockQueue( Queue_t * const pxQueue ) + /*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& - [1/2]pxQueue->locked |-> ?m &*& - mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*& - queue_locked_invariant(pxQueue)();@*/ + * [1/2]pxQueue->locked |-> ?m &*& + * mutex_held(m, queue_locked_invariant(pxQueue), currentThread, 1/2) &*& + * queue_locked_invariant(pxQueue)();@*/ + /*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr) &*& - [1/2]queuelock(pxQueue);@*/ + * [1/2]queuelock(pxQueue);@*/ { /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */ @@ -125,12 +127,12 @@ static void prvUnlockQueue( Queue_t * const pxQueue ) pxQueue->cTxLock = queueUNLOCKED; } -#ifndef VERIFAST /*< ***merge cTxLock and cRxLock critical regions*** */ - taskEXIT_CRITICAL(); + #ifndef VERIFAST /*< ***merge cTxLock and cRxLock critical regions*** */ + taskEXIT_CRITICAL(); - /* Do the same for the Rx lock. */ - taskENTER_CRITICAL(); -#endif + /* Do the same for the Rx lock. */ + taskENTER_CRITICAL(); + #endif { int8_t cRxLock = pxQueue->cRxLock; @@ -160,7 +162,7 @@ static void prvUnlockQueue( Queue_t * const pxQueue ) } /*@close queue(pxQueue, Storage, N, M, W, R, K, false, abs);@*/ taskEXIT_CRITICAL(); -#ifdef VERIFAST /*< ghost action */ - mutex_release( pxQueue->locked ); -#endif + #ifdef VERIFAST /*< ghost action */ + mutex_release( pxQueue->locked ); + #endif } |