blob: 1e5832b20d363b0162f4f4408064c6bb3e9f4683 (
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
|
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "queue.h"
#include "list.h"
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_DNS.h"
#include "FreeRTOS_IP_Private.h"
/* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
void vDNSInitialise(void);
void vDNSSetCallBack(const char *pcHostName, void *pvSearchID, FOnDNSEvent pCallbackFunction, TickType_t xTimeout, TickType_t xIdentifier);
void *safeMalloc(size_t xWantedSize) { /* Returns a NULL pointer if the wanted size is 0. */
if(xWantedSize == 0) {
return NULL;
}
uint8_t byte;
return byte ? malloc(xWantedSize) : NULL;
}
/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
BaseType_t xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait) { }
/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
BaseType_t xTaskResumeAll(void) { }
/* The function func mimics the callback function.*/
void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) {}
void harness() {
vDNSInitialise(); /* We initialize the callbacklist in order to be able to check for functions that timed out. */
size_t pvSearchID;
FOnDNSEvent pCallback = func;
TickType_t xTimeout;
TickType_t xIdentifier;
size_t len;
__CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN);
char *pcHostName = safeMalloc(len);
if (len && pcHostName) {
pcHostName[len-1] = NULL;
}
vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier); /* Add an item to be able to check the cancel function if the list is non-empty. */
FreeRTOS_gethostbyname_cancel(&pvSearchID);
}
|
