FreeRTOS-Kernel/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2

This is the memory safety proof for FreeRTOS_OutputARPRequest method combined with the BufferAllocation_2.c allocation strategy.

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:

• vPortEnterCritical

• vPortExitCritical

• vPortGenerateSimulatedInterrupt

• vAssertCalled

• xTaskGetSchedulerState

• pvTaskIncrementMutexHeldCount

• xTaskRemoveFromEventList

• xTaskPriorityDisinherit

• pvPortMalloc

• pvPortFree

• xNetworkInterfaceOutput

• vNetworkInterfaceAllocateRAMToBuffers

This proof disables the tracing library in the header.

This proof checks FreeRTOS_OutputARPRequest in multiple configuration:

• The proof in the directory config_minimal_configuration guarantees that the implementation and interaction between FreeRTOS_OutputARPRequest and FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c are memory save. This proof depends entirely of the implementation correctness of vNetworkInterfaceAllocateRAMToBuffers.
• The proof in directory minimal_configuration_minimal_packet_size guarantees that using FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ).
• The directory minimal_configuration_minimal_packet_size_no_tcp reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c allocator.
• The proof in directory config_minimal_configuration_linked_rx_messages guarantees that the ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the memory safety claim.

All harnesses include the queue.c file, but test only for the happy path.