blob: d9b79a1f46b55272cda84e5f172c553561c122a1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
This proof demonstrates the memory safety of the TaskPrioritySet function. The
initialization for the task to be set and `pxCurrentTCB` is quite similar
(since the task handle may be NULL, and in that case `pxCurrentTCB` is used).
Task lists are initialized with these tasks and nondet. filled with a few more
items.
This proof is a work-in-progress. Proof assumptions are described in
the harness. The proof also assumes the following functions are
memory safe and have no side effects relevant to the memory safety of
this function:
* vPortEnterCritical
* vPortExitCritical
* vPortGenerateSimulatedInterrupt
|
