1 /* FreeRTOS includes. */
2 #include "FreeRTOS.h"
3 #include "queue.h"
4
5 /* FreeRTOS+TCP includes. */
6 #include "FreeRTOS_IP.h"
7 #include "FreeRTOS_IP_Private.h"
8
9 /* proof is done separately */
xProcessReceivedTCPPacket(NetworkBufferDescriptor_t * pxNetworkBuffer)10 BaseType_t xProcessReceivedTCPPacket( NetworkBufferDescriptor_t * pxNetworkBuffer )
11 {
12 }
13
14 /* proof is done separately */
xProcessReceivedUDPPacket(NetworkBufferDescriptor_t * pxNetworkBuffer,uint16_t usPort)15 BaseType_t xProcessReceivedUDPPacket( NetworkBufferDescriptor_t * pxNetworkBuffer,
16 uint16_t usPort )
17 {
18 }
19
20 /* This proof was done before. Hence we assume it to be correct here. */
vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress,const uint32_t ulIPAddress)21 void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress,
22 const uint32_t ulIPAddress )
23 {
24 }
25
26 eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket,
27 NetworkBufferDescriptor_t * const pxNetworkBuffer );
28
29 #if ( ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM == 0 )
30
31 /* The checksum generation is stubbed out since the actual checksum
32 * does not matter. The stub will return an indeterminate value each time. */
usGenerateChecksum(uint16_t usSum,const uint8_t * pucNextData,size_t uxByteCount)33 uint16_t usGenerateChecksum( uint16_t usSum,
34 const uint8_t * pucNextData,
35 size_t uxByteCount )
36 {
37 uint16_t usReturn;
38
39 __CPROVER_assert( pucNextData != NULL, "Next data cannot be NULL" );
40
41 /* Return an indeterminate value. */
42 return usReturn;
43 }
44
45 /* The checksum generation is stubbed out since the actual checksum
46 * does not matter. The stub will return an indeterminate value each time. */
usGenerateProtocolChecksum(const uint8_t * const pucEthernetBuffer,size_t uxBufferLength,BaseType_t xOutgoingPacket)47 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
48 size_t uxBufferLength,
49 BaseType_t xOutgoingPacket )
50 {
51 uint16_t usReturn;
52
53 __CPROVER_assert( pucEthernetBuffer != NULL, "Ethernet buffer cannot be NULL" );
54
55 /* Return an indeterminate value. */
56 return usReturn;
57 }
58 #endif /* if ( ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM == 0 ) */
59
harness()60 void harness()
61 {
62 NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc( sizeof( NetworkBufferDescriptor_t ) );
63
64 __CPROVER_assume( pxNetworkBuffer != NULL );
65
66 /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/
67 pxNetworkBuffer->pucEthernetBuffer = malloc( ipTOTAL_ETHERNET_FRAME_SIZE );
68 __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
69
70 /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */
71 __CPROVER_assume( pxNetworkBuffer->xDataLength >= sizeof( IPPacket_t ) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE );
72
73 IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer;
74
75 publicProcessIPPacket( pxIPPacket, pxNetworkBuffer );
76 }
77
