1 files changed, 22 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
new file mode 100644
index 000000000..523783564
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -0,0 +1,22 @@
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "list.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_ARP.h"
+
+//We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure.
+//This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof.
+NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){
+	NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t));
+	pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes);
+	pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
+	return pxNetworkBuffer;
+}
+
+void harness()
+{
+  vARPAgeCache();
+}
+\ No newline at end of file