diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/create.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/create.c | 206 |
1 files changed, 107 insertions, 99 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/create.c b/FreeRTOS/Test/VeriFast/queue/create.c index 144e87839..3282676a9 100644 --- a/FreeRTOS/Test/VeriFast/queue/create.c +++ b/FreeRTOS/Test/VeriFast/queue/create.c @@ -37,35 +37,37 @@ /* The following intermediate queue predicates summarise states used by queue * initialization but not used elsewhere so we confine them to these proofs * locally. */ + /*@ -predicate queue_init1(QueueHandle_t q;) = - QUEUE_SHAPE(q, _, _, _, _) &*& - queuelists(q) - ; - -predicate queue_init2(QueueHandle_t q, int8_t *Storage, size_t N, size_t M;) = - QUEUE_SHAPE(q, Storage, N, M, _) &*& - queuelists(q) &*& - 0 < N &*& - chars(Storage, (N*M), _) &*& - malloc_block(Storage, N*M) &*& - Storage + N * M <= (int8_t *)UINTPTR_MAX &*& - true - ; -@*/ + * predicate queue_init1(QueueHandle_t q;) = + * QUEUE_SHAPE(q, _, _, _, _) &*& + * queuelists(q) + * ; + * + * predicate queue_init2(QueueHandle_t q, int8_t *Storage, size_t N, size_t M;) = + * QUEUE_SHAPE(q, Storage, N, M, _) &*& + * queuelists(q) &*& + * 0 < N &*& + * chars(Storage, (N*M), _) &*& + * malloc_block(Storage, N*M) &*& + * Storage + N * M <= (int8_t *)UINTPTR_MAX &*& + * true + * ; + * @*/ BaseType_t xQueueGenericReset( QueueHandle_t xQueue, BaseType_t xNewQueue ) /*@requires queue_init2(xQueue, ?Storage, ?N, ?M);@*/ + /*@ensures 0 == M - ? freertos_mutex(xQueue, Storage, N, 0) - : queue(xQueue, Storage, N, M, 0, (N-1), 0, false, nil) &*& queuelists(xQueue);@*/ + * ? freertos_mutex(xQueue, Storage, N, 0) + * : queue(xQueue, Storage, N, M, 0, (N-1), 0, false, nil) &*& queuelists(xQueue);@*/ { -#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 ); @@ -125,18 +127,20 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, Queue_t * pxNewQueue ) /*@requires queue_init1(pxNewQueue) &*& - 0 < uxQueueLength &*& 0 < uxItemSize &*& - malloc_block(pucQueueStorage, uxQueueLength * uxItemSize) &*& - pucQueueStorage + uxQueueLength * uxItemSize <= (uint8_t *)UINTPTR_MAX &*& - uchars(pucQueueStorage, uxQueueLength * uxItemSize,_);@*/ + * 0 < uxQueueLength &*& 0 < uxItemSize &*& + * malloc_block(pucQueueStorage, uxQueueLength * uxItemSize) &*& + * pucQueueStorage + uxQueueLength * uxItemSize <= (uint8_t *)UINTPTR_MAX &*& + * uchars(pucQueueStorage, uxQueueLength * uxItemSize,_);@*/ + /*@ensures queue(pxNewQueue, ((int8_t *)(void *)pucQueueStorage), uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& - queuelists(pxNewQueue);@*/ + * queuelists(pxNewQueue);@*/ { -#ifndef VERIFAST /*< void cast of unused var */ - /* Remove compiler warnings about unused parameters should - * configUSE_TRACE_FACILITY not be set to 1. */ - ( void ) ucQueueType; -#endif + #ifndef VERIFAST /*< void cast of unused var */ + + /* Remove compiler warnings about unused parameters should + * configUSE_TRACE_FACILITY not be set to 1. */ + ( void ) ucQueueType; + #endif if( uxItemSize == ( UBaseType_t ) 0 ) { @@ -144,20 +148,20 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, * be set to NULL because NULL is used as a key to say the queue is used as * a mutex. Therefore just set pcHead to point to the queue as a benign * value that is known to be within the memory map. */ -#ifdef VERIFAST /*< stricter casting */ - pxNewQueue->pcHead = ( int8_t * ) ( void * ) pxNewQueue; -#else - pxNewQueue->pcHead = ( int8_t * ) pxNewQueue; -#endif + #ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pxNewQueue; + #else + pxNewQueue->pcHead = ( int8_t * ) pxNewQueue; + #endif } else { /* Set the head to the start of the queue storage area. */ -#ifdef VERIFAST /*< stricter casting */ - pxNewQueue->pcHead = ( int8_t * ) ( void * ) pucQueueStorage; -#else - pxNewQueue->pcHead = ( int8_t * ) pucQueueStorage; -#endif + #ifdef VERIFAST /*< stricter casting */ + pxNewQueue->pcHead = ( int8_t * ) ( void * ) pucQueueStorage; + #else + pxNewQueue->pcHead = ( int8_t * ) pucQueueStorage; + #endif } /* Initialise the queue members as described where the queue type is @@ -165,11 +169,11 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, pxNewQueue->uxLength = uxQueueLength; pxNewQueue->uxItemSize = uxItemSize; /*@close queue_init2(pxNewQueue, _, uxQueueLength, uxItemSize);@*/ -#ifdef VERIFAST /*< void cast of unused return value */ - xQueueGenericReset( pxNewQueue, pdTRUE ); -#else - ( void ) xQueueGenericReset( pxNewQueue, pdTRUE ); -#endif + #ifdef VERIFAST /*< void cast of unused return value */ + xQueueGenericReset( pxNewQueue, pdTRUE ); + #else + ( void ) xQueueGenericReset( pxNewQueue, pdTRUE ); + #endif #if ( configUSE_TRACE_FACILITY == 1 ) { @@ -187,41 +191,44 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, } - QueueHandle_t xQueueGenericCreate( const UBaseType_t uxQueueLength, - const UBaseType_t uxItemSize, - const uint8_t ucQueueType ) - /*@requires 0 < uxQueueLength &*& - 0 < uxItemSize &*& - 0 < uxQueueLength * uxItemSize &*& - uxQueueLength * uxItemSize <= UINT_MAX;@*/ - /*@ensures result == NULL - ? true - : queue(result, _, uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& - queuelists(result) &*& - result->irqMask |-> _ &*& - result->schedulerSuspend |-> _ &*& - result->locked |-> _;@*/ - { - Queue_t * pxNewQueue; - size_t xQueueSizeInBytes; - uint8_t * pucQueueStorage; +QueueHandle_t xQueueGenericCreate( const UBaseType_t uxQueueLength, + const UBaseType_t uxItemSize, + const uint8_t ucQueueType ) - configASSERT( uxQueueLength > ( UBaseType_t ) 0 ); +/*@requires 0 < uxQueueLength &*& + * 0 < uxItemSize &*& + * 0 < uxQueueLength * uxItemSize &*& + * uxQueueLength * uxItemSize <= UINT_MAX;@*/ + +/*@ensures result == NULL + * ? true + * : queue(result, _, uxQueueLength, uxItemSize, 0, (uxQueueLength-1), 0, false, nil) &*& + * queuelists(result) &*& + * result->irqMask |-> _ &*& + * result->schedulerSuspend |-> _ &*& + * result->locked |-> _;@*/ +{ + Queue_t * pxNewQueue; + size_t xQueueSizeInBytes; + uint8_t * pucQueueStorage; - /* Allocate enough space to hold the maximum number of items that - * can be in the queue at any time. It is valid for uxItemSize to be - * zero in the case the queue is used as a semaphore. */ - xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ + configASSERT( uxQueueLength > ( UBaseType_t ) 0 ); - /* Check for multiplication overflow. */ - configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); + /* Allocate enough space to hold the maximum number of items that + * can be in the queue at any time. It is valid for uxItemSize to be + * zero in the case the queue is used as a semaphore. */ + xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ - /* Check for addition overflow. */ - configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) > xQueueSizeInBytes ); + /* Check for multiplication overflow. */ + configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); -#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + /* Check for addition overflow. */ + configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) > xQueueSizeInBytes ); + + #ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) ); -#else + #else + /* Allocate the queue and storage area. Justification for MISRA * deviation as follows: pvPortMalloc() always ensures returned memory * blocks are aligned per the requirements of the MCU stack. In this case @@ -232,11 +239,11 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, * is safe. In other cases alignment requirements are not strict (one or * two bytes). */ pxNewQueue = ( Queue_t * ) pvPortMalloc( sizeof( Queue_t ) + xQueueSizeInBytes ); /*lint !e9087 !e9079 see comment above. */ -#endif + #endif - if( pxNewQueue != NULL ) - { -#ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ + if( pxNewQueue != NULL ) + { + #ifdef VERIFAST /*< ***model single malloc of struct and buffer*** */ pucQueueStorage = ( uint8_t * ) pvPortMalloc( xQueueSizeInBytes ); if( pucQueueStorage == NULL ) @@ -246,29 +253,30 @@ static void prvInitialiseNewQueue( const UBaseType_t uxQueueLength, } /*@malloc_block_limits(pucQueueStorage);@*/ -#else + #else + /* Jump past the queue structure to find the location of the queue * storage area. */ pucQueueStorage = ( uint8_t * ) pxNewQueue; pucQueueStorage += sizeof( Queue_t ); /*lint !e9016 Pointer arithmetic allowed on char types, especially when it assists conveying intent. */ -#endif + #endif /* ifdef VERIFAST */ - #if ( configSUPPORT_STATIC_ALLOCATION == 1 ) - { - /* Queues can be created either statically or dynamically, so - * note this task was created dynamically in case it is later - * deleted. */ - pxNewQueue->ucStaticallyAllocated = pdFALSE; - } - #endif /* configSUPPORT_STATIC_ALLOCATION */ - - prvInitialiseNewQueue( uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue ); - } - else - { - traceQUEUE_CREATE_FAILED( ucQueueType ); - mtCOVERAGE_TEST_MARKER(); - } + #if ( configSUPPORT_STATIC_ALLOCATION == 1 ) + { + /* Queues can be created either statically or dynamically, so + * note this task was created dynamically in case it is later + * deleted. */ + pxNewQueue->ucStaticallyAllocated = pdFALSE; + } + #endif /* configSUPPORT_STATIC_ALLOCATION */ - return pxNewQueue; + prvInitialiseNewQueue( uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue ); + } + else + { + traceQUEUE_CREATE_FAILED( ucQueueType ); + mtCOVERAGE_TEST_MARKER(); } + + return pxNewQueue; +} |