Fix CBMC testing

HTRamsey · Oct 16, 2024 · 8af0a42 · 8af0a42
1 parent 0f744c8
commit 8af0a42
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 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
@@ -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
@@ -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
@@ -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/...cbmc/proofs/parsing/ProcessReceivedUDPPacket_IPv6/ProcessReceivedUDPPacket_IPv6_harness.c b/...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 );