Home
last modified time | relevance | path

Searched refs:buffer_size (Results 1 – 4 of 4) sorted by relevance

/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptions/
DCheckOptions_harness.c35 size_t buffer_size; variable
49 __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, in __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions()
51 __CPROVER_assert( 8 <= buffer_size, in __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions()
55 __CPROVER_assert( uxTotalLength <= buffer_size, in __CPROVER_file_local_FreeRTOS_TCP_IP_c_prvSingleStepTCPHeaderOptions()
77 buffer_size = buf_size; in harness()
85 pxNetworkBuffer.pucEthernetBuffer = malloc( buffer_size ); in harness()
87 pxNetworkBuffer.xDataLength = buffer_size; in harness()
94 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
97 __CPROVER_assume( buffer_size <= BUFFER_SIZE ); in harness()
100 __CPROVER_assume( buffer_size > 47 ); in harness()
/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptionsOuter/
DCheckOptionsOuter_harness.c38 size_t buffer_size; variable
49 __CPROVER_assert( buffer_size < CBMC_MAX_OBJECT_SIZE, in __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption()
51 __CPROVER_assert( uxIndex <= buffer_size, in __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption()
53 __CPROVER_assert( uxIndex + 8 <= buffer_size, in __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvReadSackOption()
72 buffer_size = buf_size; in harness()
74 uint8_t * pucPtr = malloc( buffer_size ); in harness()
84 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
87 __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */ in harness()
89 __CPROVER_assume( uxTotalLength <= buffer_size ); in harness()
/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/CheckOptionsInner/
DCheckOptionsInner_harness.c40 size_t buffer_size; in harness() local
41 uint8_t * pucPtr = malloc( buffer_size ); in harness()
90 __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE ); in harness()
94 __CPROVER_assume( uxIndex <= buffer_size ); in harness()
95 __CPROVER_assume( uxIndex + 8 <= buffer_size ); in harness()
/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/stubs/
Dfreertos_api.c167 uint32_t buffer_size = payload_size + sizeof( UDPPacket_t ); in FreeRTOS_recvfrom() local
168 uint8_t * buffer = safeMalloc( buffer_size ); in FreeRTOS_recvfrom()
172 buffer_size = 0; in FreeRTOS_recvfrom()
177 buffer_size = buffer_size - sizeof( UDPPacket_t ); in FreeRTOS_recvfrom()
181 return buffer_size; in FreeRTOS_recvfrom()