diff options
| author | Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> | 2020-08-24 16:46:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-24 16:46:50 -0700 |
| commit | 3c573ad0913fc271e7aedebe5c9708eb9c58e5a3 (patch) | |
| tree | 5c758179a8baa1837d6436aa5fc08ab19acd0a0d | |
| parent | 6eba275f8902aba010adc53150d4e5a8f9e45809 (diff) | |
| download | freertos-git-3c573ad0913fc271e7aedebe5c9708eb9c58e5a3.tar.gz | |
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
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json | 24 | ||||
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c | 19 |
2 files changed, 43 insertions, 0 deletions
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 000000000..fbbf00d79 --- /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 000000000..dc71cb65f --- /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 ); +} |