summaryrefslogtreecommitdiff
path: root/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
blob: 3dae34a341d1f62a9bd4492cacb9498bc952f275 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
/* This harness is linked against
 * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto
 */
#include <stdint.h>
#include <stdio.h>

/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "task.h"
#include "queue.h"
#include "semphr.h"

/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_Sockets.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_ARP.h"
#include "FreeRTOS_UDP_IP.h"
#include "FreeRTOS_DHCP.h"
#if( ipconfigUSE_LLMNR == 1 )
	#include "FreeRTOS_DNS.h"
#endif /* ipconfigUSE_LLMNR */
#include "NetworkInterface.h"
#include "NetworkBufferManagement.h"

void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){
	for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){
		NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x];
		#ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES
			current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t)));
		#else
			current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t));
		#endif
		current->xDataLength = sizeof(ARPPacket_t);
	}
}

/* The code expects that the Semaphore creation relying on pvPortMalloc
   is successful. This is checked by an assert statement, that gets
   triggered when the allocation fails. Nevertheless, the code is perfectly
   guarded against a failing Semaphore allocation. To make the assert pass,
   it is assumed for now, that pvPortMalloc doesn't fail. Using a model allowing
   failures of the allocation might be possible
   after removing the assert in l.105 of BufferAllocation_1.c, from a memory
   safety point of view. */
void *pvPortMalloc( size_t xWantedSize ){
	return malloc(xWantedSize);
}

/*
 * This function is implemented by a third party.
 * After looking through a couple of samples in the demos folder, it seems
 * like the only shared contract is that you want to add the if statement
 * for releasing the buffer to the end. Apart from that, it is up to the vendor,
 * how to write this code out to the network.
 */
BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){
	if( bReleaseAfterSend != pdFALSE )
	{
		vReleaseNetworkBufferAndDescriptor( pxDescriptor );
	}
}

void harness()
{
	BaseType_t xRes = xNetworkBuffersInitialise();
	if(xRes == pdPASS){
		uint32_t ulIPAddress;
		FreeRTOS_OutputARPRequest( ulIPAddress );
	}
}