diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/xQueueReceive.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/xQueueReceive.c | 82 |
1 files changed, 44 insertions, 38 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c index ac8740eda..63a13cc3d 100644 --- a/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c +++ b/FreeRTOS/Test/VeriFast/queue/xQueueReceive.c @@ -30,44 +30,48 @@ BaseType_t xQueueReceive( QueueHandle_t xQueue, void * const pvBuffer, TickType_t xTicksToWait ) + /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& - [1/2]queuesuspend(xQueue) &*& - chars(pvBuffer, M, ?x);@*/ + * [1/2]queuesuspend(xQueue) &*& + * chars(pvBuffer, M, ?x);@*/ + /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& - [1/2]queuesuspend(xQueue) &*& - (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/ + * [1/2]queuesuspend(xQueue) &*& + * (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/ { BaseType_t xEntryTimeSet = pdFALSE; TimeOut_t xTimeOut; -#ifdef VERIFAST /*< const pointer declaration */ - Queue_t * pxQueue = xQueue; -#else - Queue_t * const pxQueue = xQueue; - /* Check the pointer is not NULL. */ - configASSERT( ( pxQueue ) ); + #ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; + #else + Queue_t * const pxQueue = xQueue; - /* The buffer into which data is received can only be NULL if the data size - * is zero (so no data is copied into the buffer). */ - configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) ); + /* Check the pointer is not NULL. */ + configASSERT( ( pxQueue ) ); - /* Cannot block if the scheduler is suspended. */ - #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) - { - configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); - } - #endif -#endif + /* The buffer into which data is received can only be NULL if the data size + * is zero (so no data is copied into the buffer). */ + configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) ); + + /* Cannot block if the scheduler is suspended. */ + #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) + { + configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); + } + #endif + #endif /* ifdef VERIFAST */ /*lint -save -e904 This function relaxes the coding standard somewhat to * allow return statements within the function itself. This is done in the * interest of execution time efficiency. */ for( ; ; ) + /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*& - [1/2]queuesuspend(xQueue) &*& - chars(pvBuffer, M, x) &*& - u_integer(&xTicksToWait, _) &*& - xTIME_OUT(&xTimeOut);@*/ + * [1/2]queuesuspend(xQueue) &*& + * chars(pvBuffer, M, x) &*& + * u_integer(&xTicksToWait, _) &*& + * xTIME_OUT(&xTimeOut);@*/ { taskENTER_CRITICAL(); /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ @@ -86,9 +90,10 @@ BaseType_t xQueueReceive( QueueHandle_t xQueue, pxQueue->uxMessagesWaiting = uxMessagesWaiting - ( UBaseType_t ) 1; /*@assert - pxQueue->pcHead |-> ?buffer &*& - buffer(buffer, N, M, ?contents);@*/ + * pxQueue->pcHead |-> ?buffer &*& + * buffer(buffer, N, M, ?contents);@*/ /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/ + /* There is now space in the queue, were any tasks waiting to * post to the queue? If so, unblock the highest priority waiting * task. */ @@ -118,6 +123,7 @@ BaseType_t xQueueReceive( QueueHandle_t xQueue, if( xTicksToWait == ( TickType_t ) 0 ) { /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + /* The queue was empty and no block time is specified (or * the block time has expired) so leave now. */ taskEXIT_CRITICAL(); @@ -176,12 +182,12 @@ BaseType_t xQueueReceive( QueueHandle_t xQueue, /* The queue contains data again. Loop back to try and read the * data. */ prvUnlockQueue( pxQueue ); -#ifdef VERIFAST /*< void cast of unused return value */ - /*@close exists(pxQueue);@*/ - xTaskResumeAll(); -#else - ( void ) xTaskResumeAll(); -#endif + #ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); + #else + ( void ) xTaskResumeAll(); + #endif } } else @@ -189,12 +195,12 @@ BaseType_t xQueueReceive( QueueHandle_t xQueue, /* Timed out. If there is no data in the queue exit, otherwise loop * back and attempt to read the data. */ prvUnlockQueue( pxQueue ); -#ifdef VERIFAST /*< void cast of unused return value */ - /*@close exists(pxQueue);@*/ - xTaskResumeAll(); -#else - ( void ) xTaskResumeAll(); -#endif + #ifdef VERIFAST /*< void cast of unused return value */ + /*@close exists(pxQueue);@*/ + xTaskResumeAll(); + #else + ( void ) xTaskResumeAll(); + #endif if( prvIsQueueEmpty( pxQueue ) != pdFALSE ) { |