From 5ec1c2fa4782f64925bf3dc184b2cb856849bcd4 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 03:05:30 +0000
Subject: [PATCH 01/29] Fix issue of data recv being interrupted

---
 source/core_mqtt.c | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 90f629142..276c16856 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -719,8 +719,11 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             totalBytesRecvd = bytesRecvd;
             receiveError = true;
         }
-        else
+        else if( bytesRecvd > 0 )
         {
+            /* Reset the elapsed time as we have not received all bytes from the network. */
+            entryTimeMs = getTimeStampMs();
+
             /* It is a bug in the application's transport receive implementation
              * if more bytes than expected are received. To avoid a possible
              * overflow in converting bytesRemaining from unsigned to signed,
@@ -737,13 +740,16 @@ static int32_t recvExact( const MQTTContext_t * pContext,
                         ( unsigned long ) bytesRemaining,
                         ( long int ) totalBytesRecvd ) );
         }
-
-        elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
-
-        if( ( bytesRemaining > 0U ) && ( elapsedTimeMs >= timeoutMs ) )
+        else
         {
-            LogError( ( "Time expired while receiving packet." ) );
-            receiveError = true;
+            /* No bytes were read from the network. */
+            elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
+
+            if( ( bytesRemaining > 0U ) && ( elapsedTimeMs >= timeoutMs ) )
+            {
+                LogError( ( "Time expired while receiving packet." ) );
+                receiveError = true;
+            }
         }
     }
 

From 4205109ee305f3ad487f04bc2a2e42905b773a00 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 03:08:04 +0000
Subject: [PATCH 02/29] Rename elapsedTimeMs variable to its express its new
 meaning

---
 source/core_mqtt.c | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 276c16856..ca1c440f2 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -689,7 +689,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
     int32_t totalBytesRecvd = 0, bytesRecvd;
-    uint32_t entryTimeMs = 0U, elapsedTimeMs = 0U;
+    uint32_t entryTimeMs = 0U, noDataRecvdTimeMs = 0U;
     TransportRecv_t recvFunc = NULL;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
@@ -721,7 +721,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         }
         else if( bytesRecvd > 0 )
         {
-            /* Reset the elapsed time as we have not received all bytes from the network. */
+            /* Reset the starting time as we have received some data from the network. */
             entryTimeMs = getTimeStampMs();
 
             /* It is a bug in the application's transport receive implementation
@@ -743,9 +743,9 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
+            noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
 
-            if( ( bytesRemaining > 0U ) && ( elapsedTimeMs >= timeoutMs ) )
+            if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= timeoutMs ) )
             {
                 LogError( ( "Time expired while receiving packet." ) );
                 receiveError = true;

From 0704c72f51631a431d2ba91bebc3afcf54d8d6e1 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 04:07:28 +0000
Subject: [PATCH 03/29] Use configuration const for recvExact timeout

---
 source/core_mqtt.c                         | 25 ++++++++++++++--------
 source/include/core_mqtt_config_defaults.h | 21 ++++++++++++++++++
 2 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index ca1c440f2..5df3782ff 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -71,17 +71,25 @@ static uint32_t calculateElapsedTime( uint32_t later,
 static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType );
 
 /**
- * @brief Receive bytes into the network buffer, with a timeout.
+ * @brief Receive bytes into the network buffer.
  *
  * @param[in] pContext Initialized MQTT Context.
  * @param[in] bytesToRecv Number of bytes to receive.
- * @param[in] timeoutMs Time remaining to receive the packet.
+ *
+ * @note This operation calls the transport receive function
+ * repeatedly to read bytes from the network until either:
+ * 1. The requested number of bytes @a bytesToRecv are read.
+ *                    OR
+ * 2. There is a timeout of MQTT_PACKET_RECV_TIMEOUT_MS duration
+ * between receiving bytes over the network.
+ *                    OR
+ * 3. There is an error in reading from the network.
+ *
  *
  * @return Number of bytes received, or negative number on network error.
  */
 static int32_t recvExact( const MQTTContext_t * pContext,
-                          size_t bytesToRecv,
-                          uint32_t timeoutMs );
+                          size_t bytesToRecv );
 
 /**
  * @brief Discard a packet from the transport interface.
@@ -683,8 +691,7 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType )
 /*-----------------------------------------------------------*/
 
 static int32_t recvExact( const MQTTContext_t * pContext,
-                          size_t bytesToRecv,
-                          uint32_t timeoutMs )
+                          size_t bytesToRecv )
 {
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
@@ -745,7 +752,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             /* No bytes were read from the network. */
             noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
 
-            if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= timeoutMs ) )
+            if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_PACKET_RECV_TIMEOUT_MS ) )
             {
                 LogError( ( "Time expired while receiving packet." ) );
                 receiveError = true;
@@ -785,7 +792,7 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
             bytesToReceive = remainingLength - totalBytesReceived;
         }
 
-        bytesReceived = recvExact( pContext, bytesToReceive, remainingTimeMs );
+        bytesReceived = recvExact( pContext, bytesToReceive );
 
         if( bytesReceived != ( int32_t ) bytesToReceive )
         {
@@ -852,7 +859,7 @@ static MQTTStatus_t receivePacket( const MQTTContext_t * pContext,
     else
     {
         bytesToReceive = incomingPacket.remainingLength;
-        bytesReceived = recvExact( pContext, bytesToReceive, remainingTimeMs );
+        bytesReceived = recvExact( pContext, bytesToReceive );
 
         if( bytesReceived == ( int32_t ) bytesToReceive )
         {
diff --git a/source/include/core_mqtt_config_defaults.h b/source/include/core_mqtt_config_defaults.h
index 5b7c26c25..931a1dd20 100644
--- a/source/include/core_mqtt_config_defaults.h
+++ b/source/include/core_mqtt_config_defaults.h
@@ -108,6 +108,27 @@
     #define MQTT_PINGRESP_TIMEOUT_MS    ( 500U )
 #endif
 
+/**
+ * @brief The timeout for receiving data over network for an incoming MQTT
+ * packet by the #MQTT_ProcessLoop or #MQTT_ReceiveLoop API functions.
+ *
+ * When an incoming MQTT packet is detected, the transport receive function
+ * may be called multiple times until all the expected number of bytes for the packet
+ * is received.
+ * This timeout represents the maximum duration to wait for data to be received
+ * between consecutive reception of bytes over the network in that scenario.
+ * If the timeout expires, the #MQTTProcessLoop or #MQTT_ReceiveLoop functions
+ * return #MQTTRecvFailed.
+ *
+ * <b>Possible values:</b> Any positive integer up to SIZE_MAX. Recommended to
+ * use a small timeout value. <br>
+ * <b>Default value:</b> `10`
+ *
+ */
+#ifndef MQTT_PACKET_RECV_TIMEOUT_MS
+    #define MQTT_PACKET_RECV_TIMEOUT_MS    ( 10U )
+#endif
+
 /**
  * @brief Macro that is called in the MQTT library for logging "Error" level
  * messages.

From adce7668e497dc358d92e08ab37434bf33ce395b Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 04:31:13 +0000
Subject: [PATCH 04/29] Remove timeout check from discardPacket and address CI
 check failures

---
 source/core_mqtt.c | 23 +++++------------------
 1 file changed, 5 insertions(+), 18 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 5df3782ff..54fc85feb 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -751,12 +751,12 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         {
             /* No bytes were read from the network. */
             noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
+        }
 
-            if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_PACKET_RECV_TIMEOUT_MS ) )
-            {
-                LogError( ( "Time expired while receiving packet." ) );
-                receiveError = true;
-            }
+        if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_PACKET_RECV_TIMEOUT_MS ) )
+        {
+            LogError( ( "Time expired while receiving packet." ) );
+            receiveError = true;
         }
     }
 
