espressif/FreeRTOS
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS.git synced 2025-06-04 04:56:47 +08:00
Code Issues Packages Projects Releases Wiki Activity

Add CBMC proof for prvProcessEthernetPacket (#199)

Browse Source 
* Add proof

* Remove and Rename files

* Modify the makefile

* Update Makefile.json

* Add _static to FreeRTOS_IP.c

* Update prvProcessEthernetPacket_harness.c

* Update the proof and add list to stubs

* add assertions

* Update the proof

* cleanup

* Update

* Update after @yanjos-dev's comment

* Remove unnecessary assumption
This commit is contained in:
Aniruddha Kanhere
2020-08-27 16:25:17 -07:00
committed by GitHub
parent 0b48e6a3b5
commit 66371d0cf0
3 changed files with 97 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

32
FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/Makefile.json Normal file
View File

@ -0,0 +1,32 @@
{
"ENTRY": "prvProcessEthernetPacket",
"CBMCFLAGS":
[
"--unwind 1",
"--unwindset prvTCPSendRepeated.0:13",
"--nondet-static",
"--flush"
],
"OBJS":
[
"$(ENTRY)_harness.goto",
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto"
],
"INSTFLAGS":
[
],
"OPT":
[
"--export-file-local-symbols"
],
"DEF":
[
"FREERTOS_TCP_ENABLE_VERIFICATION"
],
"INC":
[
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility",
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/stubs"
]
}

63
FreeRTOS-Plus/Test/CBMC/proofs/prvProcessEthernetPacket/prvProcessEthernetPacket_harness.c Normal file
View File

@ -0,0 +1,63 @@
/* Standard includes. */
#include <stdint.h>
#include <stdio.h>
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "task.h"
#include "queue.h"
#include "semphr.h"
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_Sockets.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_UDP_IP.h"
#include "FreeRTOS_DHCP.h"
#include "NetworkInterface.h"
#include "NetworkBufferManagement.h"
#include "FreeRTOS_ARP.h"
#include "memory_assignments.c"
#include "freertos_api.c"
/****************************************************************
* Signature of function under test
****************************************************************/
void __CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( NetworkBufferDescriptor_t * const pxNetworkBuffer );
/* This function has been proved to be memory safe in another proof (in ARP/ARPRefreshCacheEntry). Hence we assume it to be correct here. */
void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress )
{
/* pxMACAddress can be NULL or non-NULL. No need to assert. */
}
/* This function has been proved to be memory safe in another proof (in ARP/ARPProcessPacket). Hence we assume it to be correct here. */
eFrameProcessingResult_t eARPProcessPacket( ARPPacket_t * const pxARPFrame )
{
__CPROVER_assert( pxARPFrame != NULL, "pxARPFrame cannot be NULL" );
eFrameProcessingResult_t eReturn;
return eReturn;
}
/* This function has been proved to be memory safe in another proof (in parsing/ProcessIPPacket). Hence we assume it to be correct here. */
eFrameProcessingResult_t __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( IPPacket_t * pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
__CPROVER_assert( pxIPPacket != NULL, "pxIPPacket cannot be NULL" );
__CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
eFrameProcessingResult_t result;
return result;
}
void harness() {
NetworkBufferDescriptor_t * const pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ipTOTAL_ETHERNET_FRAME_SIZE, 0 );
/* The network buffer cannot be NULL for this function call. If it is, it will hit an assert in the function. */
__CPROVER_assume( pxNetworkBuffer != NULL );
__CPROVER_file_local_FreeRTOS_IP_c_prvProcessEthernetPacket( pxNetworkBuffer );
}

2
FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
View File

@ -1,3 +1,5 @@
#include <stdlib.h>
#define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length)
/* Implementation of safe malloc which returns NULL if the requested size is 0.