begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/xQueueReceive.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 xQueueReceive( 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
  45     #ifdef VERIFAST /*< const pointer declaration */
  46         Queue_t * pxQueue = xQueue;
  47     #else
  48         Queue_t * const pxQueue = xQueue;
  49
  50         /* Check the pointer is not NULL. */
  51         configASSERT( ( pxQueue ) );
  52
  53         /* The buffer into which data is received can only be NULL if the data size
  54          * is zero (so no data is copied into the buffer). */
  55         configASSERT( !( ( ( pvBuffer ) == NULL ) && ( ( pxQueue )->uxItemSize != ( UBaseType_t ) 0U ) ) );
  56
  57         /* Cannot block if the scheduler is suspended. */
  58         #if ( ( INCLUDE_xTaskGetSchedulerState == 1 ) || ( configUSE_TIMERS == 1 ) )
  59             {
  60                 configASSERT( !( ( xTaskGetSchedulerState() == taskSCHEDULER_SUSPENDED ) && ( xTicksToWait != 0 ) ) );
  61             }
  62         #endif
  63     #endif /* ifdef VERIFAST */
  64
  65     /*lint -save -e904  This function relaxes the coding standard somewhat to
  66      * allow return statements within the function itself.  This is done in the
  67      * interest of execution time efficiency. */
  68     for( ; ; )
  69
  70     /*@invariant [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  71      *  [1/2]queuesuspend(xQueue) &*&
  72      *  chars(pvBuffer, M, x) &*&
  73      *  u_integer(&xTicksToWait, _) &*&
  74      *  xTIME_OUT(&xTimeOut);@*/
  75     {
  76         taskENTER_CRITICAL();
  77         /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/
  78         {
  79             const UBaseType_t uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  80
  81             /* Is there data in the queue now?  To be running the calling task
  82              * must be the highest priority task wanting to access the queue. */
  83             if( uxMessagesWaiting > ( UBaseType_t ) 0 )
  84             {
  85                 /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  86                 /* Data available, remove one item. */
  87                 prvCopyDataFromQueue( pxQueue, pvBuffer );
  88                 /*@open queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs);@*/
  89                 traceQUEUE_RECEIVE( pxQueue );
  90                 pxQueue->uxMessagesWaiting = uxMessagesWaiting - ( UBaseType_t ) 1;
  91
  92                 /*@assert
  93                  *  pxQueue->pcHead |-> ?buffer &*&
  94                  *  buffer(buffer, N, M, ?contents);@*/
  95                 /*@deq_lemma(K, (R+1)%N, contents, abs, head(abs));@*/
  96
  97                 /* There is now space in the queue, were any tasks waiting to
  98                  * post to the queue?  If so, unblock the highest priority waiting
  99                  * task. */
 100                 if( listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToSend ) ) == pdFALSE )
 101                 {
 102                     if( xTaskRemoveFromEventList( &( pxQueue->xTasksWaitingToSend ) ) != pdFALSE )
 103                     {
 104                         queueYIELD_IF_USING_PREEMPTION();
 105                     }
 106                     else
 107                     {
 108                         mtCOVERAGE_TEST_MARKER();
 109                     }
 110                 }
 111                 else
 112                 {
 113                     mtCOVERAGE_TEST_MARKER();
 114                 }
 115
 116                 /*@close queue(pxQueue, Storage, N, M, W, (R+1)%N, K-1, is_locked, tail(abs));@*/
 117                 /*@assert chars(pvBuffer, M, head(abs));@*/
 118                 taskEXIT_CRITICAL();
 119                 return pdPASS;
 120             }
 121             else
 122             {
 123                 if( xTicksToWait == ( TickType_t ) 0 )
 124                 {
 125                     /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
 126
 127                     /* The queue was empty and no block time is specified (or
 128                      * the block time has expired) so leave now. */
 129                     taskEXIT_CRITICAL();
 130                     traceQUEUE_RECEIVE_FAILED( pxQueue );
 131                     return errQUEUE_EMPTY;
 132                 }
 133                 else if( xEntryTimeSet == pdFALSE )
 134                 {
 135                     /* The queue was empty and a block time was specified so
 136                      * configure the timeout structure. */
 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(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             /* The timeout has not expired.  If the queue is still empty place
 161              * the task on the list of tasks waiting to receive from the queue. */
 162             if( prvIsQueueEmpty( pxQueue ) != pdFALSE )
 163             {
 164                 traceBLOCKING_ON_QUEUE_RECEIVE( 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(pxQueue);@*/
 171                 if( xTaskResumeAll() == pdFALSE )
 172                 {
 173                     portYIELD_WITHIN_API();
 174                 }
 175                 else
 176                 {
 177                     mtCOVERAGE_TEST_MARKER();
 178                 }
 179             }
 180             else
 181             {
 182                 /* The queue contains data again.  Loop back to try and read the
 183                  * data. */
 184                 prvUnlockQueue( pxQueue );
 185                 #ifdef VERIFAST /*< void cast of unused return value */
 186                     /*@close exists(pxQueue);@*/
 187                     xTaskResumeAll();
 188                 #else
 189                     ( void ) xTaskResumeAll();
 190                 #endif
 191             }
 192         }
 193         else
 194         {
 195             /* Timed out.  If there is no data in the queue exit, otherwise loop
 196              * back and attempt to read the data. */
 197             prvUnlockQueue( pxQueue );
 198             #ifdef VERIFAST /*< void cast of unused return value */
 199                 /*@close exists(pxQueue);@*/
 200                 xTaskResumeAll();
 201             #else
 202                 ( void ) xTaskResumeAll();
 203             #endif
 204
 205             if( prvIsQueueEmpty( pxQueue ) != pdFALSE )
 206             {
 207                 traceQUEUE_RECEIVE_FAILED( pxQueue );
 208                 return errQUEUE_EMPTY;
 209             }
 210             else
 211             {
 212                 mtCOVERAGE_TEST_MARKER();
 213             }
 214         }
 215     } /*lint -restore */
 216 }