           *******************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

           *******************************************************


                   function Parser_Utilities.convertIpv6




For path(s) from start to run-time check associated with statement of line 857:

function_convertipv6_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    begidx >= rr_type__linelengthindex__first .
C2:    begidx <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 858:

function_convertipv6_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

For path(s) from start to run-time check associated with statement of line 859:

function_convertipv6_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
        ->
C1:    0 >= unsigned_types__unsigned16__first .
C2:    0 <= unsigned_types__unsigned16__last .
 

For path(s) from start to run-time check associated with statement of line 860:

function_convertipv6_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

For path(s) from start to assertion of line 863:

function_convertipv6_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   begidx < endidx .
H21:   0 <= req_num_separators .
H22:   0 <= max_digits_in_field .
        ->
C1:    begidx < endidx .
C2:    0 <= req_num_separators .
C3:    0 <= max_digits_in_field .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C5:    begidx >= rr_type__linelengthindex__first .
C6:    begidx <= rr_type__linelengthindex__last .
C7:    endidx >= rr_type__linelengthindex__first .
C8:    endidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to assertion of line 863:

function_convertipv6_6.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   ctr + 1 < endidx .
H40:   numseparators <= req_num_separators .
H41:   numdigitsinfield + 1 <= max_digits_in_field .
        ->
C1:    ctr + 1 < endidx .
C2:    numseparators <= req_num_separators .
C3:    numdigitsinfield + 1 <= max_digits_in_field .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C5:    begidx >= rr_type__linelengthindex__first .
C6:    begidx <= rr_type__linelengthindex__last .
C7:    endidx >= rr_type__linelengthindex__first .
C8:    endidx <= rr_type__linelengthindex__last .
 

function_convertipv6_7.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   ctr + 1 < endidx .
H52:   numseparators <= req_num_separators .
H53:   numdigitsinfield + 1 <= max_digits_in_field .
        ->
C1:    ctr + 1 < endidx .
C2:    numseparators <= req_num_separators .
C3:    numdigitsinfield + 1 <= max_digits_in_field .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C5:    begidx >= rr_type__linelengthindex__first .
C6:    begidx <= rr_type__linelengthindex__last .
C7:    endidx >= rr_type__linelengthindex__first .
C8:    endidx <= rr_type__linelengthindex__last .
 

function_convertipv6_8.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   ctr + 1 < endidx .
H56:   numseparators + 1 <= req_num_separators .
H57:   0 <= max_digits_in_field .
        ->
C1:    ctr + 1 < endidx .
C2:    numseparators + 1 <= req_num_separators .
C3:    0 <= max_digits_in_field .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C5:    begidx >= rr_type__linelengthindex__first .
C6:    begidx <= rr_type__linelengthindex__last .
C7:    endidx >= rr_type__linelengthindex__first .
C8:    endidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 864:

function_convertipv6_9.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr]) >= character__first .
C2:    element(s, [ctr]) <= character__last .
C3:    ctr >= rr_type__linelengthindex__first .
C4:    ctr <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 865:

function_convertipv6_10.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    ctr >= rr_type__linelengthindex__first .
C4:    ctr <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 866:

function_convertipv6_11.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
        ->
C1:    numdigitsinfield + 1 >= natural__first .
C2:    numdigitsinfield + 1 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 867:

function_convertipv6_12.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr]) >= character__first .
C2:    element(s, [ctr]) <= character__last .
C3:    ctr >= rr_type__linelengthindex__first .
C4:    ctr <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 868:

function_convertipv6_13.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
        ->
C1:    element(s, [ctr]) >= character__first .
C2:    element(s, [ctr]) <= character__last .
C3:    ctr >= rr_type__linelengthindex__first .
C4:    ctr <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 868:

function_convertipv6_14.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
        ->
C1:    ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 869:

function_convertipv6_15.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
        ->
C1:    numdigitsinfield + 1 >= natural__first .
C2:    numdigitsinfield + 1 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 871:

function_convertipv6_16.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
        ->
C1:    numseparators + 1 >= natural__first .
C2:    numseparators + 1 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 872:

