README.md
1This is the memory safety proof for FreeRTOS_OutputARPRequest.
2
3This proof is a work-in-progress. Proof assumptions are described in
4the harness. The proof also assumes the following functions are
5memory safe and have no side effects relevant to the memory safety of
6this function:
7
8* xNetworkInterfaceOutput
9
10This proof checks FreeRTOS_OutputARPRequest in multiple configuration:
11
12* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof
13 guarantees that for a buffer allocated to xDataLength,
14 the code executed by the FreeRTOS_OutputARPRequest function
15 call of FreeRTOS_ARP.c is memory safe.
16* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the
17 buffer allocated by pxGetNetworkBufferWithDescriptor allocates
18 a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES,
19 the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof
20 guarantees that the code executed by the
21 FreeRTOS_OutputARPRequest function call
22 of FreeRTOS_ARP.c is memory safe.
23* The third configuration in the subdirectory
24 config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates
25 that the code is not memory safe, if the allocation
26 code violates our assumption.
27* All proofs mock the pxGetNetworkBufferWithDescriptor
28 function for modelling the assumptions about the
29 buffer management layer.
30
