6 lines
229 B
Markdown
6 lines
229 B
Markdown
This proof demonstrates the memory safety of the TaskSuspendAll function.
|
|
No assumption or abstraction is required for this memory-safety proof.
|
|
|
|
This proof is a work-in-progress. Proof assumptions are described in
|
|
the harness.
|