diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c | 103 |
1 files changed, 55 insertions, 48 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c index 0b4fdbc3c..e40fe22e4 100644 --- a/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c +++ b/FreeRTOS/Test/VeriFast/queue/xQueueGenericSend.c @@ -31,45 +31,50 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue, const void * const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition ) + /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& - [1/2]queuesuspend(xQueue) &*& - chars(pvItemToQueue, M, ?x) &*& - (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/ + * [1/2]queuesuspend(xQueue) &*& + * chars(pvItemToQueue, M, ?x) &*& + * (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/ + /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& - [1/2]queuesuspend(xQueue) &*& - chars(pvItemToQueue, M, x);@*/ + * [1/2]queuesuspend(xQueue) &*& + * chars(pvItemToQueue, M, x);@*/ { BaseType_t xEntryTimeSet = pdFALSE, xYieldRequired; TimeOut_t xTimeOut; -#ifdef VERIFAST /*< const pointer declaration */ - Queue_t * pxQueue = xQueue; -#else - Queue_t * const pxQueue = xQueue; - configASSERT( pxQueue ); - configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); - configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) ); - #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) - { - configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); - } - #endif -#endif + #ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; + #else + Queue_t * const pxQueue = xQueue; + + configASSERT( pxQueue ); + configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); + configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) ); + #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(pvItemToQueue, M, x) &*& - u_integer(&xTicksToWait, _) &*& - (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1)) &*& - xTIME_OUT(&xTimeOut);@*/ + * [1/2]queuesuspend(xQueue) &*& + * chars(pvItemToQueue, M, x) &*& + * u_integer(&xTicksToWait, _) &*& + * (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1)) &*& + * xTIME_OUT(&xTimeOut);@*/ { taskENTER_CRITICAL(); { /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ + /* Is there room on the queue now? The running task must be the * highest priority task wanting to access the queue. If the head item * in the queue is to be overwritten then it does not matter if the @@ -177,19 +182,19 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue, #endif /* configUSE_QUEUE_SETS */ /*@ - if (xCopyPosition == queueSEND_TO_BACK) - { - close queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))); - } - else if (xCopyPosition == queueSEND_TO_FRONT) - { - close queue(pxQueue, Storage, N, M, W, (R == 0 ? (N-1) : (R-1)), (K+1), is_locked, cons(x, abs)); - } - else if (xCopyPosition == queueOVERWRITE) - { - close queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)); - } - @*/ + * if (xCopyPosition == queueSEND_TO_BACK) + * { + * close queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))); + * } + * else if (xCopyPosition == queueSEND_TO_FRONT) + * { + * close queue(pxQueue, Storage, N, M, W, (R == 0 ? (N-1) : (R-1)), (K+1), is_locked, cons(x, abs)); + * } + * else if (xCopyPosition == queueOVERWRITE) + * { + * close queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)); + * } + * @*/ taskEXIT_CRITICAL(); return pdPASS; } @@ -198,6 +203,7 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue, if( xTicksToWait == ( TickType_t ) 0 ) { /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ + /* The queue was full and no block time is specified (or * the block time has expired) so leave now. */ taskEXIT_CRITICAL(); @@ -220,6 +226,7 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue, mtCOVERAGE_TEST_MARKER(); } } + /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ } taskEXIT_CRITICAL(); @@ -263,24 +270,24 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue, { /* Try again. */ 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 { /* The timeout has expired. */ 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 traceQUEUE_SEND_FAILED( pxQueue ); return errQUEUE_FULL; |