README.md
1This is the memory safety proof for FreeRTOS_OutputARPRequest
2method combined with the BufferAllocation_2.c allocation strategy.
3
4This proof is a work-in-progress. Proof assumptions are described in
5the harness. The proof also assumes the following functions are
6memory safe and have no side effects relevant to the memory safety of
7this function:
8
9* vPortEnterCritical
10* vPortExitCritical
11* vPortGenerateSimulatedInterrupt
12* vAssertCalled
13* xTaskGetSchedulerState
14* pvTaskIncrementMutexHeldCount
15* xTaskRemoveFromEventList
16* xTaskPriorityDisinherit
17
18* pvPortMalloc
19* pvPortFree
20* xNetworkInterfaceOutput
21* vNetworkInterfaceAllocateRAMToBuffers
22
23This proof disables the tracing library in the header.
24
25This proof checks FreeRTOS_OutputARPRequest in multiple configuration:
26
27* The proof in the directory config_minimal_configuration guarantees
28 that the implementation and interaction between
29 FreeRTOS_OutputARPRequest and
30 FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
31 are memory save. This proof depends entirely of the implementation
32 correctness of vNetworkInterfaceAllocateRAMToBuffers.
33* The proof in directory minimal_configuration_minimal_packet_size
34 guarantees that using
35 FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
36 along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save
37 as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and
38 ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ).
39* The directory minimal_configuration_minimal_packet_size_no_tcp
40 reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used
41 if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the
42 FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c
43 allocator.
44* The proof in directory
45 config_minimal_configuration_linked_rx_messages guarantees that the
46 ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the
47 memory safety claim.
48
49All harnesses include the queue.c file, but test only for the happy path.
50
