begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h

   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 "cbmc.h"
  30
  31 /*
  32  * Our stub for pvPortMalloc in cbmc.h nondeterministically chooses
  33  * either to return NULL or to allocate the requested memory.
  34  */
  35 void vNondetSetCurrentTCB( void )
  36 {
  37         pxCurrentTCB = pvPortMalloc( sizeof(TCB_t) );
  38 }
  39 /*
  40  * We just require task lists to be initialized for this proof
  41  */
  42 void vPrepareTaskLists( void )
  43 {
  44         __CPROVER_assert_zero_allocation();
  45
  46         prvInitialiseTaskLists();
  47 }
  48
  49 /*
  50  * We set the values of relevant global
  51  * variables to nondeterministic values
  52  */
  53 void vSetGlobalVariables( void )
  54 {
  55         xSchedulerRunning = nondet_basetype();
  56         uxCurrentNumberOfTasks = nondet_ubasetype();
  57 }
  58
  59 /*
  60  * pvPortMalloc is nondeterministic by definition, thus we do not need
  61  * to check for NULL allocation in this function
  62  */
  63 TaskHandle_t *pxNondetSetTaskHandle( void )
  64 {
  65         TaskHandle_t *pxNondetTaskHandle = pvPortMalloc( sizeof(TaskHandle_t) );
  66         return pxNondetTaskHandle;
  67 }
  68
  69 /*
  70  * Tries to allocate a string of size xStringLength and sets the string
  71  * to be terminated using a nondeterministic index if allocation was successful
  72  */
  73 char *pcNondetSetString( size_t xStringLength )
  74 {
  75         char *pcName = pvPortMalloc( xStringLength );
  76
  77         if ( pcName != NULL ) {
  78                 size_t uNondetIndex;
  79                 __CPROVER_assume( uNondetIndex < xStringLength );
  80                 pcName[uNondetIndex] = '\0';
  81         }
  82
  83         return pcName;
  84 }