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

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