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

   1 Assuming the parameter passed to QueueMessagesWaiting is a pointer to a Queue_t
   2 struct, this harness proves the memory safety of QueueMessagesWaiting.
   3 The concurrency related functions vPortEnterCrititcal and vPortExitCritical
   4 are abstracted away.
   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 * vPortEnterCritical
  12 * vPortExitCritical