Searched refs:ensure_memory_is_valid (Results 1 – 7 of 7) sorted by relevance
| /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/TCP/prvTCPHandleState/ |
| D | TCPHandleState_harness.c | 69 if( ensure_memory_is_valid( pxSocket, socketSize ) ) in harness()
94 if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) ) in harness()
100 if( ensure_memory_is_valid( pxSocket, socketSize ) && in harness()
101 ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) && in harness()
102 ensure_memory_is_valid( pxNetworkBuffer->pucEthernetBuffer, sizeof( TCPPacket_t ) ) && in harness()
103 ensure_memory_is_valid( pxSocket->u.xTCP.pxPeerSocket, socketSize ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v4.0.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-v4.0.0/test/cbmc/proofs/TCP/prvTCPReturnPacket/ |
| D | TCPReturnPacket_harness.c | 93 if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) in pxDuplicateNetworkBufferWithDescriptor()
149 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in harness()
162 if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/ |
| D | TCPReturnPacket_IPv6_harness.c | 92 if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) ) in pxDuplicateNetworkBufferWithDescriptor()
148 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in harness()
161 if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/TCP/prvTCPPrepareSend/ |
| D | TCPPrepareSend_harness.c | 53 if( ensure_memory_is_valid( pxBuffer, bufferSize ) ) in pxGetNetworkBufferWithDescriptor()
85 if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) ) in harness()
|
| /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ |
| D | ProcessICMPMessage_IPv6_harness.c | 105 if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) in FreeRTOS_FindEndPointOnIP_IPv6()
|
| /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ |
| D | ReturnICMP_IPv6_harness.c | 108 if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) ) in FreeRTOS_FindEndPointOnIP_IPv6()
|
