xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ARP/xCheckLoopback/xCheckLoopback_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_ARP.h"
8 
9 /* CBMC includes. */
10 #include "cbmc.h"
11 
12 /* Abstraction of FreeRTOS_FindEndPointOnMAC. */
FreeRTOS_FindEndPointOnMAC(const MACAddress_t * pxMACAddress,const NetworkInterface_t * pxInterface)13 NetworkEndPoint_t * FreeRTOS_FindEndPointOnMAC( const MACAddress_t * pxMACAddress,
14                                                 const NetworkInterface_t * pxInterface )
15 {
16     NetworkEndPoint_t * pxReturnEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
17 
18     return pxReturnEndPoint;
19 }
20 
21 /* Abstraction of pxDuplicateNetworkBufferWithDescriptor. */
pxDuplicateNetworkBufferWithDescriptor(const NetworkBufferDescriptor_t * const pxNetworkBuffer,size_t uxNewLength)22 NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
23                                                                     size_t uxNewLength )
24 {
25     /* In this function, we can either return NULL or valid pointer as return value. */
26     NetworkBufferDescriptor_t * pxReturnNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
27 
28     if( pxReturnNetworkBuffer )
29     {
30         /* If the pointer is valid, we must have enough ethernet buffer for it with correct data length. */
31         pxReturnNetworkBuffer->pucEthernetBuffer = safeMalloc( uxNewLength );
32         __CPROVER_assume( pxReturnNetworkBuffer->pucEthernetBuffer != NULL );
33 
34         pxReturnNetworkBuffer->xDataLength = uxNewLength;
35     }
36 
37     return pxReturnNetworkBuffer;
38 }
39 
harness()40 void harness()
41 {
42     size_t xBufferLength;
43     NetworkBufferDescriptor_t * pxNetworkBuffer;
44     BaseType_t bReleaseAfterSend;
45 
46     __CPROVER_assume( ( xBufferLength >= 0 ) &&
47                       ( xBufferLength < ipconfigNETWORK_MTU ) );
48 
49     pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
50 
51     if( pxNetworkBuffer )
52     {
53         /* If buffer pointer is valid, allocate ethernet buffer and set data length for it. */
54         pxNetworkBuffer->xDataLength = xBufferLength;
55 
56         pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xBufferLength );
57         __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
58     }
59 
60     ( void ) xCheckLoopback( pxNetworkBuffer, bReleaseAfterSend );
61 }
62