diff --git a/source/core_http_client.c b/source/core_http_client.c index 128a1d51..927028c3 100644 --- a/source/core_http_client.c +++ b/source/core_http_client.c @@ -2099,11 +2099,11 @@ HTTPStatus_t HTTPClient_ReceiveAndParseHttpResponse( const TransportInterface_t ( totalReceived < pResponse->bufferLen ) ) ? 1U : 0U; } - if( ( returnStatus == HTTPParserPaused ) && pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) + if( ( returnStatus == HTTPParserPaused ) && ( pResponse->respOptionFlags & HTTP_RESPONSE_DO_NOT_PARSE_BODY_FLAG ) ) { returnStatus = HTTPSuccess; /* There may be dangling data if we parse with do not parse body flag. To let libraries built on top of corehttp we expose it through body. */ - pResponse->bodyLen = totalReceived - ( ( uint8_t * ) pResponse->pBody - pResponse->pBuffer ); + pResponse->bodyLen = totalReceived - ( size_t )( ( ( uintptr_t ) pResponse->pBody ) - ( ( uintptr_t ) pResponse->pBuffer ) ); } if( returnStatus == HTTPSuccess ) diff --git a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c index 8ceb72dd..8f630ba3 100644 --- a/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c +++ b/test/cbmc/stubs/HTTPClient_Send_llhttp_execute.c @@ -80,5 +80,22 @@ llhttp_errno_t llhttp_execute( llhttp_t * parser, pParsingContext->lastHeaderValueLen = 0U; } + /* The body pointer is set by the httpParserOnBodyCallback. But since we are + * removing that from CBMC proof execution, the body has to be set here. */ + size_t bodyOffset; + + if( pParsingContext->pResponse->bufferLen == 0 ) + { + bodyOffset = 0; + } + else + { + /* Body offset can be anything as long as it doesn't exceed the buffer length + * and the length of the current data packet. */ + __CPROVER_assume( bodyOffset < pParsingContext->pResponse->bufferLen ); + __CPROVER_assume( bodyOffset < len ); + } + pParsingContext->pResponse->pBody = pParsingContext->pBufferCur + bodyOffset; + return parser->error; }