From 3c573ad0913fc271e7aedebe5c9708eb9c58e5a3 Mon Sep 17 00:00:00 2001
From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Mon, 24 Aug 2020 16:46:50 -0700
Subject: [PATCH] CBMC proof for ulARPRemoveCacheEntryByMac (#198)
* Add Proof
* update
* Delete ulARPRemoveCacheEntryByMAC_harness.c
* Changes after Mark's comments
* Update after @yanjos-dev's comment
* Remove confusing variable name
* Update ulARPRemoveCacheEntryByMac_harness.c
---
.../ulARPRemoveCacheEntryByMac/Makefile.json | 24 +++++++++++++++++++
.../ulARPRemoveCacheEntryByMac_harness.c | 19 +++++++++++++++
2 files changed, 43 insertions(+)
create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json
create mode 100644 FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json
new file mode 100644
index 0000000000..fbbf00d79d
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json
@@ -0,0 +1,24 @@
+{
+ "ENTRY": "ulARPRemoveCacheEntryByMac",
+ "NUMBER_OF_CACHE_ENTRIES":6,
+ "CBMCFLAGS":
+ [
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto"
+ ],
+ "INSTFLAGS":
+ [
+ ],
+ "DEF":
+ [
+ "ipconfigUSE_ARP_REMOVE_ENTRY=1",
+ "ipconfigARP_CACHE_ENTRIES={NUMBER_OF_CACHE_ENTRIES}"
+ ],
+ "INC":
+ [
+ "$(FREERTOS)/tools/cbmc/include"
+ ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c
new file mode 100644
index 0000000000..dc71cb65f4
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c
@@ -0,0 +1,19 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_ARP.h"
+
+
+void harness() {
+ const MACAddress_t xMACAddress;
+
+ /* The pointer passed to ulARPRemoveCacheEntryByMac cannot be NULL
+ * (see the API definition). */
+ ulARPRemoveCacheEntryByMac( &xMACAddress );
+}