diff --git a/docs/doxygen/include/size_table.html b/docs/doxygen/include/size_table.html index 482a08a6..41bc6338 100644 --- a/docs/doxygen/include/size_table.html +++ b/docs/doxygen/include/size_table.html @@ -9,8 +9,8 @@ core_http_client.c -
3.1K
-
2.5K
+
3.2K
+
2.6K
http_parser.c (http-parser) @@ -19,7 +19,7 @@ Total estimates -
18.8K
-
15.5K
+
18.9K
+
15.6K
diff --git a/lexicon.txt b/lexicon.txt index 028e065e..ac4cdeff 100644 --- a/lexicon.txt +++ b/lexicon.txt @@ -233,6 +233,7 @@ sendflags sendhttpbody sendhttpheaders sendpartialcall +sensitivity sizeof snprintf statuscode diff --git a/source/core_http_client.c b/source/core_http_client.c index a3ba100a..c33675ad 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -27,6 +27,7 @@ #include #include +#include #include "core_http_client.h" #include "core_http_client_private.h" @@ -544,6 +545,22 @@ static void processCompleteHeader( HTTPParsingContext_t * pParsingContext ); */ static HTTPStatus_t processHttpParserError( const http_parser * pHttpParser ); +/** + * @brief Compares at most the first n bytes of str1 and str2 without case sensitivity + * and n must be less than the actual size of either string. + * + * @param[in] str1 First string to be compared. + * @param[in] str2 Second string to be compared. + * @param[in] n The maximum number of characters to be compared. + * + * @return One of the following: + * 0 if str1 is equal to str2 + * 1 if str1 is not equal to str2. + */ +static int8_t caseInsensitiveStringCmp( const char * str1, + const char * str2, + size_t n ); + /*-----------------------------------------------------------*/ static uint32_t getZeroTimestampMs( void ) @@ -553,6 +570,25 @@ static uint32_t getZeroTimestampMs( void ) /*-----------------------------------------------------------*/ +static int8_t caseInsensitiveStringCmp( const char * str1, + const char * str2, + size_t n ) +{ + size_t i = 0U; + + for( i = 0U; i < n; i++ ) + { + if( toupper( str1[ i ] ) != toupper( str2[ i ] ) ) + { + break; + } + } + + return ( i == n ) ? 0 : 1; +} + +/*-----------------------------------------------------------*/ + static void processCompleteHeader( HTTPParsingContext_t * pParsingContext ) { HTTPResponse_t * pResponse = NULL; @@ -2237,7 +2273,7 @@ static int findHeaderFieldParserCallback( http_parser * pHttpParser, /* Check whether the parsed header matches the header we are looking for. */ /* Each header field consists of a case-insensitive field name (RFC 7230, section 3.2). */ if( ( fieldLen == pContext->fieldLen ) && - ( strncasecmp( pContext->pField, pFieldLoc, fieldLen ) == 0 ) ) + ( caseInsensitiveStringCmp( pContext->pField, pFieldLoc, fieldLen ) == 0 ) ) { LogDebug( ( "Found header field in response: " "HeaderName=%.*s, HeaderLocation=0x%p", diff --git a/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile b/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile index e66e02d2..cb66ad21 100644 --- a/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile +++ b/test/cbmc/proofs/findHeaderFieldParserCallback/Makefile @@ -7,13 +7,13 @@ HARNESS_FILE=$(HARNESS_ENTRY) # The header field length is bounded, so strncasecmp can be unwound to an expected # amount that won't make the proof run too long. -MAX_HEADER_FIELD_LENGTH=10 +MAX_HEADER_FIELD_LENGTH=11 DEFINES += -DMAX_HEADER_FIELD_LENGTH=$(MAX_HEADER_FIELD_LENGTH) INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += strncasecmp.0:$(MAX_HEADER_FIELD_LENGTH) +UNWINDSET += __CPROVER_file_local_core_http_client_c_caseInsensitiveStringCmp.0:$(MAX_HEADER_FIELD_LENGTH) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/http_cbmc_state.c diff --git a/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c b/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c index 67fe42c8..df53c14a 100644 --- a/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c +++ b/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c @@ -46,7 +46,7 @@ void findHeaderFieldParserCallback_harness() pResponse->pBuffer != NULL && pResponse->bufferLen > 0 ); - __CPROVER_assume( 0 < fieldLen && fieldLen <= MAX_HEADER_FIELD_LENGTH && fieldLen <= pResponse->bufferLen ); + __CPROVER_assume( 0 < fieldLen && fieldLen < MAX_HEADER_FIELD_LENGTH && fieldLen <= pResponse->bufferLen ); __CPROVER_assume( fieldOffset <= pResponse->bufferLen - fieldLen ); pFieldLoc = pResponse->pBuffer + fieldOffset;