begriffs open source - cmsis-freertos/blob - Test/VeriFast/queue/vQueueDelete.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 #define configSUPPORT_DYNAMIC_ALLOCATION    1
  29 #define configSUPPORT_STATIC_ALLOCATION     0
  30
  31 void vQueueDelete( QueueHandle_t xQueue )
  32
  33 /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
  34  *  queuelists(xQueue) &*&
  35  *  xQueue->irqMask |-> _ &*&
  36  *  xQueue->schedulerSuspend |-> _ &*&
  37  *  xQueue->locked |-> _;@*/
  38 /*@ensures true;@*/
  39 {
  40     #ifdef VERIFAST /*< const pointer declaration */
  41         Queue_t * pxQueue = xQueue;
  42     #else
  43         Queue_t * const pxQueue = xQueue;
  44     #endif
  45
  46     configASSERT( pxQueue );
  47     traceQUEUE_DELETE( pxQueue );
  48
  49     #if ( configQUEUE_REGISTRY_SIZE > 0 )
  50         {
  51             vQueueUnregisterQueue( pxQueue );
  52         }
  53     #endif
  54
  55     #if ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 0 ) )
  56         {
  57             /* The queue can only have been allocated dynamically - free it
  58              * again. */
  59             vPortFree( pxQueue );
  60             #ifdef VERIFAST /*< leak ghost state on deletion */
  61                 /*@leak buffer(_, _, _, _);@*/
  62                 /*@leak malloc_block(_, _);@*/
  63             #endif
  64         }
  65     #elif ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 1 ) )
  66         {
  67             /* The queue could have been allocated statically or dynamically, so
  68              * check before attempting to free the memory. */
  69             if( pxQueue->ucStaticallyAllocated == ( uint8_t ) pdFALSE )
  70             {
  71                 vPortFree( pxQueue );
  72             }
  73             else
  74             {
  75                 mtCOVERAGE_TEST_MARKER();
  76             }
  77         }
  78     #else /* if ( ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) && ( configSUPPORT_STATIC_ALLOCATION == 0 ) ) */
  79         {
  80             /* The queue must have been statically allocated, so is not going to be
  81              * deleted.  Avoid compiler warnings about the unused parameter. */
  82             ( void ) pxQueue;
  83         }
  84     #endif /* configSUPPORT_DYNAMIC_ALLOCATION */
  85 }