Searched refs:ensure_memory_is_valid (Results 1 – 4 of 4) sorted by relevance
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/TCP/prvTCPHandleState/ |
| D | TCPHandleState_harness.c | 67 if( ensure_memory_is_valid( pxSocket, socketSize ) ) in harness()
89 if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) ) in harness()
94 if( ensure_memory_is_valid( pxSocket, socketSize ) && in harness()
95 ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) && in harness()
96 ensure_memory_is_valid( pxNetworkBuffer->pucEthernetBuffer, sizeof( TCPPacket_t ) ) && in harness()
97 ensure_memory_is_valid( pxSocket->u.xTCP.pxPeerSocket, socketSize ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/utility/ |
| D | memory_assignments.c | 3 #define ensure_memory_is_valid( px, length ) ( px != NULL ) && __CPROVER_w_ok( ( px ), length ) macro
18 if( ensure_memory_is_valid( pxSocket, sizeof( FreeRTOS_Socket_t ) ) ) in ensure_FreeRTOS_Socket_t_is_allocated()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/TCP/prvTCPPrepareSend/ |
| D | TCPPrepareSend_harness.c | 53 if( ensure_memory_is_valid( pxBuffer, bufferSize ) ) in pxGetNetworkBufferWithDescriptor()
72 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/TCP/prvTCPReturnPacket/ |
| D | TCPReturnPacket_harness.c | 54 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in pxDuplicateNetworkBufferWithDescriptor()
107 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in harness()
|
