len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-15 17:27:46 -04:00
Code Issues Projects Releases Packages Wiki Activity

CBMC proof for vProcessGeneratedUDPPacket (#203)

Browse source 
* Add Proof

* Update

* Update the proof

* Update the proof

* Clean-up

* Clean-up v2

* Update freertos_api.c

* update stub
This commit is contained in:
Aniruddha Kanhere 2020-08-24 17:06:31 -07:00 • committed by GitHub
parent 3c573ad091
commit 86117b5173
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 130 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c
View file

@ -377,3 +377,20 @@ const char * pcApplicationHostnameHook( void )
}
/****************************************************************/
/****************************************************************
* Abstract xNetworkInterfaceOutput
* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html#xNetworkInterfaceOutput
****************************************************************/
BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkBuffer, BaseType_t bReleaseAfterSend )
{
__CPROVER_assert( pxNetworkBuffer != NULL, "The networkbuffer cannot be NULL" );
BaseType_t xReturn;
/* Return some random value. */
return xReturn;
}
/****************************************************************/