Searched refs:CBMC_MAX_OBJECT_SIZE (Results 1 – 11 of 11) sorted by relevance
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/ParseDNSReply/ |
| D | ParseDNSReply_harness.c | 41 __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()
43 __CPROVER_assert( NAME_SIZE < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()
50 __CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()
52 __CPROVER_assert( uxDestLen < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()
89 __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, in DNS_SkipNameField()
94 __CPROVER_assert( uxLength < CBMC_MAX_OBJECT_SIZE, in DNS_SkipNameField()
120 __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, in harness()
123 __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/ReadNameField/ |
| D | ReadNameField_harness.c | 61 __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, in harness()
63 __CPROVER_assert( NAME_SIZE < CBMC_MAX_OBJECT_SIZE, in harness()
78 __CPROVER_assume( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE ); in harness()
79 __CPROVER_assume( uxDestLen < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/SkipNameField/ |
| D | SkipNameField_harness.c | 37 __CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE, in harness()
45 __CPROVER_assume( uxLength < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/stubs/ |
| D | freertos_api.c | 153 < CBMC_MAX_OBJECT_SIZE ); in FreeRTOS_recvfrom()
219 __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); in FreeRTOS_GetUDPPayloadBuffer()
256 xRequestedSizeBytes + ipBUFFER_PADDING < CBMC_MAX_OBJECT_SIZE, in pxGetNetworkBufferWithDescriptor()
298 __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE ); in pxGetNetworkBufferWithDescriptor()
|
| D | cbmc.c | 10 __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "safeMalloc size too big" ); in safeMalloc()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptions/ |
| D | CheckOptions_harness.c | 49 __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, in __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions()
94 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptionsOuter/ |
| D | CheckOptionsOuter_harness.c | 49 __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, in __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption()
84 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/include/ |
| D | cbmc.h | 28 #define CBMC_MAX_OBJECT_SIZE ( 0xFFFFFFFF >> ( CBMC_BITS + 1 ) ) macro
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptionsInner/ |
| D | CheckOptionsInner_harness.c | 90 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/Socket/vSocketClose/ |
| D | vSocketClose_harness.c | 37 __CPROVER_assume( xRequestedSizeBytes < ( CBMC_MAX_OBJECT_SIZE - ipBUFFER_PADDING ) ); in harness()
|
| /FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/DNS/DNSgetHostByName/ |
| D | DNSgetHostByName_harness.c | 107 __CPROVER_assume( len < CBMC_MAX_OBJECT_SIZE ); in DNS_ReadReply()
|
