len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-16 09:47:44 -04:00
Code Issues Projects Releases Packages Wiki Activity

CBMC proof for ulARPRemoveCacheEntryByMac (#198)

Browse source 
* 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
This commit is contained in:
Aniruddha Kanhere 2020-08-24 16:46:50 -07:00 • committed by GitHub
parent 6eba275f89
commit 3c573ad091
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 43 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

24
FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json Normal file
View file

@ -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"
]
}

19
FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c Normal file
View file

@ -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 );
}