1 #include <stdlib.h>
2 
3 #define ensure_memory_is_valid( px, length )    ( px != NULL ) && __CPROVER_w_ok( ( px ), length )
4 
5 /* Implementation of safe malloc which returns NULL if the requested size is 0.
6  * Warning: The behavior of malloc(0) is platform dependent.
7  * It is possible for malloc(0) to return an address without allocating memory.*/
safeMalloc(size_t xWantedSize)8 void * safeMalloc( size_t xWantedSize )
9 {
10     return nondet_bool() ? malloc( xWantedSize ) : NULL;
11 }
12 
13 /* Memory assignment for FreeRTOS_Socket_t */
ensure_FreeRTOS_Socket_t_is_allocated()14 FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
15 {
16     FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
17 
18     if( ensure_memory_is_valid( pxSocket, sizeof( FreeRTOS_Socket_t ) ) )
19     {
20         pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
21         pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
22         pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
23         pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
24     }
25 
26     return pxSocket;
27 }
28 
29 /* Memory assignment for FreeRTOS_Network_Buffer */
ensure_FreeRTOS_NetworkBuffer_is_allocated()30 NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated()
31 {
32     return safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
33 }
34