diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/vQueueDelete.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/vQueueDelete.c | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c index bab0ca536..22d2a7d14 100644 --- a/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c +++ b/FreeRTOS/Test/VeriFast/queue/vQueueDelete.c @@ -24,24 +24,25 @@ * */ +/* *INDENT-OFF* */ + #include "proof/queue.h" #define configSUPPORT_DYNAMIC_ALLOCATION 1 #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 ); @@ -57,10 +58,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 ) ) { @@ -83,3 +84,5 @@ void vQueueDelete( QueueHandle_t xQueue ) } #endif /* configSUPPORT_DYNAMIC_ALLOCATION */ } + +/* *INDENT-ON* */ |