Searched refs:uxDestLen (Results 1 – 4 of 4) sorted by relevance
30 size_t uxDestLen );47 size_t uxDestLen ) in DNS_ReadNameField() argument71 size_t uxDestLen; in harness() local74 char * pcName = malloc( uxDestLen ); in harness()79 __CPROVER_assume( uxDestLen < CBMC_MAX_OBJECT_SIZE ); in harness()82 __CPROVER_assume( uxDestLen <= NAME_SIZE ); in harness()91 __CPROVER_assume( uxDestLen > 0 ); in harness()96 uxDestLen ); in harness()100 __CPROVER_assert( index <= uxDestLen + 1 && index <= uxRemainingBytes, in harness()
39 size_t uxDestLen ) in DNS_ReadNameField() argument52 __CPROVER_assert( uxDestLen < CBMC_MAX_OBJECT_SIZE, in DNS_ReadNameField()70 __CPROVER_assert( uxDestLen > 0, in DNS_ReadNameField()77 __CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes ); in DNS_ReadNameField()
50 size_t uxDestLen );
65 size_t uxDestLen ) in DNS_ReadNameField() argument104 if( uxNameLen >= uxDestLen ) in DNS_ReadNameField()127 if( uxNameLen >= uxDestLen ) in DNS_ReadNameField()152 if( ( uxNameLen < uxDestLen ) && ( uxIndex < uxSourceLen ) ) in DNS_ReadNameField()
