diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c index 5237835649..5a97b9ba92 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -10,13 +10,16 @@ //We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. //This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof. NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ - NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); - pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); - pxNetworkBuffer->xDataLength = xRequestedSizeBytes; - return pxNetworkBuffer; + NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); + __CPROVER_assume(pxNetworkBuffer != NULL); // network buffer cannot be null + pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer != NULL); // ethernet buffer cannot be null + + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; } void harness() { vARPAgeCache(); -} \ No newline at end of file +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c index 3ec9500cc3..bbfadfb885 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -9,20 +9,21 @@ void harness() { - /* - * The assumption made here is that the buffer pointed by pucEthernerBuffer - * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. - * This is not checked inside vARPGenerateRequestPacket. - */ - uint8_t ucBUFFER_SIZE; - __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); - void *xBuffer = malloc(ucBUFFER_SIZE); + /* + * The assumption made here is that the buffer pointed by pucEthernerBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. + * This is not checked inside vARPGenerateRequestPacket. + */ + uint8_t ucBUFFER_SIZE; + __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); + void *xBuffer = malloc(ucBUFFER_SIZE); + __CPROVER_assume(xBuffer != NULL); - NetworkBufferDescriptor_t xNetworkBuffer2; - xNetworkBuffer2.pucEthernetBuffer = xBuffer; - xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; + NetworkBufferDescriptor_t xNetworkBuffer2; + xNetworkBuffer2.pucEthernetBuffer = xBuffer; + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; - /* vARPGenerateRequestPacket asserts buffer has room for a packet */ - __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); - vARPGenerateRequestPacket( &xNetworkBuffer2 ); + /* vARPGenerateRequestPacket asserts buffer has room for a packet */ + __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); + vARPGenerateRequestPacket( &xNetworkBuffer2 ); } diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c index 17a12fc49e..cf2e680f85 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -52,25 +52,27 @@ NetworkBufferDescriptor_t xNetworkBuffer; * of an ARPPacket to guarantee memory safety. */ NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ - #ifdef CBMC_PROOF_ASSUMPTION_HOLDS - #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES - xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); - #else - xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); - #endif - #else - uint32_t malloc_size; - __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); - __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); - xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); - #endif - xNetworkBuffer.xDataLength = xRequestedSizeBytes; - return &xNetworkBuffer; + #ifdef CBMC_PROOF_ASSUMPTION_HOLDS + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); + #else + xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); + #endif + #else + uint32_t malloc_size; + __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); + __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); + xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); + #endif + __CPROVER_assume(xNetworkBuffer.pucEthernetBuffer != NULL); + + xNetworkBuffer.xDataLength = xRequestedSizeBytes; + return &xNetworkBuffer; } void harness() { - uint32_t ulIPAddress; - FreeRTOS_OutputARPRequest( ulIPAddress ); + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); } diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c index 3dae34a341..b08ca53717 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -18,21 +18,22 @@ #include "FreeRTOS_UDP_IP.h" #include "FreeRTOS_DHCP.h" #if( ipconfigUSE_LLMNR == 1 ) - #include "FreeRTOS_DNS.h" + #include "FreeRTOS_DNS.h" #endif /* ipconfigUSE_LLMNR */ #include "NetworkInterface.h" #include "NetworkBufferManagement.h" void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){ - for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ - NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; - #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES - current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); - #else - current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); - #endif - current->xDataLength = sizeof(ARPPacket_t); - } + for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ + NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); + #else + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); + #endif + __CPROVER_assume(current->pucEthernetBuffer != NULL); + current->xDataLength = sizeof(ARPPacket_t); + } } /* The code expects that the Semaphore creation relying on pvPortMalloc @@ -44,7 +45,9 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB after removing the assert in l.105 of BufferAllocation_1.c, from a memory safety point of view. */ void *pvPortMalloc( size_t xWantedSize ){ - return malloc(xWantedSize); + void *ptr = malloc(xWantedSize); + __CPROVER_assume(ptr != NULL); + return ptr; } /* @@ -55,17 +58,17 @@ void *pvPortMalloc( size_t xWantedSize ){ * how to write this code out to the network. */ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ - if( bReleaseAfterSend != pdFALSE ) - { - vReleaseNetworkBufferAndDescriptor( pxDescriptor ); - } + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } } void harness() { - BaseType_t xRes = xNetworkBuffersInitialise(); - if(xRes == pdPASS){ - uint32_t ulIPAddress; - FreeRTOS_OutputARPRequest( ulIPAddress ); - } + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } } diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c index c047a27608..e97d187067 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -18,18 +18,20 @@ #include "FreeRTOS_UDP_IP.h" #include "FreeRTOS_DHCP.h" #if( ipconfigUSE_LLMNR == 1 ) - #include "FreeRTOS_DNS.h" + #include "FreeRTOS_DNS.h" #endif /* ipconfigUSE_LLMNR */ #include "NetworkInterface.h" #include "NetworkBufferManagement.h" void *pvPortMalloc( size_t xWantedSize ){ - return malloc(xWantedSize); + void *ptr = malloc(xWantedSize); + __CPROVER_assume(ptr != NULL); + return ptr; } void vPortFree( void *pv ){ - free(pv); + free(pv); } /* @@ -37,18 +39,17 @@ void vPortFree( void *pv ){ * out here, and assume it has no side effects relevant to memory safety. */ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ - if( bReleaseAfterSend != pdFALSE ) - { - vReleaseNetworkBufferAndDescriptor( pxDescriptor ); - } + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } } void harness() { - BaseType_t xRes = xNetworkBuffersInitialise(); - if(xRes == pdPASS){ - uint32_t ulIPAddress; - FreeRTOS_OutputARPRequest( ulIPAddress ); - } + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } } - diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c index fd0900c5ea..83f05ad48d 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c @@ -81,6 +81,7 @@ void harness() /* pxNetworkBuffer can be any buffer descriptor with any buffer */ NetworkBufferDescriptor_t pxNetworkBuffer; pxNetworkBuffer.pucEthernetBuffer = malloc( buffer_size ); + __CPROVER_assume(pxNetworkBuffer.pucEthernetBuffer != NULL); pxNetworkBuffer.xDataLength = buffer_size; /**************************************************************** diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c index bca2b17920..a7f07746d3 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -37,20 +37,24 @@ void harness() /* pucPtr points into a buffer */ size_t buffer_size; uint8_t * pucPtr = malloc( buffer_size ); + __CPROVER_assume(pucPtr != NULL); /* uxIndex in an index into the buffer */ size_t uxIndex; /* pxSocket can be any socket with some initialized values */ FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + __CPROVER_assume(pxSocket != NULL); pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) ); + __CPROVER_assume(pxSocket->u.xTCP.txStream != NULL); vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue ); if( nondet_bool() ) { TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume(segment != NULL); listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue, &segment->xQueueItem ); } @@ -60,6 +64,7 @@ void harness() if( nondet_bool() ) { TCPSegment_t * segment = malloc( sizeof( TCPSegment_t ) ); + __CPROVER_assume(segment != NULL); vListInitialiseItem( &segment->xSegmentItem ); listSET_LIST_ITEM_OWNER( &segment->xQueueItem, ( void * ) segment ); vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xTxSegments, &segment->xQueueItem ); diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c index b8833fc79e..66a411622f 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c @@ -72,8 +72,10 @@ void harness() buffer_size = buf_size; uint8_t * pucPtr = malloc( buffer_size ); + __CPROVER_assume(pucPtr != NULL); size_t uxTotalLength; FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) ); + __CPROVER_assume(pxSocket != NULL); BaseType_t xHasSYNFlag; /**************************************************************** diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c index d9c7c9b3aa..a49e003825 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c @@ -15,14 +15,14 @@ uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol ) { - uint16_t usResult; - return usResult; + uint16_t usResult; + return usResult; } BaseType_t xIPIsNetworkTaskReady( void ) { - /* Return true saying that the task is ready. */ - return pdTRUE; + /* Return true saying that the task is ready. */ + return pdTRUE; } @@ -46,21 +46,22 @@ BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber ) void harness() { - FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - __CPROVER_assume( pxSocket != NULL ); - __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET ); + __CPROVER_assume( pxSocket != NULL ); + __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET ); - /* malloc instead of safeMalloc since we do not allow socket without binding. */ - struct freertos_sockaddr * pxBindAddress = malloc( sizeof( struct freertos_sockaddr ) ); + /* malloc instead of safeMalloc since we do not allow socket without binding. */ + struct freertos_sockaddr * pxBindAddress = malloc( sizeof( struct freertos_sockaddr ) ); + __CPROVER_assume(pxBindAddress != NULL); - /* uxAddressLength is not used in this implementation. */ - size_t uxAddressLength; + /* uxAddressLength is not used in this implementation. */ + size_t uxAddressLength; - BaseType_t xInternal; + BaseType_t xInternal; - /* Call to init the socket list. */ - vNetworkSocketsInit(); + /* Call to init the socket list. */ + vNetworkSocketsInit(); - vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal ); + vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal ); } diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c index 9c41d7b7f5..6be896a421 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -43,30 +43,32 @@ int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescript /* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */ NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ - NetworkBufferDescriptor_t *pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated (); - size_t bufferSize = sizeof(NetworkBufferDescriptor_t); - if (ensure_memory_is_valid(pxBuffer, bufferSize)) { - /* The code does not expect pucEthernetBuffer to be equal to NULL if - pxBuffer is not NULL. */ - pxBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); - pxBuffer->xDataLength = xRequestedSizeBytes; - } - return pxBuffer; + NetworkBufferDescriptor_t *pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated (); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if (ensure_memory_is_valid(pxBuffer, bufferSize)) { + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxBuffer is not NULL. */ + pxBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + __CPROVER_assume(pxBuffer->pucEthernetBuffer != NULL); + pxBuffer->xDataLength = xRequestedSizeBytes; + } + return pxBuffer; } void harness() { - FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); - NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); - size_t socketSize = sizeof(FreeRTOS_Socket_t); - size_t bufferSize = sizeof(TCPPacket_t); - if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { - pxNetworkBuffer->xDataLength = bufferSize; - /* The code does not expect pucEthernetBuffer to be equal to NULL if - pxNetworkBuffer is not NULL. */ - pxNetworkBuffer->pucEthernetBuffer = malloc(bufferSize); - } - UBaseType_t uxOptionsLength; - if(pxSocket) { - publicTCPPrepareSend(pxSocket, &pxNetworkBuffer, uxOptionsLength ); - } + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + size_t bufferSize = sizeof(TCPPacket_t); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->xDataLength = bufferSize; + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxNetworkBuffer is not NULL. */ + pxNetworkBuffer->pucEthernetBuffer = malloc(bufferSize); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer != NULL); + } + UBaseType_t uxOptionsLength; + if(pxSocket) { + publicTCPPrepareSend(pxSocket, &pxNetworkBuffer, uxOptionsLength ); + } } diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c index def244a51a..cace50074b 100644 --- a/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c +++ b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -19,11 +19,18 @@ eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, N void harness() { - NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t)); - /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ - pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE); - /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ - __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE); - IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t)); - publicProcessIPPacket(pxIPPacket, pxNetworkBuffer); + NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t)); + __CPROVER_assume(pxNetworkBuffer != NULL); + + /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ + pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer != NULL); + + /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ + __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE); + + IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t)); + __CPROVER_assume(pxIPPacket != NULL); + + publicProcessIPPacket(pxIPPacket, pxNetworkBuffer); } diff --git a/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c b/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c index cb63e7cc8c..1f8d4413f7 100644 --- a/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c +++ b/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c @@ -37,8 +37,13 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol ) { - return nondet_bool() ? - FREERTOS_INVALID_SOCKET : malloc( sizeof( Socket_t ) ); + if ( nondet_bool() ) { + return FREERTOS_INVALID_SOCKET; + } + + void *ptr = malloc( sizeof( Socket_t ) ); + __CPROVER_assume( ptr != NULL ); + return ptr; } /**************************************************************** @@ -142,7 +147,7 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket, size_t payload_size; __CPROVER_assume( payload_size + sizeof( UDPPacket_t ) - < CBMC_MAX_OBJECT_SIZE ); + < CBMC_MAX_OBJECT_SIZE ); /**************************************************************** * TODO: We need to make this lower bound explicit in the Makefile.json @@ -158,7 +163,7 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket, uint32_t buffer_size = payload_size + sizeof( UDPPacket_t ); uint8_t *buffer = safeMalloc( buffer_size ); - + if ( buffer == NULL ) { buffer_size = 0; } @@ -167,7 +172,7 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket, buffer = buffer + sizeof( UDPPacket_t ); buffer_size = buffer_size - sizeof( UDPPacket_t ); } - + *( ( uint8_t ** ) pvBuffer ) = buffer; return buffer_size; } @@ -224,7 +229,7 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer ) __CPROVER_assert( pvBuffer != NULL, "FreeRTOS precondition: pvBuffer != NULL" ); __CPROVER_assert( __CPROVER_POINTER_OFFSET( pvBuffer ) - == sizeof( UDPPacket_t ), + == sizeof( UDPPacket_t ), "FreeRTOS precondition: pvBuffer offset" ); free( pvBuffer - sizeof( UDPPacket_t ) ); @@ -271,9 +276,9 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS */ GetNetworkBuffer_failure_count++; __CPROVER_assume( - IMPLIES( - GetNetworkBuffer_failure_count >= CBMC_GETNETWORKBUFFER_FAILURE_BOUND, - desc != NULL ) ); + IMPLIES( + GetNetworkBuffer_failure_count >= CBMC_GETNETWORKBUFFER_FAILURE_BOUND, + desc != NULL ) ); #endif if( desc != NULL ) @@ -294,8 +299,8 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS __CPROVER_assume( desc->pucEthernetBuffer != NULL ); #endif - /* Allow method to fail again next time */ - GetNetworkBuffer_failure_count = 0; + /* Allow method to fail again next time */ + GetNetworkBuffer_failure_count = 0; } return desc; @@ -387,7 +392,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB { __CPROVER_assert( pxNetworkBuffer != NULL, "The networkbuffer cannot be NULL" ); - BaseType_t xReturn; + BaseType_t xReturn; /* Return some random value. */ return xReturn;