Keep assumptions in validity functions

Signed-off-by: Felipe R. Monteiro <[email protected]>
FreeRTOS · Oct 27, 2021 · 702c4bb · 702c4bb
1 parent 495b7d7
commit 702c4bb
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c
@@ -35,7 +35,6 @@ void harness()
 
     pIncomingPacket = allocateMqttPacketInfo( NULL );
     __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) );
-    __CPROVER_assume( IMPLIES( pIncomingPacket != NULL, pIncomingPacket->remainingLength < REMAINING_LENGTH_MAX ) );
 
     /* These are allocated for coverage of a NULL input. */
     pPacketId = malloc( sizeof( uint16_t ) );

diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c
@@ -69,6 +69,11 @@ bool isValidMqttPacketInfo( const MQTTPacketInfo_t * pPacketInfo )
 {
     bool isValid = true;
 
+    if( pPacketInfo != NULL )
+    {
+        isValid = isValid && pPacketInfo->remainingLength < REMAINING_LENGTH_MAX;
+    }
+
     return isValid;
 }