diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/vQueueDelete.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/vQueueDelete.c | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c index 8107a2aa9..9dc67d6ef 100644 --- a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c +++ b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c @@ -29,18 +29,19 @@ #define configSUPPORT_STATIC_ALLOCATION 0 void vQueueDelete( QueueHandle_t xQueue ) + /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& - queuelists(xQueue) &*& - xQueue->irqMask |-> _ &*& - xQueue->schedulerSuspend |-> _ &*& - xQueue->locked |-> _;@*/ + * queuelists(xQueue) &*& + * xQueue->irqMask |-> _ &*& + * xQueue->schedulerSuspend |-> _ &*& + * xQueue->locked |-> _;@*/ /*@ensures true;@*/ { -#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 ); traceQUEUE_DELETE( pxQueue ); @@ -56,10 +57,10 @@ void vQueueDelete( QueueHandle_t xQueue ) /* The queue can only have been allocated dynamically - free it * again. */ vPortFree( pxQueue ); -#ifdef VERIFAST /*< leak ghost state on deletion */ - /*@leak buffer(_, _, _, _);@*/ - /*@leak malloc_block(_, _);@*/ -#endif + #ifdef VERIFAST /*< leak ghost state on deletion */ + /*@leak buffer(_, _, _, _);@*/ + /*@leak malloc_block(_, _);@*/ + #endif } #elif ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 1 ) ) { |