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

   1 This proof demonstrates the memory safety of the TaskGetTaskNumber function.
   2 No assumption is required since the function accepts a NULL value for the task handle.
   3
   4 This proof is a work-in-progress.  Proof assumptions are described in
   5 the harness.