blob: 3aa4e5e935d21c217c6e08165350e461b22d38b4 (
plain)
1
2
3
4
5
|
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.
|