| 30 | #include "proof/queuecontracts.h" |
| 31 | |
| 32 | BaseType_t xQueueGenericSend( QueueHandle_t xQueue, |
| 33 | const void * const pvItemToQueue, |
| 34 | TickType_t xTicksToWait, |
| 35 | const BaseType_t xCopyPosition ) |
| 36 | /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*& |
| 37 | [1/2]queuesuspend(xQueue) &*& |
| 38 | chars(pvItemToQueue, M, ?x) &*& |
| 39 | (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1));@*/ |
| 40 | /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*& |
| 41 | [1/2]queuesuspend(xQueue) &*& |
| 42 | chars(pvItemToQueue, M, x);@*/ |
| 43 | { |
| 44 | BaseType_t xEntryTimeSet = pdFALSE, xYieldRequired; |
| 45 | TimeOut_t xTimeOut; |
| 46 | #ifdef VERIFAST /*< const pointer declaration */ |
| 47 | Queue_t * pxQueue = xQueue; |
| 48 | #else |
| 49 | Queue_t * const pxQueue = xQueue; |
| 50 | |
| 51 | configASSERT( pxQueue ); |
| 52 | configASSERT( !( ( pvItemToQueue == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) ); |
| 53 | configASSERT( !( ( xCopyPosition == queueOVERWRITE ) && ( pxQueue->uxLength != 1 ) ) ); |
| 54 | #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) ) |
| 55 | { |
| 56 | configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) ); |
| 57 | } |
| 58 | #endif |
| 59 | #endif |
| 60 | |
| 61 | /*lint -save -e904 This function relaxes the coding standard somewhat to |
| 62 | * allow return statements within the function itself. This is done in the |
| 63 | * interest of execution time efficiency. */ |
| 64 | for( ; ; ) |
| 65 | /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*& |
| 66 | [1/2]queuesuspend(xQueue) &*& |
| 67 | chars(pvItemToQueue, M, x) &*& |
| 68 | u_integer(&xTicksToWait, _) &*& |
| 69 | (xCopyPosition == queueSEND_TO_BACK || xCopyPosition == queueSEND_TO_FRONT || (xCopyPosition == queueOVERWRITE && N == 1)) &*& |
| 70 | xTIME_OUT(&xTimeOut);@*/ |
| 71 | { |
| 72 | taskENTER_CRITICAL(); |
| 73 | { |
| 74 | /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ |
| 75 | /* Is there room on the queue now? The running task must be the |
| 76 | * highest priority task wanting to access the queue. If the head item |
| 77 | * in the queue is to be overwritten then it does not matter if the |
| 78 | * queue is full. */ |
| 79 | if( ( pxQueue->uxMessagesWaiting < pxQueue->uxLength ) || ( xCopyPosition == queueOVERWRITE ) ) |
| 80 | { |
| 81 | traceQUEUE_SEND( pxQueue ); |
| 82 | |
| 83 | /* VeriFast: we do not verify this configuration option */ |
| 84 | #if ( configUSE_QUEUE_SETS == 1 ) |
| 85 | { |
| 86 | const UBaseType_t uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting; |
| 87 | |
| 88 | xYieldRequired = prvCopyDataToQueue( pxQueue, pvItemToQueue, xCopyPosition ); |
| 89 |
no test coverage detected