xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/DNS/NBNSHandlePacket/NBNSHandlePacket_harness.c (revision 2d3f4daa567ffe71aeda2e0f6d0bc02850db0627) 
1 /* FreeRTOS includes. */
2 #include "FreeRTOS.h"
3 #include "queue.h"
4 
5 /* FreeRTOS+TCP includes. */
6 #include "FreeRTOS_IP.h"
7 #include "FreeRTOS_DNS.h"
8 #include "FreeRTOS_DNS_Parser.h"
9 #include "FreeRTOS_IP_Private.h"
10 
11 #include "cbmc.h"
12 
13 NetworkBufferDescriptor_t xNetworkBuffer;
14 
15 /* DNS_TreatNBNS is proved separately */
DNS_TreatNBNS(uint8_t * pucPayload,size_t uxBufferLength,uint32_t ulIPAddress)16 void DNS_TreatNBNS( uint8_t * pucPayload,
17                     size_t uxBufferLength,
18                     uint32_t ulIPAddress )
19 {
20     __CPROVER_assert( pucPayload != NULL, "Precondition: pucPayload != NULL" );
21 }
22 
harness()23 void harness()
24 {
25     uint32_t ulIPAddress;
26 
27     BaseType_t xDataSize;
28 
29     /* Assume an upper limit on max memory that can be allocated */
30     __CPROVER_assume( ( xDataSize < ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) );
31     xNetworkBuffer.xDataLength = xDataSize;
32 
33     xNetworkBuffer.pucEthernetBuffer = safeMalloc( xDataSize );
34 
35     /* pucEthernetBuffer being not NULL is pre validated before the call to ulNBNSHandlePacket */
36     __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
37 
38     xNetworkBuffer.pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
39 
40     ulNBNSHandlePacket( &xNetworkBuffer );
41 }
42