1 /* FreeRTOS includes. */
2 #include "FreeRTOS.h"
3 #include "queue.h"
4 #include "list.h"
5
6 /* FreeRTOS+TCP includes. */
7 #include "FreeRTOS_IP.h"
8 #include "FreeRTOS_DNS.h"
9 #include "FreeRTOS_IP_Private.h"
10
11
12 /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
13
14 void vDNSInitialise( void );
15
16 void vDNSSetCallBack( const char * pcHostName,
17 void * pvSearchID,
18 FOnDNSEvent pCallbackFunction,
19 TickType_t xTimeout,
20 TickType_t xIdentifier );
21
safeMalloc(size_t xWantedSize)22 void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
23 {
24 if( xWantedSize == 0 )
25 {
26 return NULL;
27 }
28
29 uint8_t byte;
30
31 return byte ? malloc( xWantedSize ) : NULL;
32 }
33
34 /* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut,TickType_t * const pxTicksToWait)35 BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
36 TickType_t * const pxTicksToWait )
37 {
38 }
39
40 /* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
xTaskResumeAll(void)41 BaseType_t xTaskResumeAll( void )
42 {
43 }
44
45 /* The function func mimics the callback function.*/
func(const char * pcHostName,void * pvSearchID,uint32_t ulIPAddress)46 void func( const char * pcHostName,
47 void * pvSearchID,
48 uint32_t ulIPAddress )
49 {
50 }
51
harness()52 void harness()
53 {
54 vDNSInitialise(); /* We initialize the callbacklist in order to be able to check for functions that timed out. */
55 size_t pvSearchID;
56 FOnDNSEvent pCallback = func;
57 TickType_t xTimeout;
58 TickType_t xIdentifier;
59 size_t len;
60
61 __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
62 char * pcHostName = safeMalloc( len );
63
64 if( len && pcHostName )
65 {
66 pcHostName[ len - 1 ] = NULL;
67 }
68
69 vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier ); /* Add an item to be able to check the cancel function if the list is non-empty. */
70 FreeRTOS_gethostbyname_cancel( &pvSearchID );
71 }
72
