/* 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 "cbmc.h" /**************************************************************** * Signature of function under test ****************************************************************/ BaseType_t prvCheckOptions( FreeRTOS_Socket_t * pxSocket, const NetworkBufferDescriptor_t * pxNetworkBuffer ); size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ); int32_t __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, size_t uxTotalLength, FreeRTOS_Socket_t * const pxSocket, BaseType_t xHasSYNFlag ); /**************************************************************** * Declare the buffer size external to the harness so it can be * accessed by the preconditions of prvSingleStepTCPHeaderOptions, and * give the buffer size an unconstrained value in the harness itself. ****************************************************************/ size_t buffer_size; size_t uxIPHeaderSizePacket_uxResult; /**************************************************************** * Function contract proved correct by CheckOptionsOuter ****************************************************************/ int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr, size_t uxTotalLength, FreeRTOS_Socket_t * const pxSocket, BaseType_t xHasSYNFlag ) { /* CBMC model of pointers limits the size of the buffer */ /* Preconditions */ __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, "prvSingleStepTCPHeaderOptions: buffer_size < CBMC_MAX_OBJECT_SIZE" ); __CPROVER_assert( 8 <= buffer_size, "prvSingleStepTCPHeaderOptions: 8 <= buffer_size" ); __CPROVER_assert( pucPtr != NULL, "prvSingleStepTCPHeaderOptions: pucPtr != NULL" ); __CPROVER_assert( uxTotalLength <= buffer_size, "prvSingleStepTCPHeaderOptions: uxTotalLength <= buffer_size" ); __CPROVER_assert( pxSocket != NULL, "prvSingleStepTCPHeaderOptions: pxSocket != NULL" ); /* Postconditions */ int32_t index; __CPROVER_assume( ( index == -1 ) || ( index == 1 ) || ( index <= uxTotalLength ) ); return index; } size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) { __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer shouldnt be NULL" ); return uxIPHeaderSizePacket_uxResult; } /**************************************************************** * Proof of CheckOptions ****************************************************************/ void harness() { /* Give buffer_size an unconstrained value */ size_t buf_size; if( nondet_bool() ) { uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv6_HEADER; } else { uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv4_HEADER; } __CPROVER_assume( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) ); buffer_size = buf_size; /* pxSocket can be any socket */ FreeRTOS_Socket_t pxSocket; /* 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; /**************************************************************** * Specification and proof of CheckOptions ****************************************************************/ /* CBMC model of pointers limits the size of the buffer */ __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); /* Bound required to bound iteration over the buffer */ __CPROVER_assume( buffer_size <= BUFFER_SIZE ); /* Buffer must be big enough to hold pxTCPPacket and pxTCPHeader */ __CPROVER_assume( buffer_size > 47 ); prvCheckOptions( &pxSocket, &pxNetworkBuffer ); }