FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md


1
2
3
4
5
6

Abstracting xQueueGenericSend away
and including tasks.c and FreeRTOS_IP.c:
The ARPSendGratutious function is memory safe,
if xQueueGenericSend is memory safe.

queue.c is not compiled into the proof binary.