From 24929523455a30caedc5ffee2be02f2634e91e08 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 11:55:20 +0530 Subject: [PATCH 01/10] Rename DNS proof --- source/FreeRTOS_DNS_Parser.c | 2 +- .../proofs/{ParseDNSReply => DNS_ParseDNSReply}/Makefile.json | 0 .../ParseDNSReply_harness.c | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename test/cbmc/proofs/{ParseDNSReply => DNS_ParseDNSReply}/Makefile.json (100%) rename test/cbmc/proofs/{ParseDNSReply => DNS_ParseDNSReply}/ParseDNSReply_harness.c (100%) diff --git a/source/FreeRTOS_DNS_Parser.c b/source/FreeRTOS_DNS_Parser.c index 67fd2d4f6..877bcb61a 100644 --- a/source/FreeRTOS_DNS_Parser.c +++ b/source/FreeRTOS_DNS_Parser.c @@ -613,7 +613,7 @@ } uxResult = DNS_SkipNameField( pxSet->pucByte, - sizeof( pxSet->pcName ) ); + pxSet->uxSourceBytesRemaining ); /* Check for a malformed response. */ if( uxResult == 0U ) diff --git a/test/cbmc/proofs/ParseDNSReply/Makefile.json b/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json similarity index 100% rename from test/cbmc/proofs/ParseDNSReply/Makefile.json rename to test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json diff --git a/test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/ParseDNSReply_harness.c similarity index 100% rename from test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c rename to test/cbmc/proofs/DNS_ParseDNSReply/ParseDNSReply_harness.c From 7e1b9018934286fee18a119331a1e504414adefc Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 11:57:01 +0530 Subject: [PATCH 02/10] Rename DNS proof --- .../{ParseDNSReply_harness.c => DNS_ParseDNSReply_harness.c} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/cbmc/proofs/DNS_ParseDNSReply/{ParseDNSReply_harness.c => DNS_ParseDNSReply_harness.c} (100%) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c similarity index 100% rename from test/cbmc/proofs/DNS_ParseDNSReply/ParseDNSReply_harness.c rename to test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c From 63726ee2705b271e2d283d2c636ad6c696f77625 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 11:57:33 +0530 Subject: [PATCH 03/10] Fix DNS parse reply proof --- .../DNS_ParseDNSReply_harness.c | 224 ++++++++++++------ .../proofs/DNS_ParseDNSReply/Makefile.json | 94 +++----- 2 files changed, 190 insertions(+), 128 deletions(-) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c index 74e594fbd..9432b9277 100644 --- a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c +++ b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c @@ -10,9 +10,6 @@ /* FreeRTOS+TCP includes. */ #include "FreeRTOS_IP.h" -#include "FreeRTOS_Sockets.h" -#include "FreeRTOS_IP_Private.h" -#include "FreeRTOS_UDP_IP.h" #include "FreeRTOS_DNS.h" #include "FreeRTOS_DNS_Parser.h" #include "NetworkBufferManagement.h" @@ -20,91 +17,148 @@ #include "IPTraceMacroDefaults.h" #include "cbmc.h" +#include "../../../utility/memory_assignments.c" /**************************************************************** * Signature of function under test ****************************************************************/ -uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer, - size_t uxBufferLength, - BaseType_t xExpected ); +uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer, + size_t uxBufferLength, + struct freertos_addrinfo ** ppxAddressInfo, + BaseType_t xExpected, + uint16_t usPort ); -/**************************************************************** -* Abstraction of DNS_ReadNameField proved in ReadNameField -****************************************************************/ +NetworkBufferDescriptor_t xNetworkBuffer; +int lIsIPv6Packet; -size_t DNS_ReadNameField( const uint8_t * pucByte, - size_t uxRemainingBytes, - char * pcName, - size_t uxDestLen ) +size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer ) { - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); - __CPROVER_assert( NAME_SIZE < CBMC_MAX_OBJECT_SIZE, - "NAME_SIZE < CBMC_MAX_OBJECT_SIZE" ); - __CPROVER_assert( NAME_SIZE >= 4, - "NAME_SIZE >= 4 required for good coverage." ); + #if IS_TESTING_IPV6 + return ipSIZE_OF_IPv6_HEADER; + #else + return ipSIZE_OF_IPv4_HEADER; + #endif +} +NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pvBuffer ) +{ + __CPROVER_assert( pvBuffer != NULL, "Precondition: pvBuffer != NULL" ); + NetworkBufferDescriptor_t * pxRBuf; + + if( nondet_bool() ) + { + pxRBuf = NULL; + } + else + { + pxRBuf = &xNetworkBuffer; + } + + return pxRBuf; +} - /* Preconditions */ - __CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, - "ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)" ); - __CPROVER_assert( uxDestLen < CBMC_MAX_OBJECT_SIZE, - "ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)" ); +uint32_t ulChar2u32( const uint8_t * pucPtr ) +{ + __CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" ); +} - __CPROVER_assert( uxRemainingBytes <= NETWORK_BUFFER_SIZE, - "ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)" ); +uint16_t usChar2u16( const uint8_t * pucPtr ) +{ + __CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" ); +} - /* This precondition in the function contract for prvReadNameField - * fails because prvCheckOptions called prvReadNameField with the - * constant value 254. - * __CPROVER_assert(uxDestLen <= NAME_SIZE, - * "ReadNameField: uxDestLen <= NAME_SIZE)"); - */ +const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily, + const void * pvSource, + char * pcDestination, + socklen_t uxSize ) +{ + __CPROVER_assert( __CPROVER_r_ok( pcDestination, uxSize ), "input buffer must be available" ); - __CPROVER_assert( pucByte != NULL, - "ReadNameField: pucByte != NULL )" ); - __CPROVER_assert( pcName != NULL, - "ReadNameField: pcName != NULL )" ); + #if IS_TESTING_IPV6 + __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET6 && __CPROVER_r_ok( pvSource, 16 ) ), "input address must be available" ); + #else + __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET && __CPROVER_r_ok( pvSource, 4 ) ), "input address must be available" ); + #endif +} - __CPROVER_assert( uxDestLen > 0, - "ReadNameField: uxDestLen > 0)" ); +BaseType_t xApplicationDNSQueryHook_Multi( struct xNetworkEndPoint * pxEndPoint, + const char * pcName ) +{ + __CPROVER_assert( strlen( pcName ) < ipconfigDNS_CACHE_NAME_LENGTH, "The length of domain name must be less than cache size" ); +} - /* Return value */ - size_t index; +void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer ) +{ + __CPROVER_assert( pxNetworkBuffer, "network descriptor must be valid." ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer, "network buffer must be valid." ); - /* Postconditions */ - __CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes ); + free( pxNetworkBuffer->pucEthernetBuffer ); + free( pxNetworkBuffer ); +} - return index; +/* The checksum generation is stubbed out since the actual checksum + * does not matter. The stub will return an indeterminate value each time. */ +uint16_t usGenerateChecksum( uint16_t usSum, + const uint8_t * pucNextData, + size_t uxByteCount ) +{ + uint16_t usReturn; + + __CPROVER_assert( __CPROVER_r_ok( pucNextData, uxByteCount ), "Data must be valid" ); + + /* Return an indeterminate value. */ + return usReturn; } -/**************************************************************** -* Abstraction of DNS_SkipNameField proved in SkipNameField -****************************************************************/ +/* The checksum generation is stubbed out since the actual checksum + * does not matter. The stub will return an indeterminate value each time. */ +uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer, + size_t uxBufferLength, + BaseType_t xOutgoingPacket ) +{ + uint16_t usReturn; + + __CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "Data must be valid" ); + + /* Return an indeterminate value. */ + return usReturn; +} -size_t DNS_SkipNameField( const uint8_t * pucByte, - size_t uxLength ) +/* pxDuplicateNetworkBufferWithDescriptor() is proved separately */ +NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer, + size_t xNewLength ) { - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); + NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) ); + if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) + { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength ); + __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer ); + pxNetworkBuffer->xDataLength = xNewLength; + } - /* Preconditions */ - __CPROVER_assert( uxLength < CBMC_MAX_OBJECT_SIZE, - "SkipNameField: uxLength < CBMC_MAX_OBJECT_SIZE)" ); - __CPROVER_assert( uxLength <= NETWORK_BUFFER_SIZE, - "SkipNameField: uxLength <= NETWORK_BUFFER_SIZE)" ); - __CPROVER_assert( pucByte != NULL, - "SkipNameField: pucByte != NULL)" ); + return pxNetworkBuffer; +} - /* Return value */ - size_t index; +/* vReturnEthernetFrame() is proved separately */ +void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" ); +} - /* Postconditions */ - __CPROVER_assume( index <= uxLength ); +uint32_t parseDNSAnswer( ParseSet_t * pxSet, + struct freertos_addrinfo ** ppxAddressInfo, + size_t * uxBytesRead ) +{ + uint32_t result; - return index; + __CPROVER_assert( __CPROVER_r_ok( pxSet->pucByte, pxSet->uxSourceBytesRemaining ), "Data must be valid" ); + + return result; } /**************************************************************** @@ -114,17 +168,43 @@ size_t DNS_SkipNameField( const uint8_t * pucByte, void harness() { size_t uxBufferLength; + uint16_t usPort; + struct freertos_addrinfo *pxAddressInfo; BaseType_t xExpected; - uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength ); + NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + const uint32_t ulIpv4UdpOffset = 42, ulIpv6UdpOffset = 62; + uint8_t *pPayloadBuffer; + size_t uxPayloadBufferLength; - __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, - "NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" ); + __CPROVER_assert( TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE, + "TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" ); __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); - __CPROVER_assume( uxBufferLength <= NETWORK_BUFFER_SIZE ); - __CPROVER_assume( pucUDPPayloadBuffer != NULL ); - - uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer, - uxBufferLength, - xExpected ); -} + __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE ); + + lIsIPv6Packet = IS_TESTING_IPV6; + + xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength ); + xNetworkBuffer.xDataLength = uxBufferLength; + xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp; + + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); + if( lIsIPv6Packet ) + { + __CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */ + pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset; + uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset; + } + else + { + __CPROVER_assume( uxBufferLength >= ulIpv4UdpOffset ); /* 42 is total size of IPv4 UDP header, including ethernet, IPv4, UDP headers. */ + pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv4UdpOffset; + uxPayloadBufferLength = uxBufferLength - ulIpv4UdpOffset; + } + + uint32_t index = DNS_ParseDNSReply( pPayloadBuffer, + uxPayloadBufferLength, + &pxAddressInfo, + xExpected, + usPort ); +} \ No newline at end of file diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json b/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json index aefd62da6..d22815651 100644 --- a/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json +++ b/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json @@ -1,68 +1,50 @@ -# The proof depends on one parameter: -# NETWORK_BUFFER_SIZE is the size of the network buffer being parsed -# The buffer size must be bounded because we must bound the number of -# iterations loops iterating over the buffer. - { - "ENTRY": "ParseDNSReply", - -################################################################ -# This is the network buffer size. -# Reasonable values are size > 12 = sizeof(xDNSMessage) - "NETWORK_BUFFER_SIZE": 40, - -################################################################ -# This is the size of the buffer into which the name is copied. -# Set to any positive value. -# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE -# In the proof, NAME_SIZE >= 4 required for good coverage. - "NAME_SIZE": "10", - -################################################################ -# Loop prvParseDNSReply.0: -# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 915 - "PARSELOOP0": "prvParseDNSReply.0", - -# M = sizeof( DNSMessage_t ) = 12 -# U = sizeof( uint32_t) = 4 -# Loop bound is (NETWORK_BUFFER_SIZE - M) div (U+1) + 1 tight for SIZE >= M -# Loop bound is 1 for 0 <= SIZE < M - "PARSELOOP0_UNWIND": - "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 12) / 5 + 1", - -################################################################ -# Loop prvParseDNSReply.1: -# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 989 - "PARSELOOP1": "prvParseDNSReply.1", - -# A = sizeof( DNSAnswerRecord_t ) = 10 -# M = sizeof( DNSMessage_t ) = 12 -# U = sizeof( uint32_t) = 4 -# Loop bound is (NETWORK_BUFFER_SIZE - M - A) div (A+1) + A + 1 tight -# for SIZE >= M + A -# Loop bound is (NETWORK_BUFFER_SIZE - M) + 1 for M <= SIZE < M + A -# Loop bound is 1 for 0 <= SIZE < M - "PARSELOOP1_UNWIND": - "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 11 if {NETWORK_BUFFER_SIZE} < 22 else ({NETWORK_BUFFER_SIZE} - 12 - 10) / 11 + 11)", - -################################################################ - + "ENTRY": "DNS_ParseDNSReply", + "TEST_PAYLOAD_SIZE": 5, + "TEST_IPV4_PACKET_SIZE": 59, + "TEST_IPV6_PACKET_SIZE": 79, "CBMCFLAGS": [ "--unwind 1", - "--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5" + "--unwindset DNS_ParseDNSReply.0:{TEST_PAYLOAD_SIZE}", + "--unwindset DNS_ReadNameField.0:{TEST_PAYLOAD_SIZE}", + "--unwindset DNS_ReadNameField.1:{TEST_PAYLOAD_SIZE}", + "--unwindset parseDNSAnswer.0:{TEST_PAYLOAD_SIZE}", + "--unwindset strncpy.0:{TEST_PAYLOAD_SIZE}" + ], + "OPT": + [ + "--export-file-local-symbols" ], - "OBJS": [ "$(ENTRY)_harness.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto", - "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto" ], - "DEF": [ - "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", - "NAME_SIZE={NAME_SIZE}" + { + "IPv4": + [ + "TEST_PACKET_SIZE={TEST_IPV4_PACKET_SIZE}", + "ipconfigUSE_LLMNR=1", + "ipconfigUSE_MDNS=1", + "IS_TESTING_IPV6=0" + ] + }, + { + "IPv6": + [ + "TEST_PACKET_SIZE={TEST_IPV6_PACKET_SIZE}", + "ipconfigUSE_LLMNR=1", + "ipconfigUSE_MDNS=1", + "IS_TESTING_IPV6=1" + ] + } + ], + "INC": + [ + "$(FREERTOS_PLUS_TCP)/test/cbmc/include" ] -} +} \ No newline at end of file From 221ef8638aebde399d63a0488adbd3419a60529b Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 12:09:42 +0530 Subject: [PATCH 04/10] Fix CBMC proof --- .../DNS_ParseDNSReply/{Makefile.json => Configurations.json} | 0 test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename test/cbmc/proofs/DNS_ParseDNSReply/{Makefile.json => Configurations.json} (100%) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json b/test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json similarity index 100% rename from test/cbmc/proofs/DNS_ParseDNSReply/Makefile.json rename to test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c index 9432b9277..13ee9a8ef 100644 --- a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c +++ b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c @@ -17,7 +17,7 @@ #include "IPTraceMacroDefaults.h" #include "cbmc.h" -#include "../../../utility/memory_assignments.c" +#include "../../utility/memory_assignments.c" /**************************************************************** * Signature of function under test From 5d0dfb636daa7f566a2f6d26bce69935cbd082a2 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 13:00:47 +0530 Subject: [PATCH 05/10] Fix unit tests --- test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c index 0eab41c75..4f0803512 100644 --- a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c +++ b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c @@ -2789,7 +2789,7 @@ void test_parseDNSAnswer_recordNOTstored_gt_count_diffUsType( void ) ret = parseDNSAnswer( &xSet, &pxAddressInfo, &uxBytesRead ); TEST_ASSERT_EQUAL( 0, ret ); - TEST_ASSERT_EQUAL( 40, uxBytesRead ); + TEST_ASSERT_EQUAL( 0, uxBytesRead ); } /** From 51020f5bb783e51108b62e4ab5e82d27334ec87f Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 13:02:25 +0530 Subject: [PATCH 06/10] Fix formatting --- .../proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c index 13ee9a8ef..9fae89ddc 100644 --- a/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c +++ b/test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c @@ -169,11 +169,11 @@ void harness() { size_t uxBufferLength; uint16_t usPort; - struct freertos_addrinfo *pxAddressInfo; + struct freertos_addrinfo * pxAddressInfo; BaseType_t xExpected; NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); const uint32_t ulIpv4UdpOffset = 42, ulIpv6UdpOffset = 62; - uint8_t *pPayloadBuffer; + uint8_t * pPayloadBuffer; size_t uxPayloadBufferLength; __CPROVER_assert( TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE, @@ -187,8 +187,9 @@ void harness() xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength ); xNetworkBuffer.xDataLength = uxBufferLength; xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp; - + __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL ); + if( lIsIPv6Packet ) { __CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */ @@ -207,4 +208,4 @@ void harness() &pxAddressInfo, xExpected, usPort ); -} \ No newline at end of file +} From dbcd08c7722fc8f36bdb23298cb87784aba99f3c Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 13:06:10 +0530 Subject: [PATCH 07/10] Fix unit tests --- test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c | 2 -- 1 file changed, 2 deletions(-) diff --git a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c index 4f0803512..b4a6fd294 100644 --- a/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c +++ b/test/unit-test/FreeRTOS_DNS_Parser/FreeRTOS_DNS_Parser_utest.c @@ -2784,8 +2784,6 @@ void test_parseDNSAnswer_recordNOTstored_gt_count_diffUsType( void ) pxDNSAnswerRecord->usDataLength = FreeRTOS_htons( ipSIZE_OF_IPv4_ADDRESS ); pxDNSAnswerRecord->usType = ( dnsTYPE_AAAA_HOST ); - usChar2u16_ExpectAnyArgsAndReturn( dnsTYPE_AAAA_HOST ); /* usType */ - ret = parseDNSAnswer( &xSet, &pxAddressInfo, &uxBytesRead ); TEST_ASSERT_EQUAL( 0, ret ); From 506db4e9d44c3ea516ab610e2a94adda1bb3ad98 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 14:39:33 +0530 Subject: [PATCH 08/10] Update CMake --- CMakeLists.txt | 8 -------- 1 file changed, 8 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 18c3ca51d..10becb0c1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -243,11 +243,3 @@ add_subdirectory(tools) add_subdirectory(test) FetchContent_MakeAvailable(freertos_kernel cmock) - -# Note following are can be removed once FreeRTOS-Kernel v10.5.0 + fixes their issues. -# To ignore header specific issues - change all of the headers to SYSTEM -set(_freertos_kernel_targets freertos_kernel freertos_kernel_port) -# foreach (_target ${_freertos_kernel_targets} ) -# get_target_property( interface_directories ${_target} INTERFACE_INCLUDE_DIRECTORIES ) -# set_target_properties(${_target} PROPERTIES INTERFACE_SYSTEM_INCLUDE_DIRECTORIES "${interface_directories}" ) -# endforeach() From d77d7b40adaf6d8290d54bb379989c2968dca967 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 17:05:27 +0530 Subject: [PATCH 09/10] Fix build checks --- CMakeLists.txt | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 10becb0c1..2b863eda9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -198,6 +198,10 @@ add_compile_options( $<$:-fdiagnostics-color=always> $<$:-fcolor-diagnostics> + ## Suppress warnings from kernel port files. + $<$:-Wno-sign-compare> + $<$:-Wno-sign-conversion> + $<$:-Wall> $<$:-Wextra> $<$:-Werror> @@ -243,3 +247,11 @@ add_subdirectory(tools) add_subdirectory(test) FetchContent_MakeAvailable(freertos_kernel cmock) + +# Note following are can be removed once FreeRTOS-Kernel v10.5.0 + fixes their issues. +# To ignore header specific issues - change all of the headers to SYSTEM +set(_freertos_kernel_targets freertos_kernel freertos_kernel_port) +# foreach (_target ${_freertos_kernel_targets} ) +# get_target_property( interface_directories ${_target} INTERFACE_INCLUDE_DIRECTORIES ) +# set_target_properties(${_target} PROPERTIES INTERFACE_SYSTEM_INCLUDE_DIRECTORIES "${interface_directories}" ) +# endforeach() From 0de1d0135d9de8240cf777c4777c3fff8264c98a Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 12 Jun 2024 17:20:25 +0530 Subject: [PATCH 10/10] Fix formatting --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2b863eda9..e73b23d3c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -201,7 +201,7 @@ add_compile_options( ## Suppress warnings from kernel port files. $<$:-Wno-sign-compare> $<$:-Wno-sign-conversion> - + $<$:-Wall> $<$:-Wextra> $<$:-Werror>