From c80540ccf3818a5f638055267cee74deae89ab9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?B=C5=82a=C5=BCej=20Sowa?= Date: Thu, 23 Nov 2023 12:31:37 +0100 Subject: [PATCH 1/8] Fix issue with strncpy truncating null character from source string --- source/FreeRTOS_DNS.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 9fb62a196..899e47978 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -282,7 +282,8 @@ ( void ) memset( pxAddrInfo, 0, sizeof( *pxAddrInfo ) ); pxAddrInfo->ai_canonname = pxAddrInfo->xPrivateStorage.ucName; - ( void ) strncpy( pxAddrInfo->xPrivateStorage.ucName, pcName, sizeof( pxAddrInfo->xPrivateStorage.ucName ) ); + ( void ) strncpy( pxAddrInfo->xPrivateStorage.ucName, pcName, sizeof( pxAddrInfo->xPrivateStorage.ucName ) - 1 ); + pxAddrInfo->xPrivateStorage.ucName[ sizeof( pxAddrInfo->xPrivateStorage.ucName ) - 1 ] = '\0'; pxAddrInfo->ai_addr = ( ( struct freertos_sockaddr * ) &( pxAddrInfo->xPrivateStorage.sockaddr ) ); From 8133702da8a38dcd78dae21a2b23e2b9a3f716fd Mon Sep 17 00:00:00 2001 From: microcris <31326314+microcris@users.noreply.github.com> Date: Thu, 30 Nov 2023 17:00:47 +0000 Subject: [PATCH 2/8] Update FreeRTOS_debug_printf in ipARP_REPLY (#1048) Replace ipconfigHAS_PRINTF by FreeRTOS_debug_printf in the ipARP_REPLY debug print --- source/FreeRTOS_ARP.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/source/FreeRTOS_ARP.c b/source/FreeRTOS_ARP.c index cc24dbfb7..5a84cd60b 100644 --- a/source/FreeRTOS_ARP.c +++ b/source/FreeRTOS_ARP.c @@ -259,13 +259,13 @@ static TickType_t xLastGratuitousARPTime = 0U; traceARP_PACKET_RECEIVED(); /* Some extra logging while still testing. */ - #if ( ipconfigHAS_PRINTF != 0 ) + #if ( ipconfigHAS_DEBUG_PRINTF != 0 ) if( pxARPHeader->usOperation == ( uint16_t ) ipARP_REPLY ) { - FreeRTOS_printf( ( "ipARP_REPLY from %xip to %xip end-point %xip\n", - ( unsigned ) FreeRTOS_ntohl( ulSenderProtocolAddress ), - ( unsigned ) FreeRTOS_ntohl( ulTargetProtocolAddress ), - ( unsigned ) FreeRTOS_ntohl( ( pxTargetEndPoint != NULL ) ? pxTargetEndPoint->ipv4_settings.ulIPAddress : 0U ) ) ); + FreeRTOS_debug_printf( ( "ipARP_REPLY from %xip to %xip end-point %xip\n", + ( unsigned ) FreeRTOS_ntohl( ulSenderProtocolAddress ), + ( unsigned ) FreeRTOS_ntohl( ulTargetProtocolAddress ), + ( unsigned ) FreeRTOS_ntohl( ( pxTargetEndPoint != NULL ) ? pxTargetEndPoint->ipv4_settings.ulIPAddress : 0U ) ) ); } #endif /* ( ipconfigHAS_DEBUG_PRINTF != 0 ) */ From d70a21ce03569118e030b348844477b92f5fd227 Mon Sep 17 00:00:00 2001 From: Monika Singh Date: Mon, 4 Dec 2023 11:00:20 +0530 Subject: [PATCH 3/8] Fix UT coverage to 100% (#1053) * Update to 100% coverage * Fix UT coverage --- .github/workflows/ci.yml | 2 ++ .../FreeRTOS_Sockets_TCP_API_utest.c | 4 +++ .../FreeRTOS_Sockets_privates_utest.c | 26 ++++++++++++++++++- 3 files changed, 31 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c21195c62..9d21a66b1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -71,6 +71,8 @@ jobs: uses: FreeRTOS/CI-CD-Github-Actions/coverage-cop@main with: coverage-file: ./test/unit-test/build/coverage.info + branch-coverage-min: 100 + line-coverage-min: 100 spell-check: runs-on: ubuntu-latest diff --git a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_TCP_API_utest.c b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_TCP_API_utest.c index f242720d8..8a562c408 100644 --- a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_TCP_API_utest.c +++ b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_TCP_API_utest.c @@ -1863,6 +1863,10 @@ void test_FreeRTOS_get_tx_base_InvalidParams( void ) xSocket.ucProtocol = FREERTOS_IPPROTO_TCP; pucReturn = FreeRTOS_get_tx_base( &xSocket ); TEST_ASSERT_EQUAL( NULL, pucReturn ); + + xSocket.u.xTCP.bits.bMallocError == pdTRUE_UNSIGNED; + pucReturn = FreeRTOS_get_tx_base( &xSocket ); + TEST_ASSERT_EQUAL( NULL, pucReturn ); } /** diff --git a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_privates_utest.c b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_privates_utest.c index 53ef4625a..8c7304893 100644 --- a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_privates_utest.c +++ b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_privates_utest.c @@ -591,7 +591,7 @@ void test_vSocketBind_TCP( void ) /** * @brief Address passed is NULL. */ -void test_vSocketBind_TCPNULLAddress( void ) +void test_vSocketBind_TCPNULLAddress_v4( void ) { BaseType_t xReturn; FreeRTOS_Socket_t xSocket; @@ -603,6 +603,30 @@ void test_vSocketBind_TCPNULLAddress( void ) memset( &xSocket, 0, sizeof( xSocket ) ); xSocket.ucProtocol = ( uint8_t ) FREERTOS_IPPROTO_TCP; + xSocket.bits.bIsIPv6 = 0; + + xApplicationGetRandomNumber_ExpectAnyArgsAndReturn( pdFALSE ); + xReturn = vSocketBind( &xSocket, NULL, uxAddressLength, xInternal ); + + TEST_ASSERT_EQUAL( -pdFREERTOS_ERRNO_EADDRNOTAVAIL, xReturn ); +} + +/** + * @brief Address passed is NULL. + */ +void test_vSocketBind_TCPNULLAddress_v6( void ) +{ + BaseType_t xReturn; + FreeRTOS_Socket_t xSocket; + struct freertos_sockaddr xBindAddress; + size_t uxAddressLength; + BaseType_t xInternal = pdFALSE; + + memset( &xBindAddress, 0xFC, sizeof( xBindAddress ) ); + memset( &xSocket, 0, sizeof( xSocket ) ); + + xSocket.ucProtocol = ( uint8_t ) FREERTOS_IPPROTO_TCP; + xSocket.bits.bIsIPv6 = 1; xApplicationGetRandomNumber_ExpectAnyArgsAndReturn( pdFALSE ); xReturn = vSocketBind( &xSocket, NULL, uxAddressLength, xInternal ); From c8d98d443b26937cab629d878c43b4da5d6202ae Mon Sep 17 00:00:00 2001 From: Monika Singh Date: Fri, 8 Dec 2023 10:37:49 +0530 Subject: [PATCH 4/8] Fix MISRA issue (#1049) Fix following MISRA issues : MISRA Rule 8_5 : Symbol "FreeRTOS_inet_ntop6" is declared more than once. MISRA Rule 8_9 : Symbol "FreeRTOS_in6addr_loopback" should be defined at block scope. MISRA Rule 8_8 : missing static storage modifier for "prvCloseDHCPSocket" which has internal linkage. MISRA Rule 9_1 : Using uninitialized value "xRemoteIP.xIs_IPv6" when calling "pxTCPSocketLookup". MISRA Rule 9_1 : Using uninitialized value "pxAddress->sin_family" when calling "prvSocketBindAdd". MISRA Rule 11_3 : A cast shall not be performed between two pointer of different object type. MISRA Rule 12_1 : Missing parentheses on sub-expression of the operator. MISRA Rule 14.4 : The condition expression 0 does not have an essentially boolean type MISRA Rule 15_6 : The body of the "then" branch of the "if" statement is not a compound statement. MISRA Rule 17_7 : The return value of a non-void function "memset" is unused. MISRA Rule 20_5 : Using "#undef". MISRA Rule 20_10 : Use of "#" or "##" preprocessor operator. MISRA Rule 21_1 : Defining or undefining a reserved name "_static", which is an identifier or macro name beginning with an underscore. MISRA Rule 21_15 : Calling function "memcmp" with incompatible types "void " and "uint8_t const ()[6]". --- source/FreeRTOS_ARP.c | 10 +++++----- source/FreeRTOS_DHCP.c | 4 ++-- source/FreeRTOS_DNS.c | 4 +--- source/FreeRTOS_IPv6.c | 3 +++ source/FreeRTOS_RA.c | 4 ++++ source/FreeRTOS_Sockets.c | 13 ++++++++++-- source/FreeRTOS_TCP_IP_IPv6.c | 1 + source/include/FreeRTOSIPConfigDefaults.h | 20 ++++++++++++++----- source/include/FreeRTOS_IPv6_Private.h | 2 +- source/include/FreeRTOS_IPv6_Sockets.h | 7 ------- .../BufferManagement/BufferAllocation_2.c | 8 ++++---- test/cbmc/patches/FreeRTOSIPConfig.h | 7 +------ 12 files changed, 48 insertions(+), 35 deletions(-) diff --git a/source/FreeRTOS_ARP.c b/source/FreeRTOS_ARP.c index 5a84cd60b..aab9b6707 100644 --- a/source/FreeRTOS_ARP.c +++ b/source/FreeRTOS_ARP.c @@ -294,8 +294,8 @@ static TickType_t xLastGratuitousARPTime = 0U; if( ulTargetProtocolAddress == pxTargetEndPoint->ipv4_settings.ulIPAddress ) { - if( memcmp( ( void * ) pxTargetEndPoint->xMACAddress.ucBytes, - ( pxARPHeader->xSenderHardwareAddress.ucBytes ), + if( memcmp( pxTargetEndPoint->xMACAddress.ucBytes, + pxARPHeader->xSenderHardwareAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) != 0 ) { vARPProcessPacketRequest( pxARPFrame, pxTargetEndPoint, ulSenderProtocolAddress ); @@ -310,9 +310,9 @@ static TickType_t xLastGratuitousARPTime = 0U; /* Make sure target MAC address is either ff:ff:ff:ff:ff:ff or 00:00:00:00:00:00 and senders MAC * address is not matching with the endpoint MAC address. */ - if( ( ( memcmp( ( const void * ) pxARPHeader->xTargetHardwareAddress.ucBytes, xBroadcastMACAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) || - ( ( memcmp( ( const void * ) pxARPHeader->xTargetHardwareAddress.ucBytes, xGARPTargetAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) ) ) && - ( memcmp( ( void * ) pxTargetEndPoint->xMACAddress.ucBytes, ( pxARPHeader->xSenderHardwareAddress.ucBytes ), ipMAC_ADDRESS_LENGTH_BYTES ) != 0 ) ) + if( ( ( memcmp( pxARPHeader->xTargetHardwareAddress.ucBytes, xBroadcastMACAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) || + ( ( memcmp( pxARPHeader->xTargetHardwareAddress.ucBytes, xGARPTargetAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) == 0 ) ) ) && + ( memcmp( pxTargetEndPoint->xMACAddress.ucBytes, pxARPHeader->xSenderHardwareAddress.ucBytes, ipMAC_ADDRESS_LENGTH_BYTES ) != 0 ) ) { MACAddress_t xHardwareAddress; NetworkEndPoint_t * pxCachedEndPoint; diff --git a/source/FreeRTOS_DHCP.c b/source/FreeRTOS_DHCP.c index 19a50bafd..1effc8f2a 100644 --- a/source/FreeRTOS_DHCP.c +++ b/source/FreeRTOS_DHCP.c @@ -843,7 +843,7 @@ * using it. * @param[in] pxEndPoint The end-point that stops using the socket. */ - void prvCloseDHCPSocket( NetworkEndPoint_t * pxEndPoint ) + static void prvCloseDHCPSocket( NetworkEndPoint_t * pxEndPoint ) { if( ( EP_DHCPData.xDHCPSocket == NULL ) || ( EP_DHCPData.xDHCPSocket != xDHCPv4Socket ) ) { @@ -905,7 +905,7 @@ ( void ) FreeRTOS_setsockopt( xDHCPv4Socket, 0, FREERTOS_SO_RCVTIMEO, &( xTimeoutTime ), sizeof( TickType_t ) ); ( void ) FreeRTOS_setsockopt( xDHCPv4Socket, 0, FREERTOS_SO_SNDTIMEO, &( xTimeoutTime ), sizeof( TickType_t ) ); - memset( &xAddress, 0, sizeof( xAddress ) ); + ( void ) memset( &xAddress, 0, sizeof( xAddress ) ); xAddress.sin_family = FREERTOS_AF_INET4; xAddress.sin_len = ( uint8_t ) sizeof( xAddress ); /* Bind to the standard DHCP client port. */ diff --git a/source/FreeRTOS_DNS.c b/source/FreeRTOS_DNS.c index 899e47978..9dc3832b1 100644 --- a/source/FreeRTOS_DNS.c +++ b/source/FreeRTOS_DNS.c @@ -1082,9 +1082,7 @@ /* MISRA Ref 11.3.1 [Misaligned access] */ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */ /* coverity[misra_c_2012_rule_11_3_violation] */ - const DNSMessage_t * pxDNSMessageHeader = - ( ( const DNSMessage_t * ) - pxReceiveBuffer->pucPayloadBuffer ); + const DNSMessage_t * pxDNSMessageHeader = ( const DNSMessage_t * ) pxReceiveBuffer->pucPayloadBuffer; #if ( ipconfigUSE_MDNS == 1 ) /* _HT_ changed 'pxReceiveBuffer->sin_port' to 'usPort' */ diff --git a/source/FreeRTOS_IPv6.c b/source/FreeRTOS_IPv6.c index b021f3ef2..0e8f85ea1 100644 --- a/source/FreeRTOS_IPv6.c +++ b/source/FreeRTOS_IPv6.c @@ -62,6 +62,9 @@ const struct xIPv6_Address FreeRTOS_in6addr_any = { 0 }; /** * This variable is initialized by the system to contain the loopback IPv6 address. */ +/* MISRA Ref 8.9.1 [File scoped variables] */ +/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-89 */ +/* coverity[misra_c_2012_rule_8_9_violation] */ const struct xIPv6_Address FreeRTOS_in6addr_loopback = { { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 1U } }; #if ( ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM == 1 ) diff --git a/source/FreeRTOS_RA.c b/source/FreeRTOS_RA.c index 0a5c10ee4..9f9ef8fc2 100644 --- a/source/FreeRTOS_RA.c +++ b/source/FreeRTOS_RA.c @@ -168,6 +168,10 @@ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */ /* coverity[misra_c_2012_rule_11_3_violation] */ pxICMPPacket = ( ( ICMPPacket_IPv6_t * ) pxDescriptor->pucEthernetBuffer ); + + /* MISRA Ref 11.3.1 [Misaligned access] */ + /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-113 */ + /* coverity[misra_c_2012_rule_11_3_violation] */ xRASolicitationRequest = ( ( ICMPRouterSolicitation_IPv6_t * ) &( pxICMPPacket->xICMPHeaderIPv6 ) ); pxDescriptor->xDataLength = uxNeededSize; diff --git a/source/FreeRTOS_Sockets.c b/source/FreeRTOS_Sockets.c index 894a90146..ef07f4335 100644 --- a/source/FreeRTOS_Sockets.c +++ b/source/FreeRTOS_Sockets.c @@ -1926,8 +1926,17 @@ BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, if( pxAddress == NULL ) { pxAddress = &xAddress; - /* Put the port to zero to be assigned later. */ - pxAddress->sin_port = 0U; + /* Clear the address: */ + ( void ) memset( pxAddress, 0, sizeof( struct freertos_sockaddr ) ); + + if( pxSocket->bits.bIsIPv6 != pdFALSE_UNSIGNED ) + { + pxAddress->sin_family = FREERTOS_AF_INET6; + } + else + { + pxAddress->sin_family = FREERTOS_AF_INET; + } } } #endif /* ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND == 1 */ diff --git a/source/FreeRTOS_TCP_IP_IPv6.c b/source/FreeRTOS_TCP_IP_IPv6.c index ce1ac1304..d5a537d41 100644 --- a/source/FreeRTOS_TCP_IP_IPv6.c +++ b/source/FreeRTOS_TCP_IP_IPv6.c @@ -134,6 +134,7 @@ BaseType_t xProcessReceivedTCPPacket_IPV6( NetworkBufferDescriptor_t * pxDescrip /* coverity[misra_c_2012_rule_11_3_violation] */ const IPHeader_IPv6_t * pxIPHeader_IPv6 = ( ( IPHeader_IPv6_t * ) &( pxNetworkBuffer->pucEthernetBuffer[ ipSIZE_OF_ETH_HEADER ] ) ); ( void ) memcpy( xRemoteIP.xIPAddress.xIP_IPv6.ucBytes, pxIPHeader_IPv6->xSourceAddress.ucBytes, sizeof( IPv6_Address_t ) ); + xRemoteIP.xIs_IPv6 = pdTRUE; /* Find the destination socket, and if not found: return a socket listing to * the destination PORT. */ diff --git a/source/include/FreeRTOSIPConfigDefaults.h b/source/include/FreeRTOSIPConfigDefaults.h index 97a0b0868..70406fa22 100644 --- a/source/include/FreeRTOSIPConfigDefaults.h +++ b/source/include/FreeRTOSIPConfigDefaults.h @@ -67,6 +67,9 @@ */ #ifndef _static + /* suppressing the use of _static as it is used for other tools like cbmc */ + /* coverity[misra_c_2012_rule_21_1_violation] */ + /* coverity[misra_c_2012_rule_21_2_violation] */ #define _static static #endif @@ -3063,8 +3066,8 @@ #endif #ifndef FreeRTOS_debug_printf - #ifdef configPRINTF - #define FreeRTOS_debug_printf( MSG ) if( ipconfigHAS_DEBUG_PRINTF ) configPRINTF( MSG ) + #if ( ( ipconfigHAS_DEBUG_PRINTF == 1 ) && defined( configPRINTF ) ) + #define FreeRTOS_debug_printf( MSG ) do { configPRINTF( MSG ); } while( ipFALSE_BOOL ) #else #define FreeRTOS_debug_printf( MSG ) do {} while( ipFALSE_BOOL ) #endif @@ -3099,8 +3102,8 @@ #endif #ifndef FreeRTOS_printf - #ifdef configPRINTF - #define FreeRTOS_printf( MSG ) if( ipconfigHAS_PRINTF ) configPRINTF( MSG ) + #if ( ( ipconfigHAS_PRINTF == 1 ) && defined( configPRINTF ) ) + #define FreeRTOS_printf( MSG ) do { configPRINTF( MSG ); } while( ipFALSE_BOOL ) #else #define FreeRTOS_printf( MSG ) do {} while( ipFALSE_BOOL ) #endif @@ -3119,7 +3122,14 @@ */ #ifndef FreeRTOS_flush_logging - #define FreeRTOS_flush_logging() if( ipconfigHAS_PRINTF || ipconfigHAS_DEBUG_PRINTF ) do {} while( ipFALSE_BOOL ) + #define FreeRTOS_flush_logging() \ + if( ipconfigHAS_PRINTF || ipconfigHAS_DEBUG_PRINTF ) \ + { \ + do {} while( ipFALSE_BOOL ); \ + } \ + else \ + { \ + } #endif /*---------------------------------------------------------------------------*/ diff --git a/source/include/FreeRTOS_IPv6_Private.h b/source/include/FreeRTOS_IPv6_Private.h index 1e5ad5d07..e00ab1956 100644 --- a/source/include/FreeRTOS_IPv6_Private.h +++ b/source/include/FreeRTOS_IPv6_Private.h @@ -57,10 +57,10 @@ /* The offset into an IP packet into which the IP data (payload) starts. */ #define ipIPv6_PAYLOAD_OFFSET ( sizeof( IPPacket_IPv6_t ) ) +/* The maximum UDP payload length. */ /* MISRA Ref 20.5.1 [Use of undef] */ /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-2051 */ /* coverity[misra_c_2012_rule_20_5_violation] */ -/* The maximum UDP payload length. */ #undef ipMAX_UDP_PAYLOAD_LENGTH #define ipMAX_UDP_PAYLOAD_LENGTH ( ( ipconfigNETWORK_MTU - ipSIZE_OF_IPv6_HEADER ) - ipSIZE_OF_UDP_HEADER ) /* The offset into a UDP packet at which the UDP data (payload) starts. */ diff --git a/source/include/FreeRTOS_IPv6_Sockets.h b/source/include/FreeRTOS_IPv6_Sockets.h index e435affc6..c9a931e67 100644 --- a/source/include/FreeRTOS_IPv6_Sockets.h +++ b/source/include/FreeRTOS_IPv6_Sockets.h @@ -90,13 +90,6 @@ */ void prv_ntop6_search_zeros( struct sNTOP6_Set * pxSet ); -/* - * Convert a string like 'fe80::8d11:cd9b:8b66:4a80' - * to a 16-byte IPv6 address - */ - const char * FreeRTOS_inet_ntop6( const void * pvSource, - char * pcDestination, - socklen_t uxSize ); /** @brief Called by pxTCPSocketLookup(), this function will check if a socket * is connected to a remote IP-address. It will be called from a loop diff --git a/source/portable/BufferManagement/BufferAllocation_2.c b/source/portable/BufferManagement/BufferAllocation_2.c index 95ae9fb69..02904bf15 100644 --- a/source/portable/BufferManagement/BufferAllocation_2.c +++ b/source/portable/BufferManagement/BufferAllocation_2.c @@ -70,14 +70,14 @@ /* Compile time assertion with zero runtime effects * it will assert on 'e' not being zero, as it tries to divide by it, * will also print the line where the error occurred in case of failure */ -/* MISRA Ref 20.10.1 [Lack of sizeof operator and compile time error checking] */ -/* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-2010 */ -/* coverity[misra_c_2012_rule_20_10_violation] */ #if defined( ipconfigETHERNET_MINIMUM_PACKET_BYTES ) + /* MISRA Ref 20.10.1 [Lack of sizeof operator and compile time error checking] */ + /* More details at: https://github.com/FreeRTOS/FreeRTOS-Plus-TCP/blob/main/MISRA.md#rule-2010 */ + /* coverity[misra_c_2012_rule_20_10_violation] */ #define ASSERT_CONCAT_( a, b ) a ## b #define ASSERT_CONCAT( a, b ) ASSERT_CONCAT_( a, b ) #define STATIC_ASSERT( e ) \ - enum { ASSERT_CONCAT( assert_line_, __LINE__ ) = 1 / ( !!( e ) ) } + enum { ASSERT_CONCAT( assert_line_, __LINE__ ) = ( 1 / ( !!( e ) ) ) } STATIC_ASSERT( ipconfigETHERNET_MINIMUM_PACKET_BYTES <= baMINIMAL_BUFFER_SIZE ); #endif diff --git a/test/cbmc/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h index 03d9164d6..f94bfb655 100644 --- a/test/cbmc/patches/FreeRTOSIPConfig.h +++ b/test/cbmc/patches/FreeRTOSIPConfig.h @@ -37,12 +37,7 @@ /* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to * 1 then FreeRTOS_debug_printf should be defined to the function used to print * out the debugging messages. */ -#ifndef ipconfigHAS_DEBUG_PRINTF - #define ipconfigHAS_DEBUG_PRINTF 0 -#endif -#if ( ipconfigHAS_DEBUG_PRINTF == 1 ) - #define FreeRTOS_debug_printf( X ) configPRINTF( X ) -#endif +#define FreeRTOS_debug_printf( X ) /* Set to 1 to print out non debugging messages, for example the output of the * FreeRTOS_netstat() command, and ping replies. If ipconfigHAS_PRINTF is set to 1 From f42d53ad8bc37dcc95184a8321a023dc066a4d30 Mon Sep 17 00:00:00 2001 From: Mikhail Paulyshka Date: Tue, 12 Dec 2023 14:39:41 +0300 Subject: [PATCH 5/8] phyHandling: Fix compilation with Clang, fix incorrect log output (#1060) * phyHandling: fix write to uninitialized variable, fix broken logging * phyHandling: remove ulPHYLinkStatus variable --- source/portable/NetworkInterface/Common/phyHandling.c | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/source/portable/NetworkInterface/Common/phyHandling.c b/source/portable/NetworkInterface/Common/phyHandling.c index 470256d6d..0c47b5de4 100644 --- a/source/portable/NetworkInterface/Common/phyHandling.c +++ b/source/portable/NetworkInterface/Common/phyHandling.c @@ -542,7 +542,7 @@ BaseType_t xPhyStartAutoNegotiation( EthernetPhy_t * pxPhyObject, uint32_t ulPhyMask ) { uint32_t xPhyIndex, ulDoneMask, ulBitMask; - uint32_t ulPHYLinkStatus, ulRegValue; + uint32_t ulRegValue; TickType_t xRemainingTime; TimeOut_t xTimer; @@ -624,15 +624,10 @@ BaseType_t xPhyStartAutoNegotiation( EthernetPhy_t * pxPhyObject, pxPhyObject->fnPhyRead( xPhyAddress, phyREG_01_BMSR, &ulRegValue ); - if( ( ulRegValue & phyBMSR_LINK_STATUS ) != 0 ) + if( ( ulRegValue & phyBMSR_LINK_STATUS ) != 0U ) { - ulPHYLinkStatus |= phyBMSR_LINK_STATUS; pxPhyObject->ulLinkStatusMask |= ulBitMask; } - else - { - ulPHYLinkStatus &= ~( phyBMSR_LINK_STATUS ); - } if( ulPhyID == PHY_ID_KSZ8081MNXIA ) { @@ -730,7 +725,7 @@ BaseType_t xPhyStartAutoNegotiation( EthernetPhy_t * pxPhyObject, ( unsigned int ) ulRegValue, ( ulRegValue & phyPHYSTS_DUPLEX_STATUS ) ? "full" : "half", ( ulRegValue & phyPHYSTS_SPEED_STATUS ) ? 10 : 100, - ( ( ulPHYLinkStatus |= phyBMSR_LINK_STATUS ) != 0 ) ? "high" : "low" ) ); + ( ( pxPhyObject->ulLinkStatusMask & ulBitMask ) != 0U ) ? "high" : "low" ) ); if( ( ulRegValue & phyPHYSTS_DUPLEX_STATUS ) != ( uint32_t ) 0U ) { From 10b5171dbd33b13a982110a44b349a84c48e90bf Mon Sep 17 00:00:00 2001 From: Hein Tibosch Date: Tue, 26 Dec 2023 19:48:13 +0800 Subject: [PATCH 6/8] Set ipBUFFER_PADDING to 14 bytes by default on 64 bit targets v2 (#1061) * Set ipBUFFER_PADDING to 14 bytes by default on 64 bit targets v2 * Added U suffix to some literal values like 0xFFFFFFFFU * Corrected the offset/size table in the comments * Changes ipBUFFER_PADDING checks after review Monika and Tony --------- Co-authored-by: Tony Josi --- source/FreeRTOS_IP_Utils.c | 34 ++++++++++++++++++++++------------ source/include/FreeRTOS_IP.h | 28 ++++++++++++++++++---------- 2 files changed, 40 insertions(+), 22 deletions(-) diff --git a/source/FreeRTOS_IP_Utils.c b/source/FreeRTOS_IP_Utils.c index 73ad81c10..906c2b6ba 100644 --- a/source/FreeRTOS_IP_Utils.c +++ b/source/FreeRTOS_IP_Utils.c @@ -983,18 +983,28 @@ void vPreCheckConfigs( void ) #if ( configASSERT_DEFINED == 1 ) { - volatile size_t uxSize = sizeof( uintptr_t ); - - if( uxSize == 8U ) - { - /* This is a 64-bit platform, make sure there is enough space in - * pucEthernetBuffer to store a pointer and also make sure that the value of - * ipconfigBUFFER_PADDING is such that (ipconfigBUFFER_PADDING + ipSIZE_OF_ETH_HEADER) is a - * 32 bit (4 byte) aligned value, so that when incrementing the ethernet buffer with - * (ipconfigBUFFER_PADDING + ipSIZE_OF_ETH_HEADER) bytes it lands in a 32 bit aligned address - * which lets us efficiently access 32 bit values later in the packet. */ - configASSERT( ( ipconfigBUFFER_PADDING >= 14 ) && ( ( ( ( ipconfigBUFFER_PADDING ) + ( ipSIZE_OF_ETH_HEADER ) ) % 4 ) == 0 ) ); - } + size_t uxSize; + + /* Check if ipBUFFER_PADDING has a minimum size, depending on the platform. + * See FreeRTOS_IP.h for more details. */ + #if ( UINTPTR_MAX > 0xFFFFFFFFU ) + + /* + * This is a 64-bit platform, make sure there is enough space in + * pucEthernetBuffer to store a pointer. + */ + configASSERT( ipBUFFER_PADDING >= 14U ); + #else + /* This is a 32-bit platform. */ + configASSERT( ipBUFFER_PADDING >= 10U ); + #endif /* UINTPTR_MAX > 0xFFFFFFFFU */ + + /* + * The size of the Ethernet header (14) plus ipBUFFER_PADDING should be a + * multiple of 32 bits, in order to get aligned access to all uint32_t + * fields in the protocol headers. + */ + configASSERT( ( ( ( ipSIZE_OF_ETH_HEADER ) + ( ipBUFFER_PADDING ) ) % 4U ) == 0U ); /* LCOV_EXCL_BR_START */ uxSize = ipconfigNETWORK_MTU; diff --git a/source/include/FreeRTOS_IP.h b/source/include/FreeRTOS_IP.h index 1995b9ffe..85af11a7e 100644 --- a/source/include/FreeRTOS_IP.h +++ b/source/include/FreeRTOS_IP.h @@ -97,22 +97,30 @@ extern uint32_t ulApplicationGetNextSequenceNumber( uint32_t ulSourceAddress, * pointer back to the network buffer. Should be a multiple of 8 to ensure 8 byte * alignment is maintained on architectures that require it. * - * In order to get a 32-bit alignment of network packets, an offset of 2 bytes - * would be desirable, as defined by ipconfigPACKET_FILLER_SIZE. So the malloc'd + * In order to get a 32-bit or 64-bit alignment of network packets, an offset of 2 bytes + * is ideal as defined by ipconfigPACKET_FILLER_SIZE. So the malloc'd * buffer will have the following contents: - * uint32_t pointer; // word-aligned - * uchar_8 filler[6]; - * << ETH-header >> // half-word-aligned - * uchar_8 dest[6]; // start of pucEthernetBuffer - * uchar_8 dest[6]; - * uchar16_t type; - * << IP-header >> // word-aligned + * + * +---------+-----------+---------+ + * | Offset | Alignment | Length | + * | 32 | 64 | 32 | 64 | 32 | 64 | + * |----|----|-----|-----|----|----| + * | 0 | 0 | 4 | 8 | 4 | 8 | uchar_8 * pointer; // Points to the 'NetworkBufferDescriptor_t'. + * | 4 | 8 | 4 | 8 | 6 | 6 | uchar_8 filler[6]; // To give the +2 byte offset. + * |-------------------------------| + * | 10 | 14 | 4+2 | 8+2 | 6 | 6 | uchar_8 dest_mac[6]; // Destination address. + * | 16 | 20 | 4 | 8 | 6 | 6 | uchar_8 src_mac[6]; // Source address. + * | 22 | 26 | 4+2 | 4+2 | 2 | 2 | uchar16_t ethertype; + * | 24 | 28 | 4 | 4 | ~ | ~ | << IP-header >> // word-aligned, either 4 or 8 bytes. * uint8_t ucVersionHeaderLength; * etc */ -#if ( ipconfigBUFFER_PADDING != 0 ) +/* Use setting from FreeRTOS if defined and non-zero */ +#if defined( ipconfigBUFFER_PADDING ) && ( ipconfigBUFFER_PADDING != 0 ) #define ipBUFFER_PADDING ipconfigBUFFER_PADDING +#elif ( UINTPTR_MAX > 0xFFFFFFFF ) + #define ipBUFFER_PADDING ( 12U + ipconfigPACKET_FILLER_SIZE ) #else #define ipBUFFER_PADDING ( 8U + ipconfigPACKET_FILLER_SIZE ) #endif From af07ccf4c4ed038409910892c400b3e04b40c183 Mon Sep 17 00:00:00 2001 From: Hein Tibosch Date: Tue, 2 Jan 2024 14:37:53 +0800 Subject: [PATCH 7/8] Avoid critical sections where possible (#1063) * Avoid critical sections where possible * Repair unit test FreeRTOS_Sockets --------- Co-authored-by: Tony Josi --- source/FreeRTOS_Sockets.c | 4 +- source/FreeRTOS_UDP_IPv4.c | 10 +-- source/FreeRTOS_UDP_IPv6.c | 10 +-- .../FreeRTOS_Sockets_UDP_API_utest.c | 72 +++++++++++++++---- 4 files changed, 65 insertions(+), 31 deletions(-) diff --git a/source/FreeRTOS_Sockets.c b/source/FreeRTOS_Sockets.c index ef07f4335..ca170e050 100644 --- a/source/FreeRTOS_Sockets.c +++ b/source/FreeRTOS_Sockets.c @@ -1171,7 +1171,7 @@ static NetworkBufferDescriptor_t * prvRecvFromWaitForPacket( FreeRTOS_Socket_t c if( lPacketCount > 0 ) { - taskENTER_CRITICAL(); + vTaskSuspendAll(); { /* The owner of the list item is the network buffer. */ pxNetworkBuffer = ( ( NetworkBufferDescriptor_t * ) listGET_OWNER_OF_HEAD_ENTRY( &( pxSocket->u.xUDP.xWaitingPacketsList ) ) ); @@ -1183,7 +1183,7 @@ static NetworkBufferDescriptor_t * prvRecvFromWaitForPacket( FreeRTOS_Socket_t c ( void ) uxListRemove( &( pxNetworkBuffer->xBufferListItem ) ); } } - taskEXIT_CRITICAL(); + ( void ) xTaskResumeAll(); } *pxEventBits = xEventBits; diff --git a/source/FreeRTOS_UDP_IPv4.c b/source/FreeRTOS_UDP_IPv4.c index 9562ea90d..0cea8ae5b 100644 --- a/source/FreeRTOS_UDP_IPv4.c +++ b/source/FreeRTOS_UDP_IPv4.c @@ -445,13 +445,9 @@ BaseType_t xProcessReceivedUDPPacket_IPv4( NetworkBufferDescriptor_t * pxNetwork { vTaskSuspendAll(); { - taskENTER_CRITICAL(); - { - /* Add the network packet to the list of packets to be - * processed by the socket. */ - vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) ); - } - taskEXIT_CRITICAL(); + /* Add the network packet to the list of packets to be + * processed by the socket. */ + vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) ); } ( void ) xTaskResumeAll(); diff --git a/source/FreeRTOS_UDP_IPv6.c b/source/FreeRTOS_UDP_IPv6.c index 7644780da..894f863f3 100644 --- a/source/FreeRTOS_UDP_IPv6.c +++ b/source/FreeRTOS_UDP_IPv6.c @@ -536,13 +536,9 @@ BaseType_t xProcessReceivedUDPPacket_IPv6( NetworkBufferDescriptor_t * pxNetwork { vTaskSuspendAll(); { - taskENTER_CRITICAL(); - { - /* Add the network packet to the list of packets to be - * processed by the socket. */ - vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) ); - } - taskEXIT_CRITICAL(); + /* Add the network packet to the list of packets to be + * processed by the socket. */ + vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( pxNetworkBuffer->xBufferListItem ) ); } ( void ) xTaskResumeAll(); diff --git a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_UDP_API_utest.c b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_UDP_API_utest.c index 6f6ac2779..d321d4999 100644 --- a/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_UDP_API_utest.c +++ b/test/unit-test/FreeRTOS_Sockets/FreeRTOS_Sockets_UDP_API_utest.c @@ -380,9 +380,14 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_JustUDPHeader( void ) listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); - uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + + uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -441,9 +446,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100( void ) listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); - uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -503,9 +512,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall( void listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); - uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -566,7 +579,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_Peek( listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + } + + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -624,7 +643,12 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_Peek_ listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -681,9 +705,15 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_Packet100SizeSmall_ZeroC listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + + uxListRemove_ExpectAndReturn( &xNetworkBuffer.xBufferListItem, 0U ); + } - uxListRemove_ExpectAndReturn( &xNetworkBuffer.xBufferListItem, 0U ); + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -733,7 +763,11 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBegining_Packet100SizeSmall_Zero xListItem.pvOwner = &xNetworkBuffer; xSocket->u.xUDP.xWaitingPacketsList.xListEnd.pxNext = &xListItem; - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv4_HEADER ); @@ -789,9 +823,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_IPv6Packet100( void ) listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); - uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( ipSIZE_OF_IPv6_HEADER ); @@ -850,9 +888,13 @@ void test_FreeRTOS_recvfrom_BlockingGetsPacketInBetween_UnknownIPHeaderSize( voi listCURRENT_LIST_LENGTH_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), 0x12 ); - listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); + vTaskSuspendAll_Expect(); + { + listGET_OWNER_OF_HEAD_ENTRY_ExpectAndReturn( &( xSocket->u.xUDP.xWaitingPacketsList ), &xNetworkBuffer ); - uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + uxListRemove_ExpectAndReturn( &( xNetworkBuffer.xBufferListItem ), 0 ); + } + xTaskResumeAll_ExpectAndReturn( pdFALSE ); uxIPHeaderSizePacket_IgnoreAndReturn( 0xFF ); From fcd2de003931c317123cbe0c73ec3b6d7cc68372 Mon Sep 17 00:00:00 2001 From: Monika Singh Date: Tue, 2 Jan 2024 12:29:15 +0530 Subject: [PATCH 8/8] Remove unused FreeRTOS_flush_logging (#1066) * Remove unused FreeRTOS_flush_logging * Fix CBMC failures --------- Co-authored-by: tony-josi-aws --- source/FreeRTOS_TCP_WIN.c | 7 ------ source/include/FreeRTOSIPConfigDefaults.h | 23 ------------------- .../proofs/CheckOptionsInner/Makefile.json | 2 +- 3 files changed, 1 insertion(+), 31 deletions(-) diff --git a/source/FreeRTOS_TCP_WIN.c b/source/FreeRTOS_TCP_WIN.c index c570fe611..a00e67b11 100644 --- a/source/FreeRTOS_TCP_WIN.c +++ b/source/FreeRTOS_TCP_WIN.c @@ -1158,7 +1158,6 @@ pxWindow->usOurPortNumber, ( unsigned ) ( ulSequenceNumber - pxWindow->rx.ulFirstSequenceNumber ), ( unsigned ) listCURRENT_LIST_LENGTH( &pxWindow->xRxSegments ) ) ); - FreeRTOS_flush_logging(); } /* Return a positive value. The packet may be accepted @@ -1391,7 +1390,6 @@ ( int ) pxSegment->lDataLength, ( unsigned ) ( pxWindow->ulNextTxSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ), ( int ) pxSegment->lStreamPos ) ); - FreeRTOS_flush_logging(); } return lToWrite; @@ -1703,7 +1701,6 @@ ( int ) pxSegment->lDataLength, ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) pxSegment->ulSequenceNumber ) ); - FreeRTOS_flush_logging(); } } else @@ -1776,7 +1773,6 @@ ( int ) pxSegment->lDataLength, ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) ulWindowSize ) ); - FreeRTOS_flush_logging(); } } @@ -1823,7 +1819,6 @@ ( int ) pxSegment->lDataLength, ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) ulWindowSize ) ); - FreeRTOS_flush_logging(); } } else @@ -2137,7 +2132,6 @@ FreeRTOS_debug_printf( ( "prvTCPWindowFastRetransmit: Requeue sequence number %u < %u\n", ( unsigned ) ( pxSegment->ulSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) ( ulFirst - pxWindow->tx.ulFirstSequenceNumber ) ) ); - FreeRTOS_flush_logging(); } /* Remove it from xWaitQueue. */ @@ -2222,7 +2216,6 @@ ( unsigned ) ( ulFirst - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) ( ulLast - pxWindow->tx.ulFirstSequenceNumber ), ( unsigned ) ( pxWindow->tx.ulCurrentSequenceNumber - pxWindow->tx.ulFirstSequenceNumber ) ) ); - FreeRTOS_flush_logging(); } return ulAckCount; diff --git a/source/include/FreeRTOSIPConfigDefaults.h b/source/include/FreeRTOSIPConfigDefaults.h index 70406fa22..33db82fc4 100644 --- a/source/include/FreeRTOSIPConfigDefaults.h +++ b/source/include/FreeRTOSIPConfigDefaults.h @@ -3111,29 +3111,6 @@ /*---------------------------------------------------------------------------*/ -/* - * FreeRTOS_flush_logging - * - * Type: Macro Function - * - * Macro that is called in cases where a lot of logging is produced. - * - * This gives the logging module a chance to flush the data. - */ - -#ifndef FreeRTOS_flush_logging - #define FreeRTOS_flush_logging() \ - if( ipconfigHAS_PRINTF || ipconfigHAS_DEBUG_PRINTF ) \ - { \ - do {} while( ipFALSE_BOOL ); \ - } \ - else \ - { \ - } -#endif - -/*---------------------------------------------------------------------------*/ - /* * ipconfigTCP_IP_SANITY * diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json index f318ae1cd..a902bcc94 100644 --- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json +++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json @@ -3,7 +3,7 @@ "CBMCFLAGS": [ "--unwind 1", "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowTxCheckAck.0:2", - "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.1:2" + "--unwindset __CPROVER_file_local_FreeRTOS_TCP_WIN_c_prvTCPWindowFastRetransmit.0:2" ], "OPT": [