diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c index 2b88a420e..37292dd81 100644 --- a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c +++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c @@ -28,16 +28,17 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + /*@ensures queue(xQueue, Storage, N, M, W, R, K, is_locked, abs) &*& - result == ((K == N) ? pdTRUE : pdFALSE);@*/ + * result == ((K == N) ? pdTRUE : pdFALSE);@*/ { BaseType_t xReturn; -#ifdef VERIFAST /*< const pointer declaration */ - Queue_t * pxQueue = xQueue; -#else - Queue_t * const pxQueue = xQueue; -#endif + #ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; + #else + Queue_t * const pxQueue = xQueue; + #endif configASSERT( pxQueue ); |