From 8af0a42bea1015289b62b49a2707890e61ea67b2 Mon Sep 17 00:00:00 2001 From: ActoryOu Date: Wed, 16 Oct 2024 09:33:33 +0000 Subject: [PATCH] Fix CBMC testing --- .../ProcessICMPMessage_IPv6_harness.c | 8 ++++---- .../ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c | 6 +++--- .../parsing/ProcessIPPacket/ProcessIPPacket_harness.c | 4 +++- .../ProcessReceivedUDPPacket_IPv6_harness.c | 6 ++++-- 4 files changed, 14 insertions(+), 10 deletions(-) diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c index 0b02ac8ed..8fdbc87a7 100644 --- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c +++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c @@ -156,7 +156,7 @@ void harness() * which is validated only when bIPv6 is set*/ __CPROVER_assume( ( pxNetworkBuffer->pxEndPoint != NULL ) && ( pxNetworkBuffer->pxEndPoint->bits.bIPv6 == pdTRUE_UNSIGNED ) ); - /* Non deterministically determine whether the pxARPWaitingNetworkBuffer will + /* Non deterministically determine whether the pxNDWaitingNetworkBuffer will * point to some valid data or will it be NULL. */ if( nondet_bool() ) { @@ -167,7 +167,7 @@ void harness() pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 ); /* Since this pointer is maintained by the IP-task, either the pointer - * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer + * pxNDWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer * will be non-NULL. */ __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL ); __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL ); @@ -176,11 +176,11 @@ void harness() /* Add matching data length to the network buffer descriptor. */ pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize; - pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; + pxNDWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; } else { - pxARPWaitingNetworkBuffer = NULL; + pxNDWaitingNetworkBuffer = NULL; } prvProcessICMPMessage_IPv6( pxNetworkBuffer ); diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c index e0340a76c..597734285 100644 --- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c +++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c @@ -161,7 +161,7 @@ void harness() __CPROVER_assume( ( pxNetworkBuffer->pxEndPoint != NULL ) && ( pxNetworkBuffer->pxEndPoint->bits.bIPv6 == pdTRUE_UNSIGNED ) ); - /* Initializing pxARPWaitingNetworkBuffer */ + /* Initializing pxNDWaitingNetworkBuffer */ /* The packet must at least be as big as an IPv6 Packet. The size is not * checked in the function as the pointer is stored by the IP-task itself @@ -170,7 +170,7 @@ void harness() pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 ); /* Since this pointer is maintained by the IP-task, either the pointer - * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer + * pxNDWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer * will be non-NULL. */ __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL ); __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL ); @@ -179,7 +179,7 @@ void harness() /* Add matching data length to the network buffer descriptor. */ pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize; - pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; + pxNDWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer; prvProcessICMPMessage_IPv6( pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c index 5b926e4c4..add375d18 100644 --- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c +++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -42,12 +42,14 @@ BaseType_t xGetExtensionOrder( uint8_t ucProtocol, return xIsExtensionHeader( ucProtocol ); } -BaseType_t xCheckRequiresARPResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer ) +BaseType_t xCheckRequiresResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer ) { BaseType_t xReturn; __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" ); + + return xReturn; } void vARPRefreshCacheEntryAge( const MACAddress_t * pxMACAddress, diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket_IPv6/ProcessReceivedUDPPacket_IPv6_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket_IPv6/ProcessReceivedUDPPacket_IPv6_harness.c index 5737bb359..aef236b61 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket_IPv6/ProcessReceivedUDPPacket_IPv6_harness.c +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket_IPv6/ProcessReceivedUDPPacket_IPv6_harness.c @@ -43,11 +43,12 @@ FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort ) } /* This proof was done before. Hence we assume it to be correct here. */ -BaseType_t xCheckRequiresARPResolution( NetworkBufferDescriptor_t * pxNetworkBuffer ) +BaseType_t xCheckRequiresNDResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer ) { BaseType_t xReturn; - __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) ); + __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" ); + __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" ); return xReturn; } @@ -95,6 +96,7 @@ void harness() pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( UDPPacket_IPv6_t ) ); pxNetworkBuffer->pxEndPoint = &xEndpoint; + pxNetworkBuffer->xDataLength = sizeof( UDPPacket_IPv6_t ); /* The ethernet buffer must be valid. */ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );