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

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


                  procedure Process_Dns_Request.Trim_Name




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

procedure_trim_name_1.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
        ->
C1:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
C2:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
C3:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
C4:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
C5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
C6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
C7:    rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C8:    rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
 

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

procedure_trim_name_2.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
        ->
C1:    32 >= character__first .
C2:    32 <= character__last .
 

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

procedure_trim_name_3.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H13:   32 >= character__first .
H14:   32 <= character__last .
        ->
C1:    qname_location >= dns_types__qname_ptr_range__first .
C2:    qname_location <= dns_types__qname_ptr_range__last .
 

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

procedure_trim_name_4.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H13:   32 >= character__first .
H14:   32 <= character__last .
H15:   qname_location >= dns_types__qname_ptr_range__first .
H16:   qname_location <= dns_types__qname_ptr_range__last .
H17:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H18:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H19:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 > 
           0 .
H20:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 < 
           rr_type__wirestringtypeindex__last .
H21:   qname_location >= dns_types__qname_ptr_range__first .
H22:   qname_location <= dns_types__qname_ptr_range__last .
H23:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H24:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
        ->
C1:    qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           dns_types__qname_ptr_range__first .
C2:    qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           dns_types__qname_ptr_range__last .
C3:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           dns_types__qname_ptr_range__first .
C4:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           dns_types__qname_ptr_range__last .
 

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

procedure_trim_name_5.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H13:   32 >= character__first .
H14:   32 <= character__last .
H15:   qname_location >= dns_types__qname_ptr_range__first .
H16:   qname_location <= dns_types__qname_ptr_range__last .
H17:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H18:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H19:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 > 
           0 .
H20:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 < 
           rr_type__wirestringtypeindex__last .
H21:   qname_location >= dns_types__qname_ptr_range__first .
H22:   qname_location <= dns_types__qname_ptr_range__last .
H23:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H24:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H25:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           dns_types__qname_ptr_range__first .
H26:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           dns_types__qname_ptr_range__last .
H27:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           dns_types__qname_ptr_range__first .
H28:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           dns_types__qname_ptr_range__last .
        ->
C1:    rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__first .
C2:    rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__last .
C3:    rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__base__first .
C4:    rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__base__last .
C5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
C6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
C7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
C8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
C9:    rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C10:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
C11:   1 >= integer__first .
C12:   1 <= integer__last .
 

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

procedure_trim_name_6.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H13:   32 >= character__first .
H14:   32 <= character__last .
H15:   qname_location >= dns_types__qname_ptr_range__first .
H16:   qname_location <= dns_types__qname_ptr_range__last .
H17:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H18:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H19:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 > 
           0 .
H20:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 < 
           rr_type__wirestringtypeindex__last .
H21:   qname_location >= dns_types__qname_ptr_range__first .
H22:   qname_location <= dns_types__qname_ptr_range__last .
H23:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H24:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H25:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           dns_types__qname_ptr_range__first .
H26:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           dns_types__qname_ptr_range__last .
H27:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           dns_types__qname_ptr_range__first .
H28:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           dns_types__qname_ptr_range__last .
H29:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__first .
H30:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__last .
H31:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__base__first .
H32:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__base__last .
H33:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H34:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H35:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H36:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H37:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H38:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H39:   1 >= integer__first .
H40:   1 <= integer__last .
        ->
C1:    (1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)) -> ((
           rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           rr_type__wirestringtypeindex__first) and (
           rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           rr_type__wirestringtypeindex__last)) .
C2:    (1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)) -> ((
           1 >= rr_type__wirestringtypeindex__first) and (1 <= 
           rr_type__wirestringtypeindex__last)) .
 

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

procedure_trim_name_7.
H1:    qname_location <= dns_types__packet_length_range__last .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H3:    qname_location >= dns_types__qname_ptr_range__first .
H4:    qname_location <= dns_types__qname_ptr_range__last .
H5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H13:   32 >= character__first .
H14:   32 <= character__last .
H15:   qname_location >= dns_types__qname_ptr_range__first .
H16:   qname_location <= dns_types__qname_ptr_range__last .
H17:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H18:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H19:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 > 
           0 .
H20:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 < 
           rr_type__wirestringtypeindex__last .
