Skip to content

Commit

Permalink
Fix CBMC proof for xCheckRequiresARPResolution and formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
tony-josi-aws committed Nov 8, 2024
1 parent 5341b9b commit c260cfc
Showing 1 changed file with 5 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -89,12 +89,10 @@ void harness()
size_t xBufferLength;
NetworkBufferDescriptor_t * pxNetworkBuffer;
IPPacket_t * pxIPPacket;

const IPPacket_t * pxIPPacket;
const IPHeader_t * pxIPHeader;
IPHeader_t * pxIPHeader;

/* Make sure buffer size is enough, xCheckRequiresARPResolution is only called for
IPv4 packets hence the minimum size should be sizeof( IPPacket_t ) */
* IPv4 packets hence the minimum size should be sizeof( IPPacket_t ) */
__CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );

pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
Expand All @@ -106,11 +104,12 @@ void harness()
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );

/* Its asserted in the code that xCheckRequiresARPResolution is only called on IPv4 frame types */

/* See assertion: configASSERT( ( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE ) || ( pxIPPacket->xEthernetHeader.usFrameType == ipARP_FRAME_TYPE ) );
in xCheckRequiresARPResolution() */
* in xCheckRequiresARPResolution() */
pxIPPacket = ( ( const IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer );
pxIPHeader = &( pxIPPacket->xIPHeader );
__CPROVER_assume(pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE);
__CPROVER_assume( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE );

pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
__CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
Expand Down

0 comments on commit c260cfc

Please sign in to comment.