Null check

FreeRTOS · Mar 19, 2021 · b541382 · b541382
1 parent 7d12d86
commit b541382
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
@@ -65,6 +65,9 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * pxDescriptor,
 {
     BaseType_t xReturn;
 
+    __CPROVER_assert( pxDescriptor, "The descriptor cannot be NULL" );
+    __CPROVER_assert( pxDescriptor->pucEthernetBuffer, "The ethernet buffer cannot be NULL" );
+
     return xReturn;
 }