Searched refs:uxRemainingBytes (Results 1 – 4 of 4) sorted by relevance
28 size_t uxRemainingBytes,45 size_t uxRemainingBytes, in DNS_ReadNameField() argument70 size_t uxRemainingBytes; in harness() local73 uint8_t * pucByte = malloc( uxRemainingBytes ); in harness()78 __CPROVER_assume( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE ); in harness()81 __CPROVER_assume( uxRemainingBytes <= NETWORK_BUFFER_SIZE ); in harness()94 uxRemainingBytes, in harness()100 __CPROVER_assert( index <= uxDestLen + 1 && index <= uxRemainingBytes, in harness()
37 size_t uxRemainingBytes, in DNS_ReadNameField() argument50 __CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()55 __CPROVER_assert( uxRemainingBytes <= NETWORK_BUFFER_SIZE, in DNS_ReadNameField()77 __CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes ); in DNS_ReadNameField()
48 size_t uxRemainingBytes,
63 size_t uxRemainingBytes, in DNS_ReadNameField() argument69 size_t uxSourceLen = uxRemainingBytes; in DNS_ReadNameField()