1 files changed, 49 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md
new file mode 100644
index 000000000..5d509a7e8
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md
@@ -0,0 +1,49 @@
+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.