xref: /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/utility/memory_assignments.c (revision 9d15770091225885eac5dbecba5cdb6840843db2) 
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     }
24 
25     return pxSocket;
26 }
27 
28 /* Memory assignment for FreeRTOS_Network_Buffer */
ensure_FreeRTOS_NetworkBuffer_is_allocated()29 NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated()
30 {
31     return safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
32 }
33