begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/Queue/QueueGenericSendFromISR/QueueGenericSendFromISR_harness.c

   1 /*
   2  * FreeRTOS memory safety proofs with CBMC.
   3  * Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person
   6  * obtaining a copy of this software and associated documentation
   7  * files (the "Software"), to deal in the Software without
   8  * restriction, including without limitation the rights to use, copy,
   9  * modify, merge, publish, distribute, sublicense, and/or sell copies
  10  * of the Software, and to permit persons to whom the Software is
  11  * furnished to do so, subject to the following conditions:
  12  *
  13  * The above copyright notice and this permission notice shall be
  14  * included in all copies or substantial portions of the Software.
  15  *
  16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  17  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  18  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  19  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
  20  * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
  21  * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  22  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
  23  * SOFTWARE.
  24  *
  25  * http://aws.amazon.com/freertos
  26  * http://www.FreeRTOS.org
  27  */
  28
  29 #include "FreeRTOS.h"
  30 #include "queue.h"
  31 #include "queue_init.h"
  32
  33 #include "cbmc.h"
  34
  35 #ifndef ITEM_BOUND
  36     #define ITEM_BOUND    10
  37 #endif
  38
  39 #if ( configUSE_QUEUE_SETS == 0 )
  40     BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
  41                                    const void * pvItemToQueue,
  42                                    const BaseType_t xPosition )
  43     {
  44         if( pxQueue->uxItemSize > ( UBaseType_t ) 0 )
  45         {
  46             __CPROVER_assert( __CPROVER_r_ok( pvItemToQueue, ( size_t ) pxQueue->uxItemSize ), "pvItemToQueue region must be readable" );
  47
  48             if( xPosition == queueSEND_TO_BACK )
  49             {
  50                 __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize ), "pxQueue->pcWriteTo region must be writable" );
  51             }
  52             else
  53             {
  54                 __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ), "pxQueue->u.xQueue.pcReadFrom region must be writable" );
  55             }
  56
  57             return pdFALSE;
  58         }
  59         else
  60         {
  61             return nondet_BaseType_t();
  62         }
  63     }
  64 #endif /* if ( configUSE_QUEUE_SETS == 0 ) */
  65
  66 void harness()
  67 {
  68     QueueHandle_t xQueue = xUnconstrainedQueueBoundedItemSize( ITEM_BOUND );
  69
  70
  71     if( xQueue )
  72     {
  73         void * pvItemToQueue = pvPortMalloc( xQueue->uxItemSize );
  74         BaseType_t * xHigherPriorityTaskWoken = pvPortMalloc( sizeof( BaseType_t ) );
  75         BaseType_t xCopyPosition;
  76
  77         if( xQueue->uxItemSize == 0 )
  78         {
  79             /* uxQueue->xQueueType is a pointer to the head of the queue storage area.
  80              * If an item has a size, this pointer must not be modified after init.
  81              * Otherwise some of the write statements will fail. */
  82             xQueue->uxQueueType = nondet_int8_t();
  83             pvItemToQueue = 0;
  84         }
  85
  86         /* This code checks explicitly for violations of the pxQueue->uxMessagesWaiting < pxQueue->uxLength
  87          * invariant. */
  88         xQueue->uxMessagesWaiting = nondet_UBaseType_t();
  89
  90         if( !pvItemToQueue )
  91         {
  92             xQueue->uxItemSize = 0;
  93         }
  94
  95         if( xCopyPosition == 2 )
  96         {
  97             __CPROVER_assume( xQueue->uxLength == 1 );
  98         }
  99
 100         xQueueGenericSendFromISR( xQueue, pvItemToQueue, xHigherPriorityTaskWoken, xCopyPosition );
 101     }
 102 }