xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md (revision dfe2e90ad7488c5ecfea69e095105e590f2ab006) 
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