3 files changed, 38 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
new file mode 100644
index 000000000..f2d8e61ae
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -0,0 +1,15 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "queue.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_ARP.h"
+
+void harness()
+{
+  ARPPacket_t xARPFrame;
+
+  eARPProcessPacket( &xARPFrame );
+}
+\ No newline at end of file
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json
new file mode 100644
index 000000000..48d5d83c9
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json
@@ -0,0 +1,19 @@
+{
+  "ENTRY": "ARPProcessPacket",
+  "CBMCFLAGS":
+  [
+      "--unwind 1",
+      "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
+      "--nondet-static"
+  ],
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto"
+  ],
+  "DEF":
+  [
+    {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]},
+    {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]}
+  ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md
new file mode 100644
index 000000000..0197851b1
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md
@@ -0,0 +1,4 @@
+The proofs in the subdirectories show that
+ARPProcessPacket is memory safe independent
+of the configuration value of
+ipconfigARP_USE_CLASH_DETECTION.
+\ No newline at end of file