Fix formatting and CBMC proofs

FreeRTOS · Sep 21, 2022 · f792ab0 · f792ab0
1 parent 0737ab4
commit f792ab0
Show file tree

Hide file tree

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