begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/Task/TaskCreate/README.md

   1 This proof demonstrates the memory safety of the TaskCreate function.
   2 We initialize task lists, but we set other data structures to
   3 unconstrained (arbitrary) values, including the data structures
   4 `pxCurrentTCB`, `uxCurrentNumberOfTasks`, `pcName` and `pxCreateTask`.
   5 STACK_DEPTH is set to a fixed number (10) since it is not possible to
   6 specify a range.
   7
   8 This proof is a work-in-progress.  Proof assumptions are described in
   9 the harness.  The proof also assumes the following functions are
  10 memory safe and have no side effects relevant to the memory safety of
  11 this function:
  12
  13 * prvTraceGetObjectHandle
  14 * prvTraceGetTaskNumber
  15 * prvTraceSetObjectName
  16 * prvTraceSetPriorityProperty
  17 * prvTraceStoreKernelCall
  18 * prvTraceStoreTaskReady
  19 * pxPortInitialiseStack
  20 * vPortEnterCritical
  21 * vPortExitCritical
  22 * vPortGenerateSimulatedInterrupt