function_convertipv6_17.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    ctr >= rr_type__linelengthindex__first .
C2:    ctr <= rr_type__linelengthindex__last .
C3:    numseparators + 1 >= separatorindextype__first .
C4:    numseparators + 1 <= separatorindextype__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 873:

function_convertipv6_18.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
        ->
C1:    fieldtotal >= unsigned_types__unsigned16__first .
C2:    fieldtotal <= unsigned_types__unsigned16__last .
C3:    numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 874:

function_convertipv6_19.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
        ->
C1:    0 >= unsigned_types__unsigned16__first .
C2:    0 <= unsigned_types__unsigned16__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 875:

function_convertipv6_20.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 877:

function_convertipv6_21.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    ctr + 1 >= rr_type__linelengthindex__first .
C2:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_22.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    ctr + 1 >= rr_type__linelengthindex__first .
C2:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_23.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
        ->
C1:    ctr + 1 >= rr_type__linelengthindex__first .
C2:    ctr + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 881:

function_convertipv6_24.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [begidx]) >= character__first .
C2:    element(s, [begidx]) <= character__last .
C3:    begidx >= rr_type__linelengthindex__first .
C4:    begidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 881:

function_convertipv6_25.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_26.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_27.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 882:

function_convertipv6_28.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   ada__characters__handling__is_decimal_digit(element(
           s, [begidx])) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   0 >= unsigned_types__unsigned16__first .
H38:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    begidx >= rr_type__linelengthindex__first .
C4:    begidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 882:

function_convertipv6_29.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H57:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_30.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H69:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_31.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   0 >= unsigned_types__unsigned16__first .
H73:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 883:

function_convertipv6_32.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   ada__characters__handling__is_decimal_digit(element(
           s, [begidx])) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   0 >= unsigned_types__unsigned16__first .
H38:   0 <= unsigned_types__unsigned16__last .
H39:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H40:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
        ->
C1:    0 + 1 >= natural__first .
C2:    0 + 1 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 883:

function_convertipv6_33.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H57:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H58:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H59:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H60:   ctr + 1 >= rr_type__linelengthindex__first .
H61:   ctr + 1 <= rr_type__linelengthindex__last .
H62:   numdigitsinfield + 1 >= natural__first .
H63:   numdigitsinfield + 1 <= natural__last .
        ->
C1:    numdigitsinfield + 1 + 1 >= natural__first .
C2:    numdigitsinfield + 1 + 1 <= natural__last .
 

function_convertipv6_34.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H69:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H70:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H71:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H72:   ctr + 1 >= rr_type__linelengthindex__first .
H73:   ctr + 1 <= rr_type__linelengthindex__last .
H74:   numdigitsinfield + 1 >= natural__first .
H75:   numdigitsinfield + 1 <= natural__last .
        ->
C1:    numdigitsinfield + 1 + 1 >= natural__first .
C2:    numdigitsinfield + 1 + 1 <= natural__last .
 

function_convertipv6_35.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   0 >= unsigned_types__unsigned16__first .
H73:   0 <= unsigned_types__unsigned16__last .
H74:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H75:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H76:   ctr + 1 >= rr_type__linelengthindex__first .
H77:   ctr + 1 <= rr_type__linelengthindex__last .
H78:   0 >= natural__first .
H79:   0 <= natural__last .
        ->
C1:    0 + 1 >= natural__first .
C2:    0 + 1 <= natural__last .
 

For path(s) from start to run-time check associated with statement of line 884:

function_convertipv6_36.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   ada__characters__handling__is_decimal_digit(element(
           s, [begidx])) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   0 >= unsigned_types__unsigned16__first .
H38:   0 <= unsigned_types__unsigned16__last .
H39:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H40:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   0 + 1 >= natural__first .
H46:   0 + 1 <= natural__last .
H47:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H48:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [begidx]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    0 + 1 >= rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    0 + 1 <= rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    0 + 1 >= integer__base__first .
C6:    0 + 1 <= integer__base__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 884:

