diff --git a/source/core_mqtt.c b/source/core_mqtt.c index a42b10ca7..b8a0a5fc9 100644 --- a/source/core_mqtt.c +++ b/source/core_mqtt.c @@ -736,7 +736,6 @@ static int32_t sendMessageVector( MQTTContext_t * pContext, uint32_t timeoutTime; uint32_t bytesToSend = 0U; int32_t bytesSentOrError = 0; - uint64_t temp = 0; TransportOutVector_t * pIoVectIterator; size_t vectorsToBeSent = ioVecCount; @@ -751,7 +750,6 @@ static int32_t sendMessageVector( MQTTContext_t * pContext, /* Count the total number of bytes to be sent as outlined in the vector. */ for( pIoVectIterator = pIoVec; pIoVectIterator <= &( pIoVec[ ioVecCount - 1U ] ); pIoVectIterator++ ) { - temp += pIoVectIterator->iov_len; bytesToSend += ( uint32_t ) pIoVectIterator->iov_len; } @@ -785,9 +783,7 @@ static int32_t sendMessageVector( MQTTContext_t * pContext, { bytesSentOrError = sendResult; - /* We do not need to break here as this condition is checked in - * the loop. The following code will not execute as bytesSentThisVector - * is not updated and is still 0. */ + break; } while( ( pIoVectIterator <= &( pIoVec[ ioVecCount - 1U ] ) ) && diff --git a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c index 08584126c..ea6397289 100644 --- a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c +++ b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c @@ -33,7 +33,7 @@ void harness() pContext = allocateMqttContext( NULL ); __CPROVER_assume( isValidMqttContext( pContext ) ); - __CPROVER_assume( pContext != NULL ); + __CPROVER_assume( pContext != NULL ); __CPROVER_assume( pContext->networkBuffer.pBuffer != NULL ); MQTT_Disconnect( pContext );