bug.patch

diff --git a/test/cbmc/sources/http_cbmc_state.c b/test/cbmc/sources/http_cbmc_state.c
index 004e428..beb8993 100644
--- a/test/cbmc/sources/http_cbmc_state.c
+++ b/test/cbmc/sources/http_cbmc_state.c
@@ -44,7 +44,7 @@ HTTPRequestHeaders_t * allocateHttpRequestHeaders( HTTPRequestHeaders_t * pReque
 
     if( pRequestHeaders != NULL )
     {
-        __CPROVER_assume( pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE );
+        // __CPROVER_assume( pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE );
         pRequestHeaders->pBuffer = mallocCanFail( pRequestHeaders->bufferLen );
     }
 
@@ -73,13 +73,13 @@ HTTPRequestInfo_t * allocateHttpRequestInfo( HTTPRequestInfo_t * pRequestInfo )
 
     if( pRequestInfo != NULL )
     {
-        __CPROVER_assume( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE );
+        // __CPROVER_assume( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE );
         pRequestInfo->pMethod = mallocCanFail( pRequestInfo->methodLen );
 
-        __CPROVER_assume( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE );
+        // __CPROVER_assume( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE );
         pRequestInfo->pHost = mallocCanFail( pRequestInfo->hostLen );
 
-        __CPROVER_assume( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
+        // __CPROVER_assume( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
         pRequestInfo->pPath = mallocCanFail( pRequestInfo->pathLen );
     }
 
@@ -111,10 +111,10 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
 
     if( pResponse != NULL )
     {
-        __CPROVER_assume( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE );
+        // __CPROVER_assume( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE );
         pResponse->pBuffer = mallocCanFail( pResponse->bufferLen );
 
-        __CPROVER_assume( headerOffset <= pResponse->bufferLen );
+        // __CPROVER_assume( headerOffset <= pResponse->bufferLen );
 
         if( pResponse->pBuffer != NULL )
         {
@@ -128,7 +128,7 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
         {
             /* The length of the headers MUST be between the start of the
              * headers and the end of the buffer. */
-            __CPROVER_assume( pResponse->headersLen < ( pResponse->bufferLen - headerOffset ) );
+            // __CPROVER_assume( pResponse->headersLen < ( pResponse->bufferLen - headerOffset ) );
         }
 
         if( pResponse->bufferLen == 0 )
@@ -137,7 +137,7 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
         }
         else
         {
-            __CPROVER_assume( bodyOffset <= pResponse->bufferLen );
+            // __CPROVER_assume( bodyOffset <= pResponse->bufferLen );
         }
 
         if( pResponse->pBuffer != NULL )
@@ -150,7 +150,7 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
          * of the buffer. */
         if( pResponse->pBody )
         {
-            __CPROVER_assume( pResponse->bodyLen < ( pResponse->bufferLen - bodyOffset ) );
+            // __CPROVER_assume( pResponse->bodyLen < ( pResponse->bufferLen - bodyOffset ) );
         }
     }
 
@@ -207,11 +207,11 @@ llhttp_t * allocateHttpSendParser( llhttp_t * pHttpParser )
     if( pHttpParser == NULL )
     {
         pHttpParser = malloc( sizeof( llhttp_t ) );
-        __CPROVER_assume( pHttpParser != NULL );
+        // __CPROVER_assume( pHttpParser != NULL );
     }
 
     pHttpParsingContext = allocateHttpSendParsingContext( NULL );
-    __CPROVER_assume( isValidHttpSendParsingContext( pHttpParsingContext ) );
+    // __CPROVER_assume( isValidHttpSendParsingContext( pHttpParsingContext ) );
     pHttpParser->data = ( void * ) pHttpParsingContext;
 
     return pHttpParser;
@@ -225,16 +225,16 @@ HTTPParsingContext_t * allocateHttpSendParsingContext( HTTPParsingContext_t * pH
     if( pHttpParsingContext == NULL )
     {
         pHttpParsingContext = malloc( sizeof( HTTPParsingContext_t ) );
-        __CPROVER_assume( pHttpParsingContext != NULL );
+        // __CPROVER_assume( pHttpParsingContext != NULL );
 
         pResponse = allocateHttpResponse( NULL );
-        __CPROVER_assume( isValidHttpResponse( pResponse ) &&
-                          pResponse != NULL &&
-                          pResponse->pBuffer != NULL &&
-                          pResponse->bufferLen > 0 );
+        // __CPROVER_assume( isValidHttpResponse( pResponse ) &&
+        //                  pResponse != NULL &&
+        //                  pResponse->pBuffer != NULL &&
+        //                  pResponse->bufferLen > 0 );
         pHttpParsingContext->pResponse = pResponse;
 
-        __CPROVER_assume( bufferOffset < pResponse->bufferLen );
+        // __CPROVER_assume( bufferOffset < pResponse->bufferLen );
         pHttpParsingContext->pBufferCur = pResponse->pBuffer + bufferOffset;
     }
 
@@ -258,7 +258,7 @@ llhttp_t * allocateHttpReadHeaderParser( llhttp_t * pHttpParser )
     if( pHttpParser == NULL )
     {
         pHttpParser = malloc( sizeof( llhttp_t ) );
-        __CPROVER_assume( pHttpParser != NULL );
+        // __CPROVER_assume( pHttpParser != NULL );
     }
 
     pFindHeaderContext = allocateFindHeaderContext( NULL );
@@ -272,7 +272,7 @@ findHeaderContext_t * allocateFindHeaderContext( findHeaderContext_t * pFindHead
     if( pFindHeaderContext == NULL )
     {
         pFindHeaderContext = malloc( sizeof( findHeaderContext_t ) );
-        __CPROVER_assume( pFindHeaderContext != NULL );
+        // __CPROVER_assume( pFindHeaderContext != NULL );
     }
 
     return pFindHeaderContext;