function_convertipv6_37.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H57:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H58:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H59:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H60:   ctr + 1 >= rr_type__linelengthindex__first .
H61:   ctr + 1 <= rr_type__linelengthindex__last .
H62:   numdigitsinfield + 1 >= natural__first .
H63:   numdigitsinfield + 1 <= natural__last .
H64:   numdigitsinfield + 1 + 1 >= natural__first .
H65:   numdigitsinfield + 1 + 1 <= natural__last .
H66:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H67:   (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 >= integer__base__first .
C6:    numseparators + 1 <= integer__base__last .
 

function_convertipv6_38.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H69:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H70:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H71:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H72:   ctr + 1 >= rr_type__linelengthindex__first .
H73:   ctr + 1 <= rr_type__linelengthindex__last .
H74:   numdigitsinfield + 1 >= natural__first .
H75:   numdigitsinfield + 1 <= natural__last .
H76:   numdigitsinfield + 1 + 1 >= natural__first .
H77:   numdigitsinfield + 1 + 1 <= natural__last .
H78:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H79:   (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 >= integer__base__first .
C6:    numseparators + 1 <= integer__base__last .
 

function_convertipv6_39.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1])) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   0 >= unsigned_types__unsigned16__first .
H73:   0 <= unsigned_types__unsigned16__last .
H74:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H75:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H76:   ctr + 1 >= rr_type__linelengthindex__first .
H77:   ctr + 1 <= rr_type__linelengthindex__last .
H78:   0 >= natural__first .
H79:   0 <= natural__last .
H80:   0 + 1 >= natural__first .
H81:   0 + 1 <= natural__last .
H82:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H83:   (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (element(
           s, [ctr + 1]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 + 1 >= integer__base__first .
C6:    numseparators + 1 + 1 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 885:

function_convertipv6_40.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [begidx]) >= character__first .
C2:    element(s, [begidx]) <= character__last .
C3:    begidx >= rr_type__linelengthindex__first .
C4:    begidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 885:

function_convertipv6_41.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_42.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_43.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 886:

function_convertipv6_44.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   element(s, [begidx]) >= character__first .
H38:   element(s, [begidx]) <= character__last .
H39:   begidx >= rr_type__linelengthindex__first .
H40:   begidx <= rr_type__linelengthindex__last .
H41:   true .
H42:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [begidx])) .
H43:   begidx >= rr_type__linelengthindex__first .
H44:   begidx <= rr_type__linelengthindex__last .
H45:   0 >= unsigned_types__unsigned16__first .
H46:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    element(s, [begidx]) >= character__first .
C2:    element(s, [begidx]) <= character__last .
C3:    begidx >= rr_type__linelengthindex__first .
C4:    begidx <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 886:

function_convertipv6_45.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   element(s, [ctr + 1]) >= character__first .
H57:   element(s, [ctr + 1]) <= character__last .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   true .
H61:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H65:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_46.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   element(s, [ctr + 1]) >= character__first .
H69:   element(s, [ctr + 1]) <= character__last .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   true .
H73:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H77:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

function_convertipv6_47.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   element(s, [ctr + 1]) >= character__first .
H73:   element(s, [ctr + 1]) <= character__last .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   true .
H77:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H78:   ctr + 1 >= rr_type__linelengthindex__first .
H79:   ctr + 1 <= rr_type__linelengthindex__last .
H80:   0 >= unsigned_types__unsigned16__first .
H81:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    element(s, [ctr + 1]) >= character__first .
C2:    element(s, [ctr + 1]) <= character__last .
C3:    ctr + 1 >= rr_type__linelengthindex__first .
C4:    ctr + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 886:

function_convertipv6_48.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   element(s, [begidx]) >= character__first .
H38:   element(s, [begidx]) <= character__last .
H39:   begidx >= rr_type__linelengthindex__first .
H40:   begidx <= rr_type__linelengthindex__last .
H41:   true .
H42:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [begidx])) .
H43:   begidx >= rr_type__linelengthindex__first .
H44:   begidx <= rr_type__linelengthindex__last .
H45:   0 >= unsigned_types__unsigned16__first .
H46:   0 <= unsigned_types__unsigned16__last .
H47:   element(s, [begidx]) >= character__first .
H48:   element(s, [begidx]) <= character__last .
H49:   begidx >= rr_type__linelengthindex__first .
H50:   begidx <= rr_type__linelengthindex__last .
H51:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H52:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
        ->
C1:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 886:

