diff --git a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c index 6bfa7740bb..41240a8f37 100644 --- a/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c +++ b/test/cbmc/proofs/DHCPv6/Process_PassReplyToEndPoint/DHCPv6Process_PassReplyToEndPoint_harness.c @@ -59,7 +59,6 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndP void harness() { - BaseType_t xResult; pxNetworkEndPoints = safeMalloc( sizeof( NetworkEndPoint_t ) ); diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c index 15a99869a7..831c2c2925 100644 --- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c +++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c @@ -57,6 +57,7 @@ void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_ void harness() { NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); /* The application provides the random number and time hook in a memory safe manner. */