1 files changed, 27 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
new file mode 100644
index 000000000..ea5eac78d
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
@@ -0,0 +1,27 @@
+This is the memory safety proof for ```FreeRTOS_OutputARPRequest```
+method combined with the BufferAllocation_1.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
+
+This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations.
+All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers.
+* The ```config_minimal_configuration``` proof sets
+  ```ipconfigUSE_LINKED_RX_MESSAGES=0```.
+* The ```config_minimal_configuration_linked_rx_messages``` proof sets
+  ```ipconfigUSE_LINKED_RX_MESSAGES=1```.
+* The ```minimal_configuration_minimal_packet_size``` proof sets
+  ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50.
+
+All harnesses include the queue.c file, but test only for the happy path.