function_convertipv6_49.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   element(s, [ctr + 1]) >= character__first .
H57:   element(s, [ctr + 1]) <= character__last .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   true .
H61:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H65:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H66:   element(s, [ctr + 1]) >= character__first .
H67:   element(s, [ctr + 1]) <= character__last .
H68:   ctr + 1 >= rr_type__linelengthindex__first .
H69:   ctr + 1 <= rr_type__linelengthindex__last .
H70:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H71:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
        ->
C1:    ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
 

function_convertipv6_50.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   element(s, [ctr + 1]) >= character__first .
H69:   element(s, [ctr + 1]) <= character__last .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   true .
H73:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H77:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H78:   element(s, [ctr + 1]) >= character__first .
H79:   element(s, [ctr + 1]) <= character__last .
H80:   ctr + 1 >= rr_type__linelengthindex__first .
H81:   ctr + 1 <= rr_type__linelengthindex__last .
H82:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H83:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
        ->
C1:    ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
 

function_convertipv6_51.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   element(s, [ctr + 1]) >= character__first .
H73:   element(s, [ctr + 1]) <= character__last .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   true .
H77:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H78:   ctr + 1 >= rr_type__linelengthindex__first .
H79:   ctr + 1 <= rr_type__linelengthindex__last .
H80:   0 >= unsigned_types__unsigned16__first .
H81:   0 <= unsigned_types__unsigned16__last .
H82:   element(s, [ctr + 1]) >= character__first .
H83:   element(s, [ctr + 1]) <= character__last .
H84:   ctr + 1 >= rr_type__linelengthindex__first .
H85:   ctr + 1 <= rr_type__linelengthindex__last .
H86:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H87:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
        ->
C1:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
 

For path(s) from start to run-time check associated with statement of line 887:

function_convertipv6_52.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   element(s, [begidx]) >= character__first .
H38:   element(s, [begidx]) <= character__last .
H39:   begidx >= rr_type__linelengthindex__first .
H40:   begidx <= rr_type__linelengthindex__last .
H41:   true .
H42:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [begidx])) .
H43:   begidx >= rr_type__linelengthindex__first .
H44:   begidx <= rr_type__linelengthindex__last .
H45:   0 >= unsigned_types__unsigned16__first .
H46:   0 <= unsigned_types__unsigned16__last .
H47:   element(s, [begidx]) >= character__first .
H48:   element(s, [begidx]) <= character__last .
H49:   begidx >= rr_type__linelengthindex__first .
H50:   begidx <= rr_type__linelengthindex__last .
H51:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H52:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H53:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H54:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H55:   0 >= natural__first .
H56:   0 <= natural__last .
        ->
C1:    0 + 1 >= natural__first .
C2:    0 + 1 <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 887:

function_convertipv6_53.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   element(s, [ctr + 1]) >= character__first .
H57:   element(s, [ctr + 1]) <= character__last .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   true .
H61:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H65:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H66:   element(s, [ctr + 1]) >= character__first .
H67:   element(s, [ctr + 1]) <= character__last .
H68:   ctr + 1 >= rr_type__linelengthindex__first .
H69:   ctr + 1 <= rr_type__linelengthindex__last .
H70:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H71:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H72:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H73:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H74:   numdigitsinfield + 1 >= natural__first .
H75:   numdigitsinfield + 1 <= natural__last .
        ->
C1:    numdigitsinfield + 1 + 1 >= natural__first .
C2:    numdigitsinfield + 1 + 1 <= natural__last .
 

function_convertipv6_54.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   element(s, [ctr + 1]) >= character__first .
H69:   element(s, [ctr + 1]) <= character__last .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   true .
H73:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H77:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H78:   element(s, [ctr + 1]) >= character__first .
H79:   element(s, [ctr + 1]) <= character__last .
H80:   ctr + 1 >= rr_type__linelengthindex__first .
H81:   ctr + 1 <= rr_type__linelengthindex__last .
H82:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H83:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H84:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H85:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H86:   numdigitsinfield + 1 >= natural__first .
H87:   numdigitsinfield + 1 <= natural__last .
        ->
C1:    numdigitsinfield + 1 + 1 >= natural__first .
C2:    numdigitsinfield + 1 + 1 <= natural__last .
 

