Fix CBMC proof of Send function

FreeRTOS · Jan 19, 2024 · c6b8308 · c6b8308
1 parent 4324547
commit c6b8308
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 2 deletions.
diff --git 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
@@ -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;
 }