blob: 4682310df5302cc9656237f696c8e13101384a00 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
This is the memory safety proof for xSendEventToIPTask, a function used
for sending different events to IP-Task. We have abstracted away queues.
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:
* uxQueueMessagesWaiting
* xQueueGenericSend
The coverage is imperfect (97%) because xSendEventToIPTask always
calls xSendEventStructToIPTask with xTimeout==0.
|
