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

   1 This proof demonstrates the memory safety of the TaskSwitchContext function.
   2 We assume task ready lists to be initialized and filled with one element each,
   3 and `pxCurrentTCB` to be the highest priority task.  We also set
   4 `uxSchedulerSuspended` to a nondeterministic value.
   5
   6 This proof is a work-in-progress.  Proof assumptions are described in
   7 the harness.  The proof also assumes the following functions are
   8 memory safe and have no side effects relevant to the memory safety of
   9 this function:
  10
  11 * prvTraceGetCurrentTaskHandle
  12 * prvTraceGetTaskNumber
  13 * prvTraceStoreTaskswitch
  14 * ulGetRunTimeCounterValue