H21:   qname_location >= dns_types__qname_ptr_range__first .
H22:   qname_location <= dns_types__qname_ptr_range__last .
H23:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H24:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H25:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           dns_types__qname_ptr_range__first .
H26:   qname_location + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           dns_types__qname_ptr_range__last .
H27:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           dns_types__qname_ptr_range__first .
H28:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           dns_types__qname_ptr_range__last .
H29:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__first .
H30:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__last .
H31:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__base__first .
H32:   rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__base__last .
H33:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H34:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H35:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H36:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H37:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H38:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H39:   1 >= integer__first .
H40:   1 <= integer__last .
H41:   (1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)) -> ((
           rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) >= 
           rr_type__wirestringtypeindex__first) and (
           rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) <= 
           rr_type__wirestringtypeindex__last)) .
H42:   (1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)) -> ((
           1 >= rr_type__wirestringtypeindex__first) and (1 <= 
           rr_type__wirestringtypeindex__last)) .
H43:   1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) .
        ->
C1:    1 + (element(domainname, [rr_type__wirestringtypeindex__first]) + 
           1) <= rr_type__wirestringtypeindex__last .
C2:    1 >= 1 .
C3:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 = element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1 .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
C5:    qname_location >= dns_types__qname_ptr_range__first .
C6:    qname_location <= dns_types__qname_ptr_range__last .
C7:    qname_location <= dns_types__packet_length_range__last .
C8:    1 >= rr_type__wirestringtypeindex__first .
C9:    1 <= rr_type__wirestringtypeindex__last .
C10:   1 >= 1 .
C11:   1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) .
 

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

procedure_trim_name_8.
H1:    loop__1__i + zone_length <= 
           rr_type__wirestringtypeindex__last .
H2:    loop__1__i >= 1 .
H3:    zone_length = element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1 .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    qname_location <= dns_types__packet_length_range__last .
H8:    loop__1__i >= rr_type__wirestringtypeindex__first .
H9:    loop__1__i <= rr_type__wirestringtypeindex__last .
H10:   loop__1__i >= 1 .
H11:   loop__1__i <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) .
H12:   element(domainname, [loop__1__i + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)]) >= 
           character__first .
H13:   element(domainname, [loop__1__i + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)]) <= 
           character__last .
H14:   loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           rr_type__wirestringtypeindex__first .
H15:   loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           rr_type__wirestringtypeindex__last .
H16:   loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__base__first .
H17:   loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__base__last .
H18:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H19:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H20:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H21:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H22:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H23:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H24:   loop__1__i >= rr_type__wirestringtypeindex__first .
H25:   loop__1__i <= rr_type__wirestringtypeindex__last .
H26:   not (loop__1__i = rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)) .
        ->
C1:    loop__1__i + 1 + zone_length <= 
           rr_type__wirestringtypeindex__last .
C2:    loop__1__i + 1 >= 1 .
C3:    zone_length = element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1 .
C4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
C5:    qname_location >= dns_types__qname_ptr_range__first .
C6:    qname_location <= dns_types__qname_ptr_range__last .
C7:    qname_location <= dns_types__packet_length_range__last .
C8:    loop__1__i + 1 >= rr_type__wirestringtypeindex__first .
C9:    loop__1__i + 1 <= rr_type__wirestringtypeindex__last .
C10:   loop__1__i + 1 >= 1 .
C11:   loop__1__i + 1 <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) .
 

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

procedure_trim_name_9.
H1:    loop__1__i + zone_length <= 
           rr_type__wirestringtypeindex__last .
H2:    loop__1__i >= 1 .
H3:    zone_length = element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1 .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    qname_location <= dns_types__packet_length_range__last .
H8:    loop__1__i >= rr_type__wirestringtypeindex__first .
H9:    loop__1__i <= rr_type__wirestringtypeindex__last .
H10:   loop__1__i >= 1 .
H11:   loop__1__i <= rr_type__wirestringtypeindex__last - (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) .
        ->
C1:    element(domainname, [loop__1__i + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)]) >= 
           character__first .
C2:    element(domainname, [loop__1__i + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1)]) <= 
           character__last .
C3:    loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           rr_type__wirestringtypeindex__first .
C4:    loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           rr_type__wirestringtypeindex__last .
C5:    loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           integer__base__first .
C6:    loop__1__i + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           integer__base__last .
C7:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
C8:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
C9:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
C10:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
C11:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C12:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
C13:   loop__1__i >= rr_type__wirestringtypeindex__first .
C14:   loop__1__i <= rr_type__wirestringtypeindex__last .
 

For path(s) from start to finish:

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


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


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

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


