blob: 8a868dda10039585324c2336ca09929cba6d3827 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
This is the memory safety proof for FreeRTOS_OutputARPRequest.
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:
* xNetworkInterfaceOutput
This proof checks FreeRTOS_OutputARPRequest in multiple configuration:
* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof
guarantees that for a buffer allocated to xDataLength,
the code executed by the FreeRTOS_OutputARPRequest function
call of FreeRTOS_ARP.c is memory safe.
* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the
buffer allocated by pxGetNetworkBufferWithDescriptor allocates
a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES,
the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof
guarantees that the code executed by the
FreeRTOS_OutputARPRequest function call
of FreeRTOS_ARP.c is memory safe.
* The third configuration in the subdirectory
config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates
that the code is not memory safe, if the allocation
code violates our assumption.
* All proofs mock the pxGetNetworkBufferWithDescriptor
function for modelling the assumptions about the
buffer management layer.
|