function_convertipv6_55.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   element(s, [ctr + 1]) >= character__first .
H73:   element(s, [ctr + 1]) <= character__last .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   true .
H77:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H78:   ctr + 1 >= rr_type__linelengthindex__first .
H79:   ctr + 1 <= rr_type__linelengthindex__last .
H80:   0 >= unsigned_types__unsigned16__first .
H81:   0 <= unsigned_types__unsigned16__last .
H82:   element(s, [ctr + 1]) >= character__first .
H83:   element(s, [ctr + 1]) <= character__last .
H84:   ctr + 1 >= rr_type__linelengthindex__first .
H85:   ctr + 1 <= rr_type__linelengthindex__last .
H86:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H87:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H88:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H89:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H90:   0 >= natural__first .
H91:   0 <= natural__last .
        ->
C1:    0 + 1 >= natural__first .
C2:    0 + 1 <= natural__last .
 

For path(s) from start to run-time check associated with statement of line 888:

function_convertipv6_56.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   element(s, [begidx]) >= character__first .
H38:   element(s, [begidx]) <= character__last .
H39:   begidx >= rr_type__linelengthindex__first .
H40:   begidx <= rr_type__linelengthindex__last .
H41:   true .
H42:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [begidx])) .
H43:   begidx >= rr_type__linelengthindex__first .
H44:   begidx <= rr_type__linelengthindex__last .
H45:   0 >= unsigned_types__unsigned16__first .
H46:   0 <= unsigned_types__unsigned16__last .
H47:   element(s, [begidx]) >= character__first .
H48:   element(s, [begidx]) <= character__last .
H49:   begidx >= rr_type__linelengthindex__first .
H50:   begidx <= rr_type__linelengthindex__last .
H51:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H52:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H53:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H54:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H55:   0 >= natural__first .
H56:   0 <= natural__last .
H57:   0 + 1 >= natural__first .
H58:   0 + 1 <= natural__last .
H59:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H60:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           begidx])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    0 + 1 >= rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    0 + 1 <= rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    0 + 1 >= integer__base__first .
C6:    0 + 1 <= integer__base__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 888:

function_convertipv6_57.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   element(s, [ctr + 1]) >= character__first .
H57:   element(s, [ctr + 1]) <= character__last .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   true .
H61:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H65:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H66:   element(s, [ctr + 1]) >= character__first .
H67:   element(s, [ctr + 1]) <= character__last .
H68:   ctr + 1 >= rr_type__linelengthindex__first .
H69:   ctr + 1 <= rr_type__linelengthindex__last .
H70:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H71:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H72:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H73:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H74:   numdigitsinfield + 1 >= natural__first .
H75:   numdigitsinfield + 1 <= natural__last .
H76:   numdigitsinfield + 1 + 1 >= natural__first .
H77:   numdigitsinfield + 1 + 1 <= natural__last .
H78:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H79:   ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 >= integer__base__first .
C6:    numseparators + 1 <= integer__base__last .
 

function_convertipv6_58.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   element(s, [ctr + 1]) >= character__first .
H69:   element(s, [ctr + 1]) <= character__last .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   true .
H73:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H77:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H78:   element(s, [ctr + 1]) >= character__first .
H79:   element(s, [ctr + 1]) <= character__last .
H80:   ctr + 1 >= rr_type__linelengthindex__first .
H81:   ctr + 1 <= rr_type__linelengthindex__last .
H82:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H83:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H84:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H85:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H86:   numdigitsinfield + 1 >= natural__first .
H87:   numdigitsinfield + 1 <= natural__last .
H88:   numdigitsinfield + 1 + 1 >= natural__first .
H89:   numdigitsinfield + 1 + 1 <= natural__last .
H90:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H91:   ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * (((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 >= integer__base__first .
C6:    numseparators + 1 <= integer__base__last .
 

function_convertipv6_59.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   element(s, [ctr + 1]) >= character__first .
H73:   element(s, [ctr + 1]) <= character__last .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   true .
H77:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1])) .
H78:   ctr + 1 >= rr_type__linelengthindex__first .
H79:   ctr + 1 <= rr_type__linelengthindex__last .
H80:   0 >= unsigned_types__unsigned16__first .
H81:   0 <= unsigned_types__unsigned16__last .
H82:   element(s, [ctr + 1]) >= character__first .
H83:   element(s, [ctr + 1]) <= character__last .
H84:   ctr + 1 >= rr_type__linelengthindex__first .
H85:   ctr + 1 <= rr_type__linelengthindex__last .
H86:   ada__characters__handling__to_upper(element(s, [ctr + 1])) >= 
           character__first .