@@ -805,19 +805,6 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
         else
         {
             totalBytesReceived += ( uint32_t ) bytesReceived;
-
-            elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
-
-            /* Update remaining time and check for timeout. */
-            if( elapsedTimeMs < timeoutMs )
-            {
-                remainingTimeMs = timeoutMs - elapsedTimeMs;
-            }
-            else
-            {
-                LogError( ( "Time expired while discarding packet." ) );
-                receiveError = true;
-            }
         }
     }
 

From f5aa1b36fba3a002ccf1ff1881b7016767f35291 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 04:35:02 +0000
Subject: [PATCH 05/29] Fix more CI check failures

---
 source/core_mqtt.c                         | 5 +----
 source/include/core_mqtt_config_defaults.h | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 54fc85feb..e34766bba 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -772,8 +772,7 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
     MQTTStatus_t status = MQTTRecvFailed;
     int32_t bytesReceived = 0;
     size_t bytesToReceive = 0U;
-    uint32_t totalBytesReceived = 0U, entryTimeMs = 0U, elapsedTimeMs = 0U;
-    uint32_t remainingTimeMs = timeoutMs;
+    uint32_t totalBytesReceived = 0U;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
 
@@ -783,8 +782,6 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
     bytesToReceive = pContext->networkBuffer.size;
     getTimeStampMs = pContext->getTime;
 
-    entryTimeMs = getTimeStampMs();
-
     while( ( totalBytesReceived < remainingLength ) && ( receiveError == false ) )
     {
         if( ( remainingLength - totalBytesReceived ) < bytesToReceive )
diff --git a/source/include/core_mqtt_config_defaults.h b/source/include/core_mqtt_config_defaults.h
index 931a1dd20..f2307d2fc 100644
--- a/source/include/core_mqtt_config_defaults.h
+++ b/source/include/core_mqtt_config_defaults.h
@@ -117,7 +117,7 @@
  * is received.
  * This timeout represents the maximum duration to wait for data to be received
  * between consecutive reception of bytes over the network in that scenario.
- * If the timeout expires, the #MQTTProcessLoop or #MQTT_ReceiveLoop functions
+ * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
  *
  * <b>Possible values:</b> Any positive integer up to SIZE_MAX. Recommended to

From 76166d01556911694cda16fbd6064027078cdb7c Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 06:41:47 +0000
Subject: [PATCH 06/29] Remove another unused local variable

---
 source/core_mqtt.c | 2 --
 1 file changed, 2 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index e34766bba..703b8f819 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -773,14 +773,12 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
     int32_t bytesReceived = 0;
     size_t bytesToReceive = 0U;
     uint32_t totalBytesReceived = 0U;
-    MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
 
     assert( pContext != NULL );
     assert( pContext->getTime != NULL );
 
     bytesToReceive = pContext->networkBuffer.size;
-    getTimeStampMs = pContext->getTime;
 
     while( ( totalBytesReceived < remainingLength ) && ( receiveError == false ) )
     {

From 1d73bb7ec2c02cbc5dc3e3b6a64e54a09643c147 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 07:16:17 +0000
Subject: [PATCH 07/29] Re-instate timeout in discard to reduce scope of
 changes

---
 source/core_mqtt.c | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 703b8f819..76a228b2a 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -772,13 +772,18 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
     MQTTStatus_t status = MQTTRecvFailed;
     int32_t bytesReceived = 0;
     size_t bytesToReceive = 0U;
-    uint32_t totalBytesReceived = 0U;
+    uint32_t totalBytesReceived = 0U, entryTimeMs = 0U, elapsedTimeMs = 0U;
+    uint32_t remainingTimeMs = timeoutMs;
+    MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
 
     assert( pContext != NULL );
     assert( pContext->getTime != NULL );
 
     bytesToReceive = pContext->networkBuffer.size;
+    getTimeStampMs = pContext->getTime;
+
+    entryTimeMs = getTimeStampMs();
 
     while( ( totalBytesReceived < remainingLength ) && ( receiveError == false ) )
     {
@@ -800,6 +805,15 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
         else
         {
             totalBytesReceived += ( uint32_t ) bytesReceived;
+
+            elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
+
+            /* Update remaining time and check for timeout. */
+            if( elapsedTimeMs >= timeoutMs )
+            {
+                LogError( ( "Time expired while discarding packet." ) );
+                receiveError = true;
+            }
         }
     }
 

From 0c5a9e3bd3af850f0fab8cb1634ba1f616e19b4a Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 07:18:31 +0000
Subject: [PATCH 08/29] Remove unused variable again

---
 source/core_mqtt.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 76a228b2a..b9920ff8f 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -773,7 +773,6 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
     int32_t bytesReceived = 0;
     size_t bytesToReceive = 0U;
     uint32_t totalBytesReceived = 0U, entryTimeMs = 0U, elapsedTimeMs = 0U;
-    uint32_t remainingTimeMs = timeoutMs;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
 

From 34adc86e091ff294457698a30a6bd3635fcbb972 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 07:52:21 +0000
Subject: [PATCH 09/29] Fix failing unit test

---
 test/unit-test/core_mqtt_utest.c | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/test/unit-test/core_mqtt_utest.c b/test/unit-test/core_mqtt_utest.c
index cf8fd922d..42c5bdbcc 100644
--- a/test/unit-test/core_mqtt_utest.c
+++ b/test/unit-test/core_mqtt_utest.c
@@ -365,6 +365,20 @@ static int32_t transportRecvOneByte( NetworkContext_t * pNetworkContext,
     return 1;
 }
 
+/**
+ * @brief Mocked transport returning zero bytes to simulate reception
+ * of no data over network.
+ */
+static int32_t transportRecvNoData( NetworkContext_t * pNetworkContext,
+                                    void * pBuffer,
+                                    size_t bytesToRead )
+{
+    ( void ) pNetworkContext;
+    ( void ) pBuffer;
+    ( void ) bytesToRead;
+    return 0;
+}
+
 /**
  * @brief Initialize the transport interface with the mocked functions for
  * send and receive.
@@ -853,7 +867,7 @@ void test_MQTT_Connect_partial_receive()
 
     setupTransportInterface( &transport );
     setupNetworkBuffer( &networkBuffer );
-    transport.recv = transportRecvOneByte;
+    transport.recv = transportRecvNoData;
 
     memset( &mqttContext, 0x0, sizeof( mqttContext ) );
     MQTT_Init( &mqttContext, &transport, getTime, eventCallback, &networkBuffer );
@@ -864,14 +878,16 @@ void test_MQTT_Connect_partial_receive()
     incomingPacket.type = MQTT_PACKET_TYPE_CONNACK;
     incomingPacket.remainingLength = 2;
 
-    /* Not enough time to receive entire packet, for branch coverage. This is due
-     * to the fact the mocked receive function reads only one byte at a time. */
-    timeout = 1;
+    /* Timeout in receiving entire packet, for branch coverage. This is due to the fact that the mocked
+     * receive function always returns 0 bytes read. */
     MQTT_GetIncomingPacketTypeAndLength_ExpectAnyArgsAndReturn( MQTTSuccess );
     MQTT_GetIncomingPacketTypeAndLength_ReturnThruPtr_pIncomingPacket( &incomingPacket );
     status = MQTT_Connect( &mqttContext, &connectInfo, NULL, timeout, &sessionPresent );
     TEST_ASSERT_EQUAL_INT( MQTTRecvFailed, status );
 
+    /* Update to use mock receive function that receives one byte at a time for the
+     * rest of the test. */
+    mqttContext.transportInterface.recv = transportRecvOneByte;
     timeout = 10;
 
     /* Not enough space for packet, discard it. */

From 2a3cc9ab5f16db2191dc40d75b8402143d1e2f6d Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 08:25:11 +0000
Subject: [PATCH 10/29] Rename new config macro, and attempt to fix CBMC
 failures

---
 source/core_mqtt.c                         |  4 ++--
 source/include/core_mqtt_config_defaults.h | 16 ++++++++--------
 test/cbmc/include/core_mqtt_config.h       | 14 ++++++++++++++
 3 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index b9920ff8f..f5e898eab 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -80,7 +80,7 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType );
  * repeatedly to read bytes from the network until either:
  * 1. The requested number of bytes @a bytesToRecv are read.
  *                    OR
- * 2. There is a timeout of MQTT_PACKET_RECV_TIMEOUT_MS duration
+ * 2. There is a timeout of MQTT_RECV_POLLING_TIMEOUT_MS duration
  * between receiving bytes over the network.
  *                    OR
  * 3. There is an error in reading from the network.
@@ -753,7 +753,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
         }
 
