begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/xQueuePeek.c

   1 /*
   2  * FreeRTOS V202111.00
   3  * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
   6  * this software and associated documentation files (the "Software"), to deal in
   7  * the Software without restriction, including without limitation the rights to
   8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
   9  * the Software, and to permit persons to whom the Software is furnished to do so,
  10  * subject to the following conditions:
  11  *
  12  * The above copyright notice and this permission notice shall be included in all
  13  * copies or substantial portions of the Software.
  14  *
  15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
  17  * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
  18  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  21  *
  22  * https://www.FreeRTOS.org
  23  * https://github.com/FreeRTOS
  24  *
  25  */
  26
  27 #include "proof/queue.h"
  28 #include "proof/queuecontracts.h"
  29
  30 BaseType_t xQueuePeek( QueueHandle_t xQueue,
  31                        void * const pvBuffer,
  32                        TickType_t xTicksToWait )
  33
  34 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
  35  *  [1/2]queuesuspend(xQueue) &*&
  36  *  chars(pvBuffer, M, ?x);@*/
  37
  38 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  39  *  [1/2]queuesuspend(xQueue) &*&
  40  *  (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/
  41 {
  42     BaseType_t xEntryTimeSet = pdFALSE;
  43     TimeOut_t xTimeOut;
  44     int8_t * pcOriginalReadPosition;
  45
  46     #ifdef VERIFAST /*< const pointer declaration */
  47         Queue_t * pxQueue = xQueue;
  48     #else
  49         Queue_t * const pxQueue = xQueue;
  50
  51         /* Check the pointer is not NULL. */
  52         configASSERT( ( pxQueue ) );
  53
  54         /* The buffer into which data is received can only be NULL if the data size
  55          * is zero (so no data is copied into the buffer. */
  56         configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) );
  57
  58         /* Cannot block if the scheduler is suspended. */
  59         #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) )
  60             {
  61                 configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) );
  62             }
  63         #endif
  64     #endif /* ifdef VERIFAST */
  65
  66     /*lint -save -e904  This function relaxes the coding standard somewhat to
  67      * allow return statements within the function itself.  This is done in the
  68      * interest of execution time efficiency. */
  69     for( ; ; )
  70
  71     /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  72      *  [1/2]queuesuspend(xQueue) &*&
  73      *  chars(pvBuffer, M, x) &*&
  74      *  u_integer(&xTicksToWait, _) &*&
  75      *  xTIME_OUT(&xTimeOut);@*/
  76     {
  77         taskENTER_CRITICAL();
  78         /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/
  79         {
  80             const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  81
  82             /* Is there data in the queue now?  To be running the calling task
  83              * must be the highest priority task wanting to access the queue. */
  84             if( uxMessagesWaiting > ( UBaseType_t ) 0 )
  85             {
  86                 /* Remember the read position so it can be reset after the data
  87                  * is read from the queue as this function is only peeking the
  88                  * data, not removing it. */
  89                 pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  90
  91                 /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  92                 prvCopyDataFromQueue( pxQueue, pvBuffer );
  93                 traceQUEUE_PEEK( pxQueue );
  94
  95                 /* The data is not being removed, so reset the read pointer. */
  96                 pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  97
  98                 /* The data is being left in the queue, so see if there are
  99                  * any other tasks waiting for the data. */
 100                 if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) ) == pdFALSE )
 101                 {
 102                     if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToReceive ) ) != pdFALSE )
 103                     {
 104                         /* The task waiting has a higher priority than this task. */
 105                         queueYIELD_IF_USING_PREEMPTION();
 106                     }
 107                     else
 108                     {
 109                         mtCOVERAGE_TEST_MARKER();
 110                     }
 111                 }
 112                 else
 113                 {
 114                     mtCOVERAGE_TEST_MARKER();
 115                 }
 116
 117                 /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 118                 taskEXIT_CRITICAL();
 119                 return pdPASS;
 120             }
 121             else
 122             {
 123                 if( xTicksToWait == ( TickType_t ) 0 )
 124                 {
 125                     /* The queue was empty and no block time is specified (or
 126                      * the block time has expired) so leave now. */
 127                     /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 128                     taskEXIT_CRITICAL();
 129                     traceQUEUE_PEEK_FAILED( pxQueue );
 130                     return errQUEUE_EMPTY;
 131                 }
 132                 else if( xEntryTimeSet == pdFALSE )
 133                 {
 134                     /* The queue was empty and a block time was specified so
 135                      * configure the timeout structure ready to enter the blocked
 136                      * state. */
 137                     vTaskInternalSetTimeOutState( &xTimeOut );
 138                     xEntryTimeSet = pdTRUE;
 139                 }
 140                 else
 141                 {
 142                     /* Entry time was already set. */
 143                     mtCOVERAGE_TEST_MARKER();
 144                 }
 145             }
 146         }
 147         /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 148         taskEXIT_CRITICAL();
 149
 150         /* Interrupts and other tasks can send to and receive from the queue
 151          * now the critical section has been exited. */
 152
 153         /*@close exists<QueueHandle_t>(pxQueue);@*/
 154         vTaskSuspendAll();
 155         prvLockQueue( pxQueue );
 156
 157         /* Update the timeout state to see if it has expired yet. */
 158         if( xTaskCheckForTimeOut( &xTimeOut, &xTicksToWait ) == pdFALSE )
 159         {
 160             /* Timeout has not expired yet, check to see if there is data in the
 161             * queue now, and if not enter the Blocked state to wait for data. */
 162             if( prvIsQueueEmpty( pxQueue ) != pdFALSE )
 163             {
 164                 traceBLOCKING_ON_QUEUE_PEEK( pxQueue );
 165                 /*@open queue_locked_invariant(xQueue)();@*/
 166                 vTaskPlaceOnEventList( &( pxQueue->xTasksWaitingToReceive ), xTicksToWait );
 167                 /*@close queue_locked_invariant(xQueue)();@*/
 168                 prvUnlockQueue( pxQueue );
 169
 170                 /*@close exists<QueueHandle_t>(pxQueue);@*/
 171                 if( xTaskResumeAll() == pdFALSE )
 172                 {
 173                     portYIELD_WITHIN_API();
 174                 }
 175                 else
 176                 {
 177                     mtCOVERAGE_TEST_MARKER();
 178                 }
 179             }
 180             else
 181             {
 182                 /* There is data in the queue now, so don't enter the blocked
 183                  * state, instead return to try and obtain the data. */
 184                 prvUnlockQueue( pxQueue );
 185                 #ifdef VERIFAST /*< void cast of unused return value */
 186                     /*@close exists<QueueHandle_t>(pxQueue);@*/
 187                     xTaskResumeAll();
 188                 #else
 189                     ( void ) xTaskResumeAll();
 190                 #endif
 191             }
 192         }
 193         else
 194         {
 195             /* The timeout has expired.  If there is still no data in the queue
 196              * exit, otherwise go back and try to read the data again. */
 197             prvUnlockQueue( pxQueue );
 198             #ifdef VERIFAST /*< void cast of unused return value */
 199                 /*@close exists<QueueHandle_t>(pxQueue);@*/
 200                 xTaskResumeAll();
 201             #else
 202                 ( void ) xTaskResumeAll();
 203             #endif
 204
 205             if( prvIsQueueEmpty( pxQueue ) != pdFALSE )
 206             {
 207                 traceQUEUE_PEEK_FAILED( pxQueue );
 208                 return errQUEUE_EMPTY;
 209             }
 210             else
 211             {
 212                 mtCOVERAGE_TEST_MARKER();
 213             }
 214         }
 215     } /*lint -restore */
 216 }