H87:   ada__characters__handling__to_upper(element(s, [ctr + 1])) <= 
           character__last .
H88:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H89:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H90:   0 >= natural__first .
H91:   0 <= natural__last .
H92:   0 + 1 >= natural__first .
H93:   0 + 1 <= natural__last .
H94:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H95:   ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
        ->
C1:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    ((ipv6_radix * 0 mod unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr + 1])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    numseparators + 1 + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C4:    numseparators + 1 + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C5:    numseparators + 1 + 1 >= integer__base__first .
C6:    numseparators + 1 + 1 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 890:

function_convertipv6_60.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    0 >= natural__first .
H9:    0 <= natural__last .
H10:   0 >= unsigned_types__unsigned16__first .
H11:   0 <= unsigned_types__unsigned16__last .
H12:   0 >= natural__first .
H13:   0 <= natural__last .
H14:   begidx >= rr_type__linelengthindex__first .
H15:   begidx <= rr_type__linelengthindex__last .
H16:   0 >= natural__first .
H17:   0 <= natural__last .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not ((begidx < endidx) and ((0 <= req_num_separators) and (0 <= 
           max_digits_in_field))) .
H21:   begidx >= rr_type__linelengthindex__first .
H22:   begidx <= rr_type__linelengthindex__last .
H23:   0 >= natural__first .
H24:   0 <= natural__last .
H25:   begidx = endidx .
H26:   0 <= req_num_separators .
H27:   begidx >= rr_type__linelengthindex__first .
H28:   begidx <= rr_type__linelengthindex__last .
H29:   element(s, [begidx]) >= character__first .
H30:   element(s, [begidx]) <= character__last .
H31:   begidx >= rr_type__linelengthindex__first .
H32:   begidx <= rr_type__linelengthindex__last .
H33:   true .
H34:   not (ada__characters__handling__is_decimal_digit(element(
           s, [begidx]))) .
H35:   begidx >= rr_type__linelengthindex__first .
H36:   begidx <= rr_type__linelengthindex__last .
H37:   element(s, [begidx]) >= character__first .
H38:   element(s, [begidx]) <= character__last .
H39:   begidx >= rr_type__linelengthindex__first .
H40:   begidx <= rr_type__linelengthindex__last .
H41:   true .
H42:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [begidx]))) .
        ->
C1:    num_fields >= natural__first .
C2:    num_fields <= natural__last .
 

For path(s) from assertion of line 863 to run-time check associated with statement of line 890:

function_convertipv6_61.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   ada__characters__handling__is_decimal_digit(element(
           s, [ctr])) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   fieldtotal >= unsigned_types__unsigned16__first .
H20:   fieldtotal <= unsigned_types__unsigned16__last .
H21:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H22:   (ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (element(s, [
           ctr]) - 48) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H23:   ctr >= rr_type__linelengthindex__first .
H24:   ctr <= rr_type__linelengthindex__last .
H25:   numdigitsinfield >= natural__first .
H26:   numdigitsinfield <= natural__last .
H27:   numdigitsinfield + 1 >= natural__first .
H28:   numdigitsinfield + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr + 1 >= rr_type__linelengthindex__first .
H32:   ctr + 1 <= rr_type__linelengthindex__last .
H33:   ctr + 1 >= rr_type__linelengthindex__first .
H34:   ctr + 1 <= rr_type__linelengthindex__last .
H35:   numseparators >= natural__first .
H36:   numseparators <= natural__last .
H37:   numdigitsinfield + 1 >= natural__first .
H38:   numdigitsinfield + 1 <= natural__last .
H39:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H40:   ctr + 1 >= rr_type__linelengthindex__first .
H41:   ctr + 1 <= rr_type__linelengthindex__last .
H42:   numseparators >= natural__first .
H43:   numseparators <= natural__last .
H44:   ctr + 1 = endidx .
H45:   numseparators <= req_num_separators .
H46:   ctr + 1 >= rr_type__linelengthindex__first .
H47:   ctr + 1 <= rr_type__linelengthindex__last .
H48:   element(s, [ctr + 1]) >= character__first .
H49:   element(s, [ctr + 1]) <= character__last .
H50:   ctr + 1 >= rr_type__linelengthindex__first .
H51:   ctr + 1 <= rr_type__linelengthindex__last .
H52:   true .
H53:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H54:   ctr + 1 >= rr_type__linelengthindex__first .
H55:   ctr + 1 <= rr_type__linelengthindex__last .
H56:   element(s, [ctr + 1]) >= character__first .
H57:   element(s, [ctr + 1]) <= character__last .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   true .
H61:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1]))) .
        ->
