diff --git a/source/core_http_client.c b/source/core_http_client.c
index 6f52de4d..405aaa1f 100644
--- a/source/core_http_client.c
+++ b/source/core_http_client.c
@@ -1727,6 +1727,11 @@ HTTPStatus_t HTTPClient_AddRangeHeader( HTTPRequestHeaders_t * pRequestHeaders,
LogError( ( "Parameter check failed: pRequestHeaders->pBuffer is NULL." ) );
returnStatus = HTTPInvalidParameter;
}
+ else if( pRequestHeaders->bufferLen > UINT32_MAX )
+ {
+ LogError( ( "Parameter check failed: pRequestHeaders->bufferLen > UINT32_MAX." ) );
+ returnStatus = HTTPInvalidParameter;
+ }
else if( pRequestHeaders->headersLen > pRequestHeaders->bufferLen )
{
LogError( ( "Parameter check failed: pRequestHeaders->headersLen > pRequestHeaders->bufferLen." ) );
diff --git a/test/cbmc/include/http_cbmc_state.h b/test/cbmc/include/http_cbmc_state.h
index 621c3dd1..a4dc3492 100644
--- a/test/cbmc/include/http_cbmc_state.h
+++ b/test/cbmc/include/http_cbmc_state.h
@@ -46,19 +46,6 @@ struct NetworkContext
*/
bool nondet_bool();
-/**
- * @brief Calls malloc based on given size or returns NULL for coverage.
- *
- * Implementation of safe malloc which returns NULL if the requested size is 0.
- * The behavior of malloc(0) is platform dependent.
- * It is possible for malloc(0) to return an address without allocating memory.
- *
- * @param[in] size Requested size to malloc.
- *
- * @return Requested memory or NULL.
- */
-void * mallocCanFail( size_t size );
-
/**
* @brief Allocates an #HTTPRequestHeaders_t object.
*
diff --git a/test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c b/test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c
index 0394e68c..25fbee9a 100644
--- a/test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c
+++ b/test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c
@@ -42,12 +42,10 @@ void HTTPClient_AddHeader_harness()
__CPROVER_assume( isValidHttpRequestHeaders( pRequestHeaders ) );
/* Initialize and make assumptions for header field. */
- __CPROVER_assume( fieldLen < CBMC_MAX_OBJECT_SIZE );
- pField = mallocCanFail( fieldLen );
+ pField = malloc( fieldLen );
/* Initialize and make assumptions for header value. */
- __CPROVER_assume( valueLen < CBMC_MAX_OBJECT_SIZE );
- pValue = mallocCanFail( valueLen );
+ pValue = malloc( valueLen );
HTTPClient_AddHeader( pRequestHeaders,
pField, fieldLen, pValue, valueLen );
diff --git a/test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c b/test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c
index 5ee4842e..8aeff82d 100644
--- a/test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c
+++ b/test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c
@@ -38,12 +38,10 @@ void HTTPClient_ReadHeader_harness()
size_t valueLen;
/* Initialize and make assumptions for header field. */
- __CPROVER_assume( fieldLen < CBMC_MAX_OBJECT_SIZE );
- pField = mallocCanFail( fieldLen );
+ pField = malloc( fieldLen );
/* Initialize and make assumptions for header value. */
- __CPROVER_assume( valueLen < CBMC_MAX_OBJECT_SIZE );
- pValue = mallocCanFail( sizeof( char * ) );
+ pValue = malloc( sizeof( char * ) );
/* Initialize and make assumptions for response object. */
pResponse = allocateHttpResponse( NULL );
diff --git a/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c b/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c
index 82258fd4..f399ff25 100644
--- a/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c
+++ b/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c
@@ -44,8 +44,7 @@ void HTTPClient_Send_harness()
__CPROVER_assume( isValidHttpRequestHeaders( pRequestHeaders ) );
/* Initialize and make assumptions for buffer to receive request body. */
- __CPROVER_assume( reqBodyBufLen < CBMC_MAX_OBJECT_SIZE );
- pRequestBodyBuf = mallocCanFail( reqBodyBufLen );
+ pRequestBodyBuf = malloc( reqBodyBufLen );
/* Initialize and make assumptions for response object. */
pResponse = allocateHttpResponse( NULL );
diff --git a/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c b/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
index c0b98f2f..70b83ce5 100644
--- a/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
+++ b/test/cbmc/proofs/findHeaderFieldParserCallback/findHeaderFieldParserCallback_harness.c
@@ -54,7 +54,6 @@ void findHeaderFieldParserCallback_harness()
__CPROVER_assume( fieldOffset <= pResponse->bufferLen - fieldLen );
pFieldLoc = pResponse->pBuffer + fieldOffset;
- __CPROVER_assume( 0 < fieldContextLen && fieldContextLen < CBMC_MAX_OBJECT_SIZE );
pFindHeaderContext->pField = ( char * ) malloc( fieldContextLen );
__CPROVER_assume( pFindHeaderContext->pField != NULL );
pFindHeaderContext->fieldLen = fieldContextLen;
diff --git a/test/cbmc/sources/http_cbmc_state.c b/test/cbmc/sources/http_cbmc_state.c
index f61be4e1..7be31cd0 100644
--- a/test/cbmc/sources/http_cbmc_state.c
+++ b/test/cbmc/sources/http_cbmc_state.c
@@ -29,23 +29,16 @@
#include "http_cbmc_state.h"
-void * mallocCanFail( size_t size )
-{
- __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "mallocCanFail size is too big" );
- return malloc( size );
-}
-
HTTPRequestHeaders_t * allocateHttpRequestHeaders( HTTPRequestHeaders_t * pRequestHeaders )
{
if( pRequestHeaders == NULL )
{
- pRequestHeaders = mallocCanFail( sizeof( HTTPRequestHeaders_t ) );
+ pRequestHeaders = malloc( sizeof( HTTPRequestHeaders_t ) );
}
if( pRequestHeaders != NULL )
{
- __CPROVER_assume( pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE );
- pRequestHeaders->pBuffer = mallocCanFail( pRequestHeaders->bufferLen );
+ pRequestHeaders->pBuffer = malloc( pRequestHeaders->bufferLen );
}
return pRequestHeaders;
@@ -54,13 +47,6 @@ HTTPRequestHeaders_t * allocateHttpRequestHeaders( HTTPRequestHeaders_t * pReque
bool isValidHttpRequestHeaders( const HTTPRequestHeaders_t * pRequestHeaders )
{
bool isValid = true;
-
- if( pRequestHeaders )
- {
- isValid = pRequestHeaders->bufferLen < CBMC_MAX_OBJECT_SIZE &&
- pRequestHeaders->headersLen < CBMC_MAX_OBJECT_SIZE;
- }
-
return isValid;
}
@@ -68,19 +54,14 @@ HTTPRequestInfo_t * allocateHttpRequestInfo( HTTPRequestInfo_t * pRequestInfo )
{
if( pRequestInfo == NULL )
{
- pRequestInfo = mallocCanFail( sizeof( HTTPRequestInfo_t ) );
+ pRequestInfo = malloc( sizeof( HTTPRequestInfo_t ) );
}
if( pRequestInfo != NULL )
{
- __CPROVER_assume( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE );
- pRequestInfo->pMethod = mallocCanFail( pRequestInfo->methodLen );
-
- __CPROVER_assume( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE );
- pRequestInfo->pHost = mallocCanFail( pRequestInfo->hostLen );
-
- __CPROVER_assume( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
- pRequestInfo->pPath = mallocCanFail( pRequestInfo->pathLen );
+ pRequestInfo->pMethod = malloc( pRequestInfo->methodLen );
+ pRequestInfo->pHost = malloc( pRequestInfo->hostLen );
+ pRequestInfo->pPath = malloc( pRequestInfo->pathLen );
}
return pRequestInfo;
@@ -89,14 +70,6 @@ HTTPRequestInfo_t * allocateHttpRequestInfo( HTTPRequestInfo_t * pRequestInfo )
bool isValidHttpRequestInfo( const HTTPRequestInfo_t * pRequestInfo )
{
bool isValid = true;
-
- if( pRequestInfo )
- {
- isValid = ( pRequestInfo->methodLen < CBMC_MAX_OBJECT_SIZE ) &&
- ( pRequestInfo->hostLen < CBMC_MAX_OBJECT_SIZE ) &&
- ( pRequestInfo->pathLen < CBMC_MAX_OBJECT_SIZE );
- }
-
return isValid;
}
@@ -106,13 +79,12 @@ HTTPResponse_t * allocateHttpResponse( HTTPResponse_t * pResponse )
if( pResponse == NULL )
{
- pResponse = mallocCanFail( sizeof( HTTPResponse_t ) );
+ pResponse = malloc( sizeof( HTTPResponse_t ) );
}
if( pResponse != NULL )
{
- __CPROVER_assume( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE );
- pResponse->pBuffer = mallocCanFail( pResponse->bufferLen );
+ pResponse->pBuffer = malloc( pResponse->bufferLen );
__CPROVER_assume( headerOffset <= pResponse->bufferLen );
@@ -163,8 +135,7 @@ bool isValidHttpResponse( const HTTPResponse_t * pResponse )
if( pResponse )
{
- isValid = ( pResponse->bufferLen < CBMC_MAX_OBJECT_SIZE ) &&
- ( pResponse->bodyLen < pResponse->bufferLen ) &&
+ isValid = ( pResponse->bodyLen < pResponse->bufferLen ) &&
( pResponse->headersLen < pResponse->bufferLen );
isValid = isValid || pResponse->pBody == NULL;
}
@@ -176,12 +147,12 @@ TransportInterface_t * allocateTransportInterface( TransportInterface_t * pTrans
{
if( pTransport == NULL )
{
- pTransport = mallocCanFail( sizeof( TransportInterface_t ) );
+ pTransport = malloc( sizeof( TransportInterface_t ) );
}
if( pTransport != NULL )
{
- pTransport->pNetworkContext = mallocCanFail( sizeof( NetworkContext_t ) );
+ pTransport->pNetworkContext = malloc( sizeof( NetworkContext_t ) );
}
return pTransport;
@@ -244,10 +215,6 @@ HTTPParsingContext_t * allocateHttpSendParsingContext( HTTPParsingContext_t * pH
bool isValidHttpSendParsingContext( const HTTPParsingContext_t * pHttpParsingContext )
{
bool isValid = true;
-
- isValid = isValid && ( pHttpParsingContext->lastHeaderFieldLen ) <= ( SIZE_MAX - CBMC_MAX_OBJECT_SIZE );
- isValid = isValid && ( pHttpParsingContext->lastHeaderValueLen ) <= ( SIZE_MAX - CBMC_MAX_OBJECT_SIZE );
-
return isValid;
}
diff --git a/test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c b/test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
index ff6d9281..d462ade6 100644
--- a/test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
+++ b/test/cbmc/stubs/HTTPClient_ReadHeader_http_parser_execute.c
@@ -54,8 +54,6 @@ size_t http_parser_execute( http_parser * parser,
"http_parser_execute settings is NULL" );
__CPROVER_assert( data != NULL,
"http_parser_execute data is NULL" );
- __CPROVER_assert( len < CBMC_MAX_OBJECT_SIZE,
- "http_parser_execute len >= CBMC_MAX_OBJECT_SIZE" );
parser->http_errno = http_errno;
diff --git a/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c b/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
index 45b8ccd9..9b7d1686 100644
--- a/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
+++ b/test/cbmc/stubs/HTTPClient_Send_http_parser_execute.c
@@ -52,8 +52,6 @@ size_t http_parser_execute( http_parser * parser,
"http_parser_execute settings is NULL" );
__CPROVER_assert( data != NULL,
"http_parser_execute data is NULL" );
- __CPROVER_assert( len < CBMC_MAX_OBJECT_SIZE,
- "http_parser_execute len >= CBMC_MAX_OBJECT_SIZE" );
__CPROVER_assume( fieldLength <= len );
__CPROVER_assume( valueLength <= len );