Update Agent to treat MQTTNeedMoreBytes correctly (#103)

* Update MQTT Agent to treat MQTTNeedMoreBytes correctly
FreeRTOS · Aug 28, 2023 · d3668a6 · d3668a6
1 parent a991b39
commit d3668a6
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 2 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -106,7 +106,7 @@ jobs:
             config: .github/memory_statistics_config.json
             check_against: docs/doxygen/include/size_table.md
   proof_ci:
-    runs-on: cbmc_ubuntu-latest_16-core
+    runs-on: cbmc_ubuntu-latest_64-core
     steps:
       - name: Set up CBMC runner
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main

diff --git a/lexicon.txt b/lexicon.txt
@@ -130,6 +130,7 @@ mqtteventcallback
 mqttfixedbuffer
 mqttgetcurrenttimefunc
 mqttkeepalivetimeout
+mqttneedmorebytes
 mqttnomemory
 mqttnotconnected
 mqttpublishinfo

diff --git a/source/core_mqtt_agent.c b/source/core_mqtt_agent.c
@@ -613,6 +613,12 @@ static MQTTStatus_t processCommand( MQTTAgentContext_t * pMqttAgentContext,
         } while( pMqttAgentContext->packetReceivedInLoop );
     }
 
+    if( operationStatus == MQTTNeedMoreBytes )
+    {
+        /* Reset the operation status as MQTTNeedMoreBytes is not an error condition. */
+        operationStatus = MQTTSuccess;
+    }
+
     /* Set the flag to break from the command loop. */
     *pEndLoop = ( commandOutParams.endLoop || ( operationStatus != MQTTSuccess ) );
 

diff --git a/test/cbmc/proofs/MQTTAgent_CommandLoop/Makefile b/test/cbmc/proofs/MQTTAgent_CommandLoop/Makefile
@@ -27,6 +27,10 @@ MAX_BOUND_FOR_COMMAND_LOOP=3
 # the loop 2 times will be enough for proving memory safety.
 MAX_BOUND_FOR_PROCESS_COMMAND_LOOP=2
 
+# Force CBMC to only use the AgentMessageRecvStub function as the pointee of
+# the recv function.
+RESTRICT_FUNCTION_POINTER += MQTTAgent_CommandLoop.function_pointer_call.1/AgentMessageRecvStub
+
 DEFINES += -DMQTT_AGENT_MAX_OUTSTANDING_ACKS=$(MQTT_AGENT_MAX_OUTSTANDING_ACKS)
 
 INCLUDES +=

diff --git a/test/unit-test/mqtt_agent_utest.c b/test/unit-test/mqtt_agent_utest.c
@@ -1753,7 +1753,7 @@ void test_MQTTAgent_CommandLoop_NoCommand_NoData( void )
 
     mqttStatus = MQTTAgent_CommandLoop( &mqttAgentContext );
 
-    TEST_ASSERT_EQUAL( MQTTNeedMoreBytes, mqttStatus );
+    TEST_ASSERT_EQUAL( MQTTSuccess, mqttStatus );
 }
 
 /**
-Original file line number
+Diff line change
@@ Expand Up / @@ -1753,7 +1753,7 @@ void test_MQTTAgent_CommandLoop_NoCommand_NoData( void ) @@
         mqttStatus = MQTTAgent_CommandLoop( &mqttAgentContext );
-        TEST_ASSERT_EQUAL( MQTTNeedMoreBytes, mqttStatus );
+        TEST_ASSERT_EQUAL( MQTTSuccess, mqttStatus );
     }
     /**
@@ Expand Down @@