Merge branch 'FreeRTOS:main' into coreMQTTThreadSafe

FreeRTOS · Sep 26, 2024 · bd28bbd · bd28bbd
2 parents 33340d2 + 6a3ec09
commit bd28bbd
Show file tree

Hide file tree

Showing 7 changed files with 234 additions and 188 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -191,7 +191,7 @@ jobs:
       - name: Set up CBMC runner
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
         with:
-          cbmc_version: "5.95.1"
+          cbmc_version: "6.3.1"
       - name: Run CBMC
         uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main
         with:

diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c b/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c
@@ -29,6 +29,15 @@
 #include "core_mqtt.h"
 #include "mqtt_cbmc_state.h"
 
+MQTTStatus_t MQTT_DeserializeAck( const MQTTPacketInfo_t * pIncomingPacket,
+                                  uint16_t * pPacketId,
+                                  bool * pSessionPresent )
+{
+    MQTTStatus_t result;
+
+    return result;
+}
+
 void harness()
 {
     MQTTContext_t * pContext;

diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c b/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c
@@ -29,6 +29,15 @@
 #include "core_mqtt.h"
 #include "mqtt_cbmc_state.h"
 
+MQTTStatus_t MQTT_DeserializeAck( const MQTTPacketInfo_t * pIncomingPacket,
+                                  uint16_t * pPacketId,
+                                  bool * pSessionPresent )
+{
+    MQTTStatus_t result;
+
+    return result;
+}
+
 void harness()
 {
     MQTTContext_t * pContext;

diff --git a/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c b/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c
@@ -36,7 +36,7 @@ void harness()
     uint16_t packetId;
 
     pFixedBuffer = allocateMqttFixedBuffer( NULL );
-    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
 
     MQTT_SerializeAck( pFixedBuffer, packetType, packetId );
 }
diff --git a/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c b/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c
@@ -34,7 +34,7 @@ void harness()
     MQTTFixedBuffer_t * pFixedBuffer;
 
     pFixedBuffer = allocateMqttFixedBuffer( NULL );
-    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
 
     MQTT_SerializeDisconnect( pFixedBuffer );
 }
diff --git a/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c b/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c
@@ -34,7 +34,7 @@ void harness()
     MQTTFixedBuffer_t * pFixedBuffer;
 
     pFixedBuffer = allocateMqttFixedBuffer( NULL );
-    __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) );
+    __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) );
 
     MQTT_SerializePingreq( pFixedBuffer );
 }