From c6b830855921fb98cde2193743d52485edf4dba3 Mon Sep 17 00:00:00 2001
From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
Date: Fri, 19 Jan 2024 01:00:10 +0000
Subject: [PATCH] Fix CBMC proof of Send function

---
 source/core_http_client.c                       |  4 ++--
 .../cbmc/stubs/HTTPClient_Send_llhttp_execute.c | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

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;
 }