C1:    num_fields >= natural__first .
C2:    num_fields <= natural__last .
 

function_convertipv6_62.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr])) .
H25:   ctr >= rr_type__linelengthindex__first .
H26:   ctr <= rr_type__linelengthindex__last .
H27:   fieldtotal >= unsigned_types__unsigned16__first .
H28:   fieldtotal <= unsigned_types__unsigned16__last .
H29:   element(s, [ctr]) >= character__first .
H30:   element(s, [ctr]) <= character__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   ada__characters__handling__to_upper(element(s, [ctr])) >= 
           character__first .
H34:   ada__characters__handling__to_upper(element(s, [ctr])) <= 
           character__last .
H35:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   ((ipv6_radix * fieldtotal mod 
           unsigned_types__unsigned16__modulus + (
           ada__characters__handling__to_upper(element(s, [
           ctr])) - 65) mod unsigned_types__unsigned16__modulus) mod 
           unsigned_types__unsigned16__modulus + 10) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   numdigitsinfield >= natural__first .
H38:   numdigitsinfield <= natural__last .
H39:   numdigitsinfield + 1 >= natural__first .
H40:   numdigitsinfield + 1 <= natural__last .
H41:   ctr >= rr_type__linelengthindex__first .
H42:   ctr <= rr_type__linelengthindex__last .
H43:   ctr + 1 >= rr_type__linelengthindex__first .
H44:   ctr + 1 <= rr_type__linelengthindex__last .
H45:   ctr + 1 >= rr_type__linelengthindex__first .
H46:   ctr + 1 <= rr_type__linelengthindex__last .
H47:   numseparators >= natural__first .
H48:   numseparators <= natural__last .
H49:   numdigitsinfield + 1 >= natural__first .
H50:   numdigitsinfield + 1 <= natural__last .
H51:   not ((ctr + 1 < endidx) and ((numseparators <= 
           req_num_separators) and (numdigitsinfield + 1 <= 
           max_digits_in_field))) .
H52:   ctr + 1 >= rr_type__linelengthindex__first .
H53:   ctr + 1 <= rr_type__linelengthindex__last .
H54:   numseparators >= natural__first .
H55:   numseparators <= natural__last .
H56:   ctr + 1 = endidx .
H57:   numseparators <= req_num_separators .
H58:   ctr + 1 >= rr_type__linelengthindex__first .
H59:   ctr + 1 <= rr_type__linelengthindex__last .
H60:   element(s, [ctr + 1]) >= character__first .
H61:   element(s, [ctr + 1]) <= character__last .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   true .
H65:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   element(s, [ctr + 1]) >= character__first .
H69:   element(s, [ctr + 1]) <= character__last .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   true .
H73:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1]))) .
        ->
C1:    num_fields >= natural__first .
C2:    num_fields <= natural__last .
 