-        if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_PACKET_RECV_TIMEOUT_MS ) )
+        if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
         {
             LogError( ( "Time expired while receiving packet." ) );
             receiveError = true;
diff --git a/source/include/core_mqtt_config_defaults.h b/source/include/core_mqtt_config_defaults.h
index f2307d2fc..0844b0a3c 100644
--- a/source/include/core_mqtt_config_defaults.h
+++ b/source/include/core_mqtt_config_defaults.h
@@ -109,14 +109,14 @@
 #endif
 
 /**
- * @brief The timeout for receiving data over network for an incoming MQTT
- * packet by the #MQTT_ProcessLoop or #MQTT_ReceiveLoop API functions.
+ * @brief The maximum duration of receiving no data over network when
+ * attempting to read an incoming MQTT packet by the #MQTT_ProcessLoop or
+ * #MQTT_ReceiveLoop API functions.
  *
  * When an incoming MQTT packet is detected, the transport receive function
- * may be called multiple times until all the expected number of bytes for the packet
- * is received.
- * This timeout represents the maximum duration to wait for data to be received
- * between consecutive reception of bytes over the network in that scenario.
+ * may be called multiple times until all the expected number of bytes for the
+ * packet are received. This timeout represents the maximum duration of polling
+ * for any data to be received over the network for the incoming.
  * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
  *
@@ -125,8 +125,8 @@
  * <b>Default value:</b> `10`
  *
  */
-#ifndef MQTT_PACKET_RECV_TIMEOUT_MS
-    #define MQTT_PACKET_RECV_TIMEOUT_MS    ( 10U )
+#ifndef MQTT_RECV_POLLING_TIMEOUT_MS
+    #define MQTT_RECV_POLLING_TIMEOUT_MS    ( 10U )
 #endif
 
 /**
diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index c8bb21699..1898a05b3 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -70,4 +70,18 @@ struct NetworkContext
  */
 #define MQTT_PINGRESP_TIMEOUT_MS                ( 500U )
 
+/**
+ * @brief The maximum duration of receiving no data over network when
+ * attempting to read an incoming MQTT packet by the #MQTT_ProcessLoop or
+ * #MQTT_ReceiveLoop API functions.
+ *
+ * When an incoming MQTT packet is detected, the transport receive function
+ * may be called multiple times until all the expected number of bytes for the
+ * packet are received. This timeout represents the maximum duration of polling
+ * for any data to be received over the network for the incoming.
+ * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
+ * return #MQTTRecvFailed.
+ */
+#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 3U )
+
 #endif /* ifndef CORE_MQTT_CONFIG_H_ */

From 70b181a1359c9f9d11cdfda3492340a93712ea5d Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 11:14:11 -0800
Subject: [PATCH 11/29] Doc: Improvement suggestions from code review

Co-authored-by: Muneeb Ahmed <54290492+muneebahmed10@users.noreply.github.com>
---
 source/core_mqtt.c                         | 12 ++++++------
 source/include/core_mqtt_config_defaults.h | 14 +++++++-------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index f5e898eab..2ac9254c1 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -80,8 +80,8 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType );
  * repeatedly to read bytes from the network until either:
  * 1. The requested number of bytes @a bytesToRecv are read.
  *                    OR
- * 2. There is a timeout of MQTT_RECV_POLLING_TIMEOUT_MS duration
- * between receiving bytes over the network.
+ * 2. No data is received from the network for MQTT_RECV_POLLING_TIMEOUT_MS duration.
+ * 
  *                    OR
  * 3. There is an error in reading from the network.
  *
@@ -696,7 +696,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
     int32_t totalBytesRecvd = 0, bytesRecvd;
-    uint32_t entryTimeMs = 0U, noDataRecvdTimeMs = 0U;
+    uint32_t lastDataRecvTimeMs = 0U, noDataRecvdTimeMs = 0U;
     TransportRecv_t recvFunc = NULL;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
