Adjust proof tooling to support CBMC v6 (#304)

Description
-----------
With CBMC v6, unwinding assertions are enabled by default, and object
bits no longer need to be set at compile time. Update various build
rules to use the latest template as provided with CBMC starter kit.

Test Steps
-----------
Tested in CI.

Checklist:
----------
<!--- Go over all the following points, and put an `x` in all the boxes
that apply. -->
<!--- If you're unsure about any of these, don't hesitate to ask. We're
here to help! -->
- [ ] I have tested my changes. No regression in existing tests.
- n/a I have modified and/or added unit-tests to cover the code changes
in this Pull Request.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

.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:

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;

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;

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 );
 }

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 );
 }

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 );
 }