begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/xQueuePeekFromISR.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 xQueuePeekFromISR( QueueHandle_t xQueue,
  31                               void * const pvBuffer )
  32
  33 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true &*&
  34  *  chars(pvBuffer, M, ?x);@*/
  35
  36 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
  37  *  (result == pdPASS ? chars(pvBuffer, M, _) : chars(pvBuffer, M, x));@*/
  38 {
  39     BaseType_t xReturn;
  40     UBaseType_t uxSavedInterruptStatus;
  41     int8_t * pcOriginalReadPosition;
  42
  43     #ifdef VERIFAST /*< const pointer declaration */
  44         Queue_t * pxQueue = xQueue;
  45     #else
  46         Queue_t * const pxQueue = xQueue;
  47
  48         configASSERT( pxQueue );
  49         configASSERT( !( ( pvBuffer == NULL ) && ( pxQueue->uxItemSize != ( UBaseType_t ) 0U ) ) );
  50         configASSERT( pxQueue->uxItemSize != 0 ); /* Can't peek a semaphore. */
  51     #endif
  52
  53     /* RTOS ports that support interrupt nesting have the concept of a maximum
  54      * system call (or maximum API call) interrupt priority.  Interrupts that are
  55      * above the maximum system call priority are kept permanently enabled, even
  56      * when the RTOS kernel is in a critical section, but cannot make any calls to
  57      * FreeRTOS API functions.  If configASSERT() is defined in FreeRTOSConfig.h
  58      * then portASSERT_IF_INTERRUPT_PRIORITY_INVALID() will result in an assertion
  59      * failure if a FreeRTOS API function is called from an interrupt that has been
  60      * assigned a priority above the configured maximum system call priority.
  61      * Only FreeRTOS functions that end in FromISR can be called from interrupts
  62      * that have been assigned a priority at or (logically) below the maximum
  63      * system call interrupt priority.  FreeRTOS maintains a separate interrupt
  64      * safe API to ensure interrupt entry is as fast and as simple as possible.
  65      * More information (albeit Cortex-M specific) is provided on the following
  66      * link: https://www.FreeRTOS.org/RTOS-Cortex-M3-M4.html */
  67     portASSERT_IF_INTERRUPT_PRIORITY_INVALID();
  68
  69     uxSavedInterruptStatus = portSET_INTERRUPT_MASK_FROM_ISR();
  70     /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/
  71     {
  72         /* Cannot block in an ISR, so check there is data available. */
  73         if( pxQueue->uxMessagesWaiting > ( UBaseType_t ) 0 )
  74         {
  75             traceQUEUE_PEEK_FROM_ISR( pxQueue );
  76
  77             /* Remember the read position so it can be reset as nothing is
  78              * actually being removed from the queue. */
  79             pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  80             /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  81             prvCopyDataFromQueue( pxQueue, pvBuffer );
  82             pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  83             /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  84
  85             xReturn = pdPASS;
  86         }
  87         else
  88         {
  89             xReturn = pdFAIL;
  90             traceQUEUE_PEEK_FROM_ISR_FAILED( pxQueue );
  91         }
  92     }
  93     /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/
  94     portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus );
  95
  96     return xReturn;
  97 }