@@ -729,7 +729,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else if( bytesRecvd > 0 )
         {
             /* Reset the starting time as we have received some data from the network. */
-            entryTimeMs = getTimeStampMs();
+            lastDataRecvTimeMs = getTimeStampMs();
 
             /* It is a bug in the application's transport receive implementation
              * if more bytes than expected are received. To avoid a possible
@@ -750,7 +750,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
+            noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
         if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
@@ -807,7 +807,7 @@ static MQTTStatus_t discardPacket( const MQTTContext_t * pContext,
 
             elapsedTimeMs = calculateElapsedTime( getTimeStampMs(), entryTimeMs );
 
-            /* Update remaining time and check for timeout. */
+            /* Check for timeout. */
             if( elapsedTimeMs >= timeoutMs )
             {
                 LogError( ( "Time expired while discarding packet." ) );
diff --git a/source/include/core_mqtt_config_defaults.h b/source/include/core_mqtt_config_defaults.h
index 0844b0a3c..019c3ac71 100644
--- a/source/include/core_mqtt_config_defaults.h
+++ b/source/include/core_mqtt_config_defaults.h
@@ -109,15 +109,15 @@
 #endif
 
 /**
- * @brief The maximum duration of receiving no data over network when
- * attempting to read an incoming MQTT packet by the #MQTT_ProcessLoop or
- * #MQTT_ReceiveLoop API functions.
+ * @brief The maximum duration between non-empty network reads while
+ * receiving an MQTT packet via the #MQTT_ProcessLoop or #MQTT_ReceiveLoop
+ * API functions.
  *
  * When an incoming MQTT packet is detected, the transport receive function
- * may be called multiple times until all the expected number of bytes for the
- * packet are received. This timeout represents the maximum duration of polling
- * for any data to be received over the network for the incoming.
- * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
+ * may be called multiple times until all of the expected number of bytes of the
+ * packet are received. This timeout represents the maximum polling duration that
+ * is allowed without any data reception from the network for the incoming packet.
+ * If the timeout expires, the #MQTT_ProcessLoop and #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
  *
  * <b>Possible values:</b> Any positive integer up to SIZE_MAX. Recommended to

From 68fcb16568ace15c41faf2a3bc347028b44b93ff Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 20:09:08 +0000
Subject: [PATCH 12/29] Fix quality check failures

---
 source/core_mqtt.c | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 2ac9254c1..2e27955fc 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -81,7 +81,7 @@ static MQTTPubAckType_t getAckFromPacketType( uint8_t packetType );
  * 1. The requested number of bytes @a bytesToRecv are read.
  *                    OR
  * 2. No data is received from the network for MQTT_RECV_POLLING_TIMEOUT_MS duration.
- * 
+ *
  *                    OR
  * 3. There is an error in reading from the network.
  *
@@ -711,7 +711,8 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     recvFunc = pContext->transportInterface.recv;
     getTimeStampMs = pContext->getTime;
 
-    entryTimeMs = getTimeStampMs();
+    /* Part of the MQTT packet has been read before calling this function. */
+    lastDataRecvTimeMs = getTimeStampMs();
 
     while( ( bytesRemaining > 0U ) && ( receiveError == false ) )
     {

From 4ba8c53f522144e46c20eb8c8dacc81ea0b2763f Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 22:39:37 +0000
Subject: [PATCH 13/29] Add test case to check partial network reads with zero
 timeout duration for ProcessLoop

---
 test/unit-test/core_mqtt_utest.c | 51 +++++++++++++++++++++++++++++++-
 1 file changed, 50 insertions(+), 1 deletion(-)

diff --git a/test/unit-test/core_mqtt_utest.c b/test/unit-test/core_mqtt_utest.c
index 42c5bdbcc..64b5e1171 100644
--- a/test/unit-test/core_mqtt_utest.c
+++ b/test/unit-test/core_mqtt_utest.c
@@ -132,6 +132,7 @@ typedef struct ProcessLoopReturns
     MQTTStatus_t processLoopStatus;           /**< @brief Return value of the process loop. */
     bool incomingPublish;                     /**< @brief Whether the incoming packet is a publish. */
     MQTTPublishInfo_t * pPubInfo;             /**< @brief Publish information to be returned by the deserializer. */
+    uint32_t timeoutMs;                       /**< @brief The timeout value to call MQTT_ProcessLoop API with. */
 } ProcessLoopReturns_t;
 
 /**
@@ -419,6 +420,7 @@ static void resetProcessLoopParams( ProcessLoopReturns_t * pExpectParams )
     pExpectParams->processLoopStatus = MQTTSuccess;
     pExpectParams->incomingPublish = false;
     pExpectParams->pPubInfo = NULL;
+    pExpectParams->timeoutMs = MQTT_NO_TIMEOUT_MS;
 }
 
 /**
@@ -562,7 +564,7 @@ static void expectProcessLoopCalls( MQTTContext_t * const pContext,
     }
 
     /* Expect the above calls when running MQTT_ProcessLoop. */
-    mqttStatus = MQTT_ProcessLoop( pContext, MQTT_NO_TIMEOUT_MS );
+    mqttStatus = MQTT_ProcessLoop( pContext, pExpectParams->timeoutMs );
     TEST_ASSERT_EQUAL( processLoopStatus, mqttStatus );
 
     /* Any final assertions to end the test. */
@@ -1589,6 +1591,53 @@ void test_MQTT_ProcessLoop_handleIncomingPublish_Error_Paths( void )
     TEST_ASSERT_FALSE( isEventCallbackInvoked );
 }
 
+/**
+ * @brief This test checks that the ProcessLoop API function is able to
+ * support receiving an entire incoming MQTT packet over the network when
+ * the transport recv function only reads less than requested bytes at a
+ * time, and the timeout passed to the API is "0ms".
+ */
+void test_MQTT_ProcessLoop_Zero_Duration_And_Slow_Network_Read( void )
+{
+    MQTTStatus_t mqttStatus;
+    MQTTContext_t context;
+    TransportInterface_t transport;
+    MQTTFixedBuffer_t networkBuffer;
+    ProcessLoopReturns_t expectParams = { 0 };
+
+    setupNetworkBuffer( &networkBuffer );
+
+    transport.send = transportSendSuccess;
+
+    /* Set the transport recv function for the test to the mock function that represents
+     * partial read of data from network (i.e. less than requested number of bytes)
+     * at a time. */
+    transport.recv = transportRecvOneByte;
+
+    /* Initialize the context. */
+    mqttStatus = MQTT_Init( &context, &transport, getTime, eventCallback, &networkBuffer );
+    TEST_ASSERT_EQUAL( MQTTSuccess, mqttStatus );
+
+    /* Set flag required for configuring behavior of expectProcessLoopCalls()
+     * helper function. */
+    modifyIncomingPacketStatus = MQTTSuccess;
+
+    /* Test the ProcessLoop() call with zero duration timeout to verify that it
+     * will be able to support reading the packet over network over multiple calls to
+     * the transport receive function. */
+    expectParams.timeoutMs = MQTT_NO_TIMEOUT_MS;
+
+    /* Test with an incoming PUBLISH packet whose payload is read only one byte
+     * per call to the transport recv function. */
+    currentPacketType = MQTT_PACKET_TYPE_PUBLISH;
+    /* Set expected return values during the loop. */
+    resetProcessLoopParams( &expectParams );
+    expectParams.stateAfterDeserialize = MQTTPubAckSend;
+    expectParams.stateAfterSerialize = MQTTPublishDone;
+    expectParams.incomingPublish = true;
+    expectProcessLoopCalls( &context, &expectParams );
+}
+
 /**
  * @brief This test case covers all calls to the private method,
  * handleIncomingAck(...),

From b7107904d0c36cf402c95c1d8574f9400426d3b0 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 22:46:09 +0000
Subject: [PATCH 14/29] style: Improving naming

---
 source/core_mqtt.c               | 8 +++++---
 test/unit-test/core_mqtt_utest.c | 2 +-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 2e27955fc..ffc0bb291 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -696,7 +696,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
     int32_t totalBytesRecvd = 0, bytesRecvd;
-    uint32_t lastDataRecvTimeMs = 0U, noDataRecvdTimeMs = 0U;
+    uint32_t lastDataRecvTimeMs = 0U, timeSinceLastDataWasRecvdMs = 0U;
     TransportRecv_t recvFunc = NULL;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
@@ -751,10 +751,12 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            noDataRecvdTimeMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
+            timeSinceLastDataWasRecvdMs =
+                calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
-        if( ( bytesRemaining > 0U ) && ( noDataRecvdTimeMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
+        if( ( bytesRemaining > 0U ) &&
+            ( timeSinceLastDataWasRecvdMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
         {
             LogError( ( "Time expired while receiving packet." ) );
             receiveError = true;
diff --git a/test/unit-test/core_mqtt_utest.c b/test/unit-test/core_mqtt_utest.c
index 64b5e1171..fb96fd6ca 100644
--- a/test/unit-test/core_mqtt_utest.c
+++ b/test/unit-test/core_mqtt_utest.c
@@ -1597,7 +1597,7 @@ void test_MQTT_ProcessLoop_handleIncomingPublish_Error_Paths( void )
  * the transport recv function only reads less than requested bytes at a
  * time, and the timeout passed to the API is "0ms".
  */
-void test_MQTT_ProcessLoop_Zero_Duration_And_Slow_Network_Read( void )
+void test_MQTT_ProcessLoop_Zero_Duration_And_Partial_Network_Read( void )
 {
     MQTTStatus_t mqttStatus;
     MQTTContext_t context;

From f8586dce9eea98ba6d764a38832206852da917da Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Thu, 3 Dec 2020 22:57:16 +0000
Subject: [PATCH 15/29] Address complexity failure

---
 source/core_mqtt.c | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index ffc0bb291..756c2c9d4 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -751,8 +751,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            timeSinceLastDataWasRecvdMs =
-                calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
+            timeSinceLastDataWasRecvdMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
         if( ( bytesRemaining > 0U ) &&

From c59d39b3079a360948d14eab944c5694c5f2f1dd Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 00:44:21 +0000
Subject: [PATCH 16/29] Address comments

---
 docs/doxygen/pages.dox               | 3 +++
 test/cbmc/include/core_mqtt_config.h | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/docs/doxygen/pages.dox b/docs/doxygen/pages.dox
index 18b8cb235..5b2da625b 100644
--- a/docs/doxygen/pages.dox
+++ b/docs/doxygen/pages.dox
@@ -188,6 +188,9 @@ Some configuration settings are C pre-processor constants, and some are function
 @section MQTT_PINGRESP_TIMEOUT_MS
 @copydoc MQTT_PINGRESP_TIMEOUT_MS
 
+@section MQTT_RECV_POLLING_TIMEOUT_MS
+@copydoc MQTT_RECV_POLLING_TIMEOUT_MS
+
 @section MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT
 @copydoc MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT
 
diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index 1898a05b3..703c7a72e 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -82,6 +82,6 @@ struct NetworkContext
  * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
  */
-#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 3U )
+#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 2U )
 
 #endif /* ifndef CORE_MQTT_CONFIG_H_ */

From af1ca026a1cf31243a64ba9dbdf7f8dbcd8ab263 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 03:11:08 +0000
Subject: [PATCH 17/29] Doc: Add blocking time equation of Receive/ProcessLoop
 functions in their API doc

---
 source/include/core_mqtt.h | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h
index 7452d665d..7aff77e46 100644
--- a/source/include/core_mqtt.h
+++ b/source/include/core_mqtt.h
@@ -603,6 +603,13 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext );
  * @param[in] timeoutMs Minimum time in milliseconds that the receive loop will
  * run, unless an error occurs.
  *
+ * @note Calling this function blocks the calling context for a time period that
+ * depends on the passed @p timeoutMs, the configured macro, #MQTT_RECV_POLLING_TIMEOUT_MS
+ * and the underlying transport interface implementation timeouts.
+ *    Blocking Time = Max( timeoutMs parameter,
+ *                         MQTT_RECV_POLLING_TIMEOUT_MS,
+ *                         Transport interface send/recv implementation timeout )
+ *
  * @return #MQTTBadParameter if context is NULL;
  * #MQTTRecvFailed if a network error occurs during reception;
  * #MQTTSendFailed if a network error occurs while sending an ACK or PINGREQ;
@@ -655,6 +662,13 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext,
  * @param[in] timeoutMs Minimum time in milliseconds that the receive loop will
  * run, unless an error occurs.
  *
+ * @note Calling this function blocks the calling context for a time period that
+ * depends on the passed @p timeoutMs, the configured macro, #MQTT_RECV_POLLING_TIMEOUT_MS
+ * and the underlying transport interface implementation timeouts.
+ *    Blocking Time = Max( timeoutMs parameter,
+ *                         MQTT_RECV_POLLING_TIMEOUT_MS,
+ *                         Transport interface send/recv implementation timeout )
+ *
  * @return #MQTTBadParameter if context is NULL;
  * #MQTTRecvFailed if a network error occurs during reception;
  * #MQTTSendFailed if a network error occurs while sending an ACK or PINGREQ;

From 86798bf7cee28aa5cc22dc251b8fe5d4712d16dd Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 03:17:32 +0000
Subject: [PATCH 18/29] Improvement in API doc

---
 source/include/core_mqtt.h | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h
index 7aff77e46..fadfbe537 100644
--- a/source/include/core_mqtt.h
+++ b/source/include/core_mqtt.h
@@ -604,8 +604,9 @@ MQTTStatus_t MQTT_Disconnect( MQTTContext_t * pContext );
  * run, unless an error occurs.
  *
  * @note Calling this function blocks the calling context for a time period that
- * depends on the passed @p timeoutMs, the configured macro, #MQTT_RECV_POLLING_TIMEOUT_MS
- * and the underlying transport interface implementation timeouts.
+ * depends on the passed @p timeoutMs, the configuration macro, #MQTT_RECV_POLLING_TIMEOUT_MS,
+ * and the underlying transport interface implementation timeouts, unless an error
+ * occurs.
  *    Blocking Time = Max( timeoutMs parameter,
  *                         MQTT_RECV_POLLING_TIMEOUT_MS,
  *                         Transport interface send/recv implementation timeout )
@@ -663,8 +664,9 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext,
  * run, unless an error occurs.
  *
  * @note Calling this function blocks the calling context for a time period that
- * depends on the passed @p timeoutMs, the configured macro, #MQTT_RECV_POLLING_TIMEOUT_MS
- * and the underlying transport interface implementation timeouts.
+ * depends on the passed @p timeoutMs, the configuration macro, #MQTT_RECV_POLLING_TIMEOUT_MS,
+ * and the underlying transport interface implementation timeouts, unless an error
+ * occurs.
  *    Blocking Time = Max( timeoutMs parameter,
  *                         MQTT_RECV_POLLING_TIMEOUT_MS,
  *                         Transport interface send/recv implementation timeout )

From e1de841166d5624493a80a6a5b8a8acabaf61758 Mon Sep 17 00:00:00 2001
From: Sarena Meas <sarem@amazon.com>
Date: Thu, 3 Dec 2020 20:44:05 -0800
Subject: [PATCH 19/29] Set MQTT_RECV_POLLING_TIMEOUT_MS so that recvExact runs
 in one iteration always for cbmc.

---
 lexicon.txt                                | 1 +
 test/cbmc/include/core_mqtt_config.h       | 6 +++++-
 test/cbmc/proofs/MQTT_Connect/Makefile     | 7 +++++--
 test/cbmc/proofs/MQTT_ProcessLoop/Makefile | 5 ++++-
 test/cbmc/proofs/MQTT_ReceiveLoop/Makefile | 5 ++++-
 5 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index 7a9ad274d..a0f7d0b31 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -279,6 +279,7 @@ receivepacket
 recordcount
 recordindex
 recv
+recvexact
 recvfunc
 reestablishment
 remaininglength
diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index 703c7a72e..2c2f59f9a 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -81,7 +81,11 @@ struct NetworkContext
  * for any data to be received over the network for the incoming.
  * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
+ *
+ * For the sake of proving memory safety quickly this is set to zero. When this
+ * is set to zero, coverage of each condition in recvExact is reached before
+ * ultimately exiting after a single iteration.
  */
-#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 2U )
+#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 0U )
 
 #endif /* ifndef CORE_MQTT_CONFIG_H_ */
diff --git a/test/cbmc/proofs/MQTT_Connect/Makefile b/test/cbmc/proofs/MQTT_Connect/Makefile
index 5e1bc80b6..cb40c9aa2 100644
--- a/test/cbmc/proofs/MQTT_Connect/Makefile
+++ b/test/cbmc/proofs/MQTT_Connect/Makefile
@@ -54,10 +54,13 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_mqtt_c_handleKeepAlive
 # function.
 REMOVE_FUNCTION_BODY += memcpy
 
-# The loops below are unwound once more than the timeout. The loops below use
+# The loop below is unwound once more than the timeout. The loop below uses
 # the user passed in timeout to break the loop.
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
+# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
+# The possible values from the transport receive can attain coverage with a
+# single iteration.
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
 # If the user passed in timeout is zero, then the loop will run until the
 # MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT is reached.
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_receiveConnack.0:$(MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT)
diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
index d43e928f1..ad05352e4 100644
--- a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
+++ b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
@@ -46,7 +46,10 @@ REMOVE_FUNCTION_BODY += MQTT_SerializeAck
 
 UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_RECEIVE_TIMEOUT)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
+# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
+# The possible values from the transport receive can attain coverage with a
+# single iteration.
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
 # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
 # sendPacket will continue until all the bytes are sent or a network error
 # occurs. Please see NetworkInterfaceReceiveStub in
diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
index 4ae14c6af..b4227e452 100644
--- a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
+++ b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
@@ -28,7 +28,10 @@ REMOVE_FUNCTION_BODY += MQTT_SerializeAck
 # The loops below are unwound once more than the exclusive timeout bound.
 UNWINDSET += MQTT_ReceiveLoop.0:$(MQTT_RECEIVE_TIMEOUT)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT)
+# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
+# The possible values from the transport receive can attain coverage with a
+# single iteration.
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
 # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
 # sendPacket will continue until all the bytes are sent or a network error
 # occurs. Please see NetworkInterfaceReceiveStub in

From ebcfb92bcc9cfd8644389a077608d5b9d3f2a84b Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 18:27:15 +0000
Subject: [PATCH 20/29] doc: Add information about zero return value for
 Transport_Recv_t

---
 source/interface/transport_interface.h | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/source/interface/transport_interface.h b/source/interface/transport_interface.h
index c71991acf..000b280d1 100644
--- a/source/interface/transport_interface.h
+++ b/source/interface/transport_interface.h
@@ -163,7 +163,11 @@ typedef struct NetworkContext NetworkContext_t;
  * @param[in] pBuffer Buffer to receive the data into.
  * @param[in] bytesToRecv Number of bytes requested from the network.
  *
- * @return The number of bytes received or a negative error code.
+ * @return The number of bytes received or a negative value to indicate
+ * error.
+ * @note If no data is available on the network to read and no error
+ * has occurred, zero SHOULD be the return value. Zero should NOT be used
+ * if a network disconnection has occurred.
  */
 /* @[define_transportrecv] */
 typedef int32_t ( * TransportRecv_t )( NetworkContext_t * pNetworkContext,

From 32f029190780689881d7de7db6053a9b01e438ff Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 18:29:22 +0000
Subject: [PATCH 21/29] fix: prevent possibility of infinite loop in timeout
 logic of ProcessLoop

---
 source/core_mqtt.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 756c2c9d4..319f28eda 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -2177,7 +2177,7 @@ MQTTStatus_t MQTT_ProcessLoop( MQTTContext_t * pContext,
             elapsedTimeMs = calculateElapsedTime( pContext->getTime(),
                                                   entryTimeMs );
 
-            if( elapsedTimeMs > timeoutMs )
+            if( elapsedTimeMs >= timeoutMs )
             {
                 break;
             }

From bf6f94db3a93ff7a4d362997f7436295ec649b0b Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 19:40:07 +0000
Subject: [PATCH 22/29] style: Minor changes

---
 source/core_mqtt.c                     | 6 +++---
 source/interface/transport_interface.h | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 319f28eda..1118d4743 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -696,7 +696,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
     int32_t totalBytesRecvd = 0, bytesRecvd;
-    uint32_t lastDataRecvTimeMs = 0U, timeSinceLastDataWasRecvdMs = 0U;
+    uint32_t lastDataRecvTimeMs = 0U, timeSinceLastRecvdMs = 0U;
     TransportRecv_t recvFunc = NULL;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
@@ -751,11 +751,11 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            timeSinceLastDataWasRecvdMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
+            timeSinceLastRecvdMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
         if( ( bytesRemaining > 0U ) &&
-            ( timeSinceLastDataWasRecvdMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
+            ( timeSinceLastRecvdMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
         {
             LogError( ( "Time expired while receiving packet." ) );
             receiveError = true;
diff --git a/source/interface/transport_interface.h b/source/interface/transport_interface.h
index 000b280d1..a0beb30a5 100644
--- a/source/interface/transport_interface.h
+++ b/source/interface/transport_interface.h
@@ -166,7 +166,7 @@ typedef struct NetworkContext NetworkContext_t;
  * @return The number of bytes received or a negative value to indicate
  * error.
  * @note If no data is available on the network to read and no error
- * has occurred, zero SHOULD be the return value. Zero should NOT be used
+ * has occurred, zero MUST be the return value. Zero MUST NOT be used
  * if a network disconnection has occurred.
  */
 /* @[define_transportrecv] */

From f0a1808e5b71d65bb9ef41c5d3204584a814cc91 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 19:41:26 +0000
Subject: [PATCH 23/29] hygiene: minor name fix

---
 source/core_mqtt.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 1118d4743..412166813 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -696,7 +696,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
     uint8_t * pIndex = NULL;
     size_t bytesRemaining = bytesToRecv;
     int32_t totalBytesRecvd = 0, bytesRecvd;
-    uint32_t lastDataRecvTimeMs = 0U, timeSinceLastRecvdMs = 0U;
+    uint32_t lastDataRecvTimeMs = 0U, timeSinceLastRecvMs = 0U;
     TransportRecv_t recvFunc = NULL;
     MQTTGetCurrentTimeFunc_t getTimeStampMs = NULL;
     bool receiveError = false;
@@ -751,11 +751,11 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         else
         {
             /* No bytes were read from the network. */
-            timeSinceLastRecvdMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
+            timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
         if( ( bytesRemaining > 0U ) &&
-            ( timeSinceLastRecvdMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
+            ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
         {
             LogError( ( "Time expired while receiving packet." ) );
             receiveError = true;

From fcaf4bb9352db8416cf4fe2aef56017d49121dfc Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 21:22:49 +0000
Subject: [PATCH 24/29] fix: Add additional check in timeout logic of recvExact

---
 source/core_mqtt.c | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 412166813..61e37d8ff 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -743,10 +743,8 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             totalBytesRecvd += ( int32_t ) bytesRecvd;
             pIndex += bytesRecvd;
             LogDebug( ( "BytesReceived=%ld, BytesRemaining=%lu, "
-                        "TotalBytesReceived=%ld.",
                         ( long int ) bytesRecvd,
-                        ( unsigned long ) bytesRemaining,
-                        ( long int ) totalBytesRecvd ) );
+                        ( unsigned long ) bytesRemaining ) );
         }
         else
         {
@@ -754,7 +752,8 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
-        if( ( bytesRemaining > 0U ) &&
+        if( ( bytesRecvd == 0 ) &&
+            ( bytesRemaining > 0U ) &&
             ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
         {
             LogError( ( "Time expired while receiving packet." ) );

From b923ea5bf5a3331838e7fc2584d26359220f65c8 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 21:24:08 +0000
Subject: [PATCH 25/29] fix: Add additional check on recvExact

---
 source/core_mqtt.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 61e37d8ff..fd9fc3501 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -752,6 +752,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
         }
 
+        /* Check for timeout if we have been waiting to receive any byte on the network. */
         if( ( bytesRecvd == 0 ) &&
             ( bytesRemaining > 0U ) &&
             ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )

From b1eba613206bd4d02ff2fc500a972f30612fabe3 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 21:31:54 +0000
Subject: [PATCH 26/29] hygiene: move timeout logic within else block for
 better readability

---
 source/core_mqtt.c | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index fd9fc3501..26b396379 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -750,15 +750,14 @@ static int32_t recvExact( const MQTTContext_t * pContext,
         {
             /* No bytes were read from the network. */
             timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
-        }
 
-        /* Check for timeout if we have been waiting to receive any byte on the network. */
-        if( ( bytesRecvd == 0 ) &&
-            ( bytesRemaining > 0U ) &&
-            ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
-        {
-            LogError( ( "Time expired while receiving packet." ) );
-            receiveError = true;
+            /* Check for timeout if we have been waiting to receive any byte on the network. */
+            if( ( bytesRemaining > 0U ) &&
+                ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
+            {
+                LogError( ( "Time expired while receiving packet." ) );
+                receiveError = true;
+            }
         }
     }
 

From 25e74d6fada5f752213fc996b916b5a452795791 Mon Sep 17 00:00:00 2001
From: Archit Aggarwal <architag@amazon.com>
Date: Fri, 4 Dec 2020 22:54:05 +0000
Subject: [PATCH 27/29] hygiene: remove always true condition from if block

---
 source/core_mqtt.c | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/source/core_mqtt.c b/source/core_mqtt.c
index 26b396379..5cb08d77b 100644
--- a/source/core_mqtt.c
+++ b/source/core_mqtt.c
@@ -752,8 +752,7 @@ static int32_t recvExact( const MQTTContext_t * pContext,
             timeSinceLastRecvMs = calculateElapsedTime( getTimeStampMs(), lastDataRecvTimeMs );
 
             /* Check for timeout if we have been waiting to receive any byte on the network. */
-            if( ( bytesRemaining > 0U ) &&
-                ( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS ) )
+            if( timeSinceLastRecvMs >= MQTT_RECV_POLLING_TIMEOUT_MS )
             {
                 LogError( ( "Time expired while receiving packet." ) );
                 receiveError = true;

From b4b0c7806a79dcbb50435b60da3d2a48ab9ae73d Mon Sep 17 00:00:00 2001
From: Sarena Meas <sarem@amazon.com>
Date: Fri, 4 Dec 2020 16:32:26 -0800
Subject: [PATCH 28/29] Update CBMC proofs that use recvExact to specify a
 transport recv stub max tries. - After MAX_NETWORK_RECV_TRIES a zero is
 always returned from the transport recv stub. - When a zero is returned
 recvExact will exit immediately because the max polling timeout is 1.

---
 lexicon.txt                                |  1 +
 test/cbmc/include/core_mqtt_config.h       | 10 +++++-----
 test/cbmc/proofs/MQTT_Connect/Makefile     | 10 ++++++----
 test/cbmc/proofs/MQTT_ProcessLoop/Makefile | 10 ++++++----
 test/cbmc/proofs/MQTT_ReceiveLoop/Makefile | 10 ++++++----
 test/cbmc/stubs/network_interface_stubs.c  | 17 +++++++++++++++++
 6 files changed, 41 insertions(+), 17 deletions(-)

diff --git a/lexicon.txt b/lexicon.txt
index a0f7d0b31..955371872 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -174,6 +174,7 @@ mytcpsocketcontext
 mytlscontext
 networkbuffer
 networkcontext
+networkinterfacereceivestub
 networkinterfacesendstub
 networkrecv
 networksend
diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index 2c2f59f9a..f0136acca 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -81,11 +81,11 @@ struct NetworkContext
  * for any data to be received over the network for the incoming.
  * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
- *
- * For the sake of proving memory safety quickly this is set to zero. When this
- * is set to zero, coverage of each condition in recvExact is reached before
- * ultimately exiting after a single iteration.
+ * 
+ * This is set to 1 to exit right away after a zero is received in the transport
+ * receive stub. There is no added value, in proving memory safety, to repeat
+ * the logic that checks if the polling timeout is reached.
  */
-#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 0U )
+#define MQTT_RECV_POLLING_TIMEOUT_MS            ( 1U )
 
 #endif /* ifndef CORE_MQTT_CONFIG_H_ */
diff --git a/test/cbmc/proofs/MQTT_Connect/Makefile b/test/cbmc/proofs/MQTT_Connect/Makefile
index cb40c9aa2..05f867721 100644
--- a/test/cbmc/proofs/MQTT_Connect/Makefile
+++ b/test/cbmc/proofs/MQTT_Connect/Makefile
@@ -32,12 +32,17 @@ MAX_NETWORK_SEND_TRIES=3
 # time out of 3 we can get coverage of the entire function. Another iteration
 # performed will unnecessarily duplicate the proof.
 MQTT_RECEIVE_TIMEOUT=3
+# The NetworkInterfaceReceiveStub is called once for getting the incoming packet
+# type with one byte of data, then it is called multiple times to reveive the
+# packet.
+MAX_NETWORK_RECV_TRIES=4
 # Please see test/cbmc/include/core_mqtt_config.h for more
 # information on these defines.
 MQTT_STATE_ARRAY_MAX_COUNT=11
 MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT=3
 DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+DEFINES += -DMAX_NETWORK_RECV_TRIES=$(MAX_NETWORK_RECV_TRIES)
 INCLUDES +=
 
 # These functions do not coincide with the call graph of MQTT_Connect, but are
@@ -57,10 +62,7 @@ REMOVE_FUNCTION_BODY += memcpy
 # The loop below is unwound once more than the timeout. The loop below uses
 # the user passed in timeout to break the loop.
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
-# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
-# The possible values from the transport receive can attain coverage with a
-# single iteration.
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES)
 # If the user passed in timeout is zero, then the loop will run until the
 # MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT is reached.
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_receiveConnack.0:$(MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT)
diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
index ad05352e4..f221e4b6b 100644
--- a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
+++ b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile
@@ -32,11 +32,16 @@ MQTT_RECEIVE_TIMEOUT=3
 # Please see test/cbmc/stubs/network_interface_subs.c for
 # more information on MAX_NETWORK_SEND_TRIES.
 MAX_NETWORK_SEND_TRIES=3
+# The NetworkInterfaceReceiveStub is called once for getting the incoming packet
+# type with one byte of data, then it is called multiple times to reveive the
+# packet.
+MAX_NETWORK_RECV_TRIES=4
 # Please see test/cbmc/include/core_mqtt_config.h for more
 # information.
 MQTT_STATE_ARRAY_MAX_COUNT=11
 DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+DEFINES += -DMAX_NETWORK_RECV_TRIES=$(MAX_NETWORK_RECV_TRIES)
 INCLUDES +=
 
 # These functions have their memory saftey proven in other harnesses.
@@ -46,10 +51,7 @@ REMOVE_FUNCTION_BODY += MQTT_SerializeAck
 
 UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_RECEIVE_TIMEOUT)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
-# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
-# The possible values from the transport receive can attain coverage with a
-# single iteration.
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES)
 # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
 # sendPacket will continue until all the bytes are sent or a network error
 # occurs. Please see NetworkInterfaceReceiveStub in
diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
index b4227e452..f41d6a331 100644
--- a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
+++ b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile
@@ -11,6 +11,10 @@ PROOF_UID=MQTT_ReceiveLoop
 # out of 2 we can get coverage of the entire function. Another iteration will
 # performed unnecessarily duplicating of the proof.
 MQTT_RECEIVE_TIMEOUT=3
+# The NetworkInterfaceReceiveStub is called once for getting the incoming packet
+# type with one byte of data, then it is called multiple times to reveive the
+# packet.
+MAX_NETWORK_RECV_TRIES=4
 # Please see test/cbmc/stubs/network_interface_subs.c for
 # more information on MAX_NETWORK_SEND_TRIES.
 MAX_NETWORK_SEND_TRIES=3
@@ -19,6 +23,7 @@ MAX_NETWORK_SEND_TRIES=3
 MQTT_STATE_ARRAY_MAX_COUNT=11
 DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT)
 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES)
+DEFINES += -DMAX_NETWORK_RECV_TRIES=$(MAX_NETWORK_RECV_TRIES)
 INCLUDES +=
 
 # These functions have their memory saftey proven in other harnesses.
@@ -28,10 +33,7 @@ REMOVE_FUNCTION_BODY += MQTT_SerializeAck
 # The loops below are unwound once more than the exclusive timeout bound.
 UNWINDSET += MQTT_ReceiveLoop.0:$(MQTT_RECEIVE_TIMEOUT)
 UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT)
-# recvExact only iterates once with MQTT_RECV_POLLING_TIMEOUT_MS set to zero.
-# The possible values from the transport receive can attain coverage with a
-# single iteration.
-UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:2
+UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MAX_NETWORK_RECV_TRIES)
 # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in
 # sendPacket will continue until all the bytes are sent or a network error
 # occurs. Please see NetworkInterfaceReceiveStub in
diff --git a/test/cbmc/stubs/network_interface_stubs.c b/test/cbmc/stubs/network_interface_stubs.c
index 6b042e9fe..15afe7bb3 100644
--- a/test/cbmc/stubs/network_interface_stubs.c
+++ b/test/cbmc/stubs/network_interface_stubs.c
@@ -35,6 +35,13 @@
     #define MAX_NETWORK_SEND_TRIES    3
 #endif
 
+/* An exclusive bound on the times that the NetworkInterfaceReceiveStub will
+ * return an unbound value. At this value and beyond, the
+ * NetworkInterfaceReceiveStub will return zero on every call. */
+#ifndef MAX_NETWORK_RECV_TRIES
+    #define MAX_NETWORK_RECV_TRIES    4
+#endif
+
 int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
                                      void * pBuffer,
                                      size_t bytesToRecv )
@@ -48,11 +55,21 @@ int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
     __CPROVER_havoc_object( pBuffer );
 
     int32_t bytesOrError;
+    static size_t tries = 0;
 
     /* It is a bug for the application defined transport send function to return
      * more than bytesToRecv. */
     __CPROVER_assume( bytesOrError <= ( int32_t ) bytesToRecv );
 
+    if( tries < ( MAX_NETWORK_RECV_TRIES - 1 ) )
+    {
+        tries++;
+    }
+    else
+    {
+        bytesOrError = 0;
+    }
+    
     return bytesOrError;
 }
 

From 95abb9326357397fce0f1914cdd999aa4b9461ba Mon Sep 17 00:00:00 2001
From: Sarena Meas <sarem@amazon.com>
Date: Fri, 4 Dec 2020 16:35:40 -0800
Subject: [PATCH 29/29] Uncrustify.:

---
 test/cbmc/include/core_mqtt_config.h      | 2 +-
 test/cbmc/stubs/network_interface_stubs.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index f0136acca..16964e14d 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -81,7 +81,7 @@ struct NetworkContext
  * for any data to be received over the network for the incoming.
  * If the timeout expires, the #MQTT_ProcessLoop or #MQTT_ReceiveLoop functions
  * return #MQTTRecvFailed.
- * 
+ *
  * This is set to 1 to exit right away after a zero is received in the transport
  * receive stub. There is no added value, in proving memory safety, to repeat
  * the logic that checks if the polling timeout is reached.
diff --git a/test/cbmc/stubs/network_interface_stubs.c b/test/cbmc/stubs/network_interface_stubs.c
index 15afe7bb3..cb182c42b 100644
--- a/test/cbmc/stubs/network_interface_stubs.c
+++ b/test/cbmc/stubs/network_interface_stubs.c
@@ -69,7 +69,7 @@ int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
     {
         bytesOrError = 0;
     }
-    
+
     return bytesOrError;
 }