Fix Disconnect CBMC proof and update size table

FreeRTOS · Sep 21, 2022 · 0737ab4 · 0737ab4
1 parent 06e5ea8
commit 0737ab4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
@@ -10,7 +10,7 @@
     <tr>
         <td>core_mqtt.c</td>
         <td><center>3.9K</center></td>
-        <td><center>3.3K</center></td>
+        <td><center>3.4K</center></td>
     </tr>
     <tr>
         <td>core_mqtt_state.c</td>
@@ -25,6 +25,6 @@
     <tr>
         <td><b>Total estimates</b></td>
         <td><b><center>8.4K</center></b></td>
-        <td><b><center>6.8K</center></b></td>
+        <td><b><center>6.9K</center></b></td>
     </tr>
 </table>
diff --git a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c
@@ -33,6 +33,8 @@ void harness()
 
     pContext = allocateMqttContext( NULL );
     __CPROVER_assume( isValidMqttContext( pContext ) );
+    __CPROVER_assume( pContext != NULL ); 
+    __CPROVER_assume( pContext->networkBuffer.pBuffer != NULL );
 
     MQTT_Disconnect( pContext );
 }