function_convertipv6_63.
H1:    ctr < endidx .
H2:    numseparators <= req_num_separators .
H3:    numdigitsinfield <= max_digits_in_field .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    ctr >= rr_type__linelengthindex__first .
H10:   ctr <= rr_type__linelengthindex__last .
H11:   element(s, [ctr]) >= character__first .
H12:   element(s, [ctr]) <= character__last .
H13:   ctr >= rr_type__linelengthindex__first .
H14:   ctr <= rr_type__linelengthindex__last .
H15:   true .
H16:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr]))) .
H17:   ctr >= rr_type__linelengthindex__first .
H18:   ctr <= rr_type__linelengthindex__last .
H19:   element(s, [ctr]) >= character__first .
H20:   element(s, [ctr]) <= character__last .
H21:   ctr >= rr_type__linelengthindex__first .
H22:   ctr <= rr_type__linelengthindex__last .
H23:   true .
H24:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr]))) .
H25:   numseparators >= natural__first .
H26:   numseparators <= natural__last .
H27:   numseparators + 1 >= natural__first .
H28:   numseparators + 1 <= natural__last .
H29:   ctr >= rr_type__linelengthindex__first .
H30:   ctr <= rr_type__linelengthindex__last .
H31:   ctr >= rr_type__linelengthindex__first .
H32:   ctr <= rr_type__linelengthindex__last .
H33:   numseparators + 1 >= separatorindextype__first .
H34:   numseparators + 1 <= separatorindextype__last .
H35:   fieldtotal >= unsigned_types__unsigned16__first .
H36:   fieldtotal <= unsigned_types__unsigned16__last .
H37:   fieldtotal >= unsigned_types__unsigned16__first .
H38:   fieldtotal <= unsigned_types__unsigned16__last .
H39:   numseparators + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H40:   numseparators + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H41:   0 >= unsigned_types__unsigned16__first .
H42:   0 <= unsigned_types__unsigned16__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   ctr >= rr_type__linelengthindex__first .
H46:   ctr <= rr_type__linelengthindex__last .
H47:   ctr + 1 >= rr_type__linelengthindex__first .
H48:   ctr + 1 <= rr_type__linelengthindex__last .
H49:   ctr + 1 >= rr_type__linelengthindex__first .
H50:   ctr + 1 <= rr_type__linelengthindex__last .
H51:   numseparators + 1 >= natural__first .
H52:   numseparators + 1 <= natural__last .
H53:   0 >= natural__first .
H54:   0 <= natural__last .
H55:   not ((ctr + 1 < endidx) and ((numseparators + 1 <= 
           req_num_separators) and (0 <= 
           max_digits_in_field))) .
H56:   ctr + 1 >= rr_type__linelengthindex__first .
H57:   ctr + 1 <= rr_type__linelengthindex__last .
H58:   numseparators + 1 >= natural__first .
H59:   numseparators + 1 <= natural__last .
H60:   ctr + 1 = endidx .
H61:   numseparators + 1 <= req_num_separators .
H62:   ctr + 1 >= rr_type__linelengthindex__first .
H63:   ctr + 1 <= rr_type__linelengthindex__last .
H64:   element(s, [ctr + 1]) >= character__first .
H65:   element(s, [ctr + 1]) <= character__last .
H66:   ctr + 1 >= rr_type__linelengthindex__first .
H67:   ctr + 1 <= rr_type__linelengthindex__last .
H68:   true .
H69:   not (ada__characters__handling__is_decimal_digit(element(
           s, [ctr + 1]))) .
H70:   ctr + 1 >= rr_type__linelengthindex__first .
H71:   ctr + 1 <= rr_type__linelengthindex__last .
H72:   element(s, [ctr + 1]) >= character__first .
H73:   element(s, [ctr + 1]) <= character__last .
H74:   ctr + 1 >= rr_type__linelengthindex__first .
H75:   ctr + 1 <= rr_type__linelengthindex__last .
H76:   true .
H77:   not (ada__characters__handling__is_hexadecimal_digit(element(
           s, [ctr + 1]))) .
        ->
C1:    num_fields >= natural__first .
C2:    num_fields <= natural__last .
 

For path(s) from start to finish:

function_convertipv6_64.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_65.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_66.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_67.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_68.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_69.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_70.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_71.
*** true .          /* trivially true VC removed by Examiner */


For path(s) from assertion of line 863 to finish:

function_convertipv6_72.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_73.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_74.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_75.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_76.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_77.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_78.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_79.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_80.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_81.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_82.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_83.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_84.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_85.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_86.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_87.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_88.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_89.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_90.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_91.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_92.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_93.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_94.
*** true .          /* trivially true VC removed by Examiner */


function_convertipv6_95.
*** true .          /* trivially true VC removed by Examiner */


