begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/README.md

   1 This harness proves the memory safety of the prvNotifyQueuSetContainer method.
   2 It assumes that the queue is initalized to a valid datastructure and added
   3 to a QueueSet. The concurrency functions and task pool functions are abstracted
   4 away. prvCopyDataToQueue is replaced with a stub checking the preconditions
   5 for prvCopyDataToQueue to be sucessful.
   6
   7 This proof is a work-in-progress.  Proof assumptions are described in
   8 the harness.  The proof also assumes the following functions are
   9 memory safe and have no side effects relevant to the memory safety of
  10 this function:
  11
  12 * vPortEnterCritical
  13 * vPortExitCritical
  14 * xTaskRemoveFromEventList