Merge branch 'RmvCmnBuffer' of https://github.com/AniruddhaKanhere/co…

…reMQTT into RmvCmnBuffer

docs/doxygen/include/size_table.md

@@ -9,8 +9,8 @@
     </tr>
     <tr>
         <td>core_mqtt.c</td>
-        <td><center>3.6K</center></td>
-        <td><center>3.1K</center></td>
+        <td><center>3.8K</center></td>
+        <td><center>3.2K</center></td>
     </tr>
     <tr>
         <td>core_mqtt_state.c</td>
@@ -24,7 +24,7 @@
     </tr>
     <tr>
         <td><b>Total estimates</b></td>
-        <td><b><center>7.9K</center></b></td>
-        <td><b><center>6.4K</center></b></td>
+        <td><b><center>8.1K</center></b></td>
+        <td><b><center>6.5K</center></b></td>
     </tr>
 </table>

source/core_mqtt.c

@@ -31,7 +31,6 @@
 #include "core_mqtt_state.h"
 #include "core_mqtt_default_logging.h"
 
-#define MQTT_SUB_UNSUB_MAX_VECTORS             ( 4U )
 /*-----------------------------------------------------------*/
 
 /**
@@ -157,7 +156,8 @@ static void addWillAndConnectInfo( const MQTTConnectInfo_t * pConnectInfo,
  * directly sending it.
  *
  * @param[in] pContext Initialized MQTT context.
- * @param[in] pSubscription MQTT subscription info.
+ * @param[in] pSubscriptionList List of MQTT subscription info.
+ * @param[in] subscriptionCount The count of elements in the list.
  * @param[in] packetId The packet ID of the subscribe packet
  * @param[in] remainingLength The remaining length of the subscribe packet.
  *
@@ -174,7 +174,8 @@ static MQTTStatus_t sendSubscribeWithoutCopy( MQTTContext_t * pContext,
  * directly sending it.
  *
  * @param[in] pContext Initialized MQTT context.
- * @param[in] pSubscription MQTT subscription info.
+ * @param[in] pSubscriptionList MQTT subscription info.
+ * @param[in] subscriptionCount The count of elements in the list.
  * @param[in] packetId The packet ID of the unsubscribe packet.
  * @param[in] remainingLength The remaining length of the unsubscribe packet.
  *
@@ -1841,7 +1842,7 @@ static MQTTStatus_t sendSubscribeWithoutCopy( MQTTContext_t * pContext,
                                                   &totalPacketLength );
 
             /* Lastly, the QoS gets sent. */
-            pIterator->iov_base = &( pSubscriptionList[ subscriptionsSent ].qos);
+            pIterator->iov_base = &( pSubscriptionList[ subscriptionsSent ].qos );
             pIterator->iov_len = 1U;
 
             /* Two slots get used by the topic string length and topic string. And

source/include/core_mqtt.h

@@ -58,13 +58,19 @@
 #define MQTT_LIBRARY_VERSION    "v1.2.0"
 /** @endcond */
 
+/**
+ * @ingroup mqtt_constants
+ * @brief Maximum number of vectors in subscribe and unsubscribe packet.
+ */
+#define MQTT_SUB_UNSUB_MAX_VECTORS    ( 4U )
+
 /**
  * @ingroup mqtt_constants
  * @brief Invalid packet identifier.
  *
  * Zero is an invalid packet identifier as per MQTT v3.1.1 spec.
  */
-#define MQTT_PACKET_ID_INVALID    ( ( uint16_t ) 0U )
+#define MQTT_PACKET_ID_INVALID        ( ( uint16_t ) 0U )
 
 /* Structures defined in this file. */
 struct MQTTPubAckInfo;

test/cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c

@@ -37,8 +37,12 @@ void harness()
     pContext = allocateMqttContext( NULL );
     __CPROVER_assume( isValidMqttContext( pContext ) );
 
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
     pSubscriptionList = allocateMqttSubscriptionList( NULL, 1U );
     __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, 1U ) );
 
-    MQTT_Subscribe( pContext, pSubscriptionList, packetId );
+    MQTT_Subscribe( pContext, pSubscriptionList, subscriptionCount, packetId );
 }

test/cbmc/proofs/MQTT_Subscribe/Makefile

@@ -45,14 +45,15 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendBuffer.0:$(MAX_NETWORK_SEND_TRIES)
 UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX)
 UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX)
-UNWINDSET += MQTT_SerializeSubscribe.0:$(SUBSCRIPTION_COUNT_MAX)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.0:${SUBSCRIBE_PACKET_VECTORS}
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.1:${SUBSCRIBE_PACKET_VECTORS}
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.2:${SUBSCRIBE_PACKET_VECTORS}
 # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength()
 # divides a size_t variable by 128 until it reaches zero to stop the loop.
 # log128(SIZE_MAX) = 4.571...
 UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_encodeRemainingLength.0:5
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendSubscribeWithoutCopy.0:$(MAX_NETWORK_SEND_TRIES)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendSubscribeWithoutCopy.1:$(MAX_NETWORK_SEND_TRIES)
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c

test/cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c

@@ -37,8 +37,12 @@ void harness()
     pContext = allocateMqttContext( NULL );
     __CPROVER_assume( isValidMqttContext( pContext ) );
 
+    /* Please see the default bound description on SUBSCRIPTION_COUNT_MAX in
+     * mqtt_cbmc_state.c for more information. */
+    __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX );
+
     pSubscriptionList = allocateMqttSubscriptionList( NULL, 1U );
     __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, 1U ) );
 
-    MQTT_Unsubscribe( pContext, pSubscriptionList, packetId );
+    MQTT_Unsubscribe( pContext, pSubscriptionList, subscriptionCount, packetId );
 }

test/cbmc/proofs/MQTT_Unsubscribe/Makefile

@@ -53,6 +53,8 @@ UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendMessageVector.2:${UNSUBSCRIBE_
 # divides a size_t variable by 128 until it reaches zero to stop the loop.
 # log128(SIZE_MAX) = 4.571...
 UNWINDSET += __CPROVER_file_local_core_mqtt_serializer_c_encodeRemainingLength.0:5
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendUnsubscribeWithoutCopy.0:$(MAX_NETWORK_SEND_TRIES)
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendUnsubscribeWithoutCopy.1:$(MAX_NETWORK_SEND_TRIES)
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c