6 lines
225 B
Markdown
6 lines
225 B
Markdown
Assuming that xSemaphore is a pointer to an allocated Queue_t instance,
|
|
this harness proves the memory safety of QueueGetMutexHolderFromISR.
|
|
|
|
This proof is a work-in-progress. Proof assumptions are described in
|
|
the harness.
|