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

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


             procedure Process_Dns_Request.Set_TTL_Data_AAAA_IP




For path(s) from start to precondition check associated with statement of line 393:

procedure_set_ttl_data_aaaa_ip_1.
H1:    start_byte <= dns_types__packet_bytes_range__last - 22 .
H2:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
H9:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
        ->
C1:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
C2:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
C3:    start_byte >= dns_types__packet_bytes_range__first .
C4:    start_byte <= dns_types__packet_bytes_range__last .
C5:    start_byte <= dns_types__packet_bytes_range__last - 3 .
 

For path(s) from start to precondition check associated with statement of line 395:

procedure_set_ttl_data_aaaa_ip_2.
H1:    start_byte <= dns_types__packet_bytes_range__last - 22 .
H2:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
H9:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
H10:   fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H11:   fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H12:   start_byte >= dns_types__packet_bytes_range__first .
H13:   start_byte <= dns_types__packet_bytes_range__last .
H14:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H15:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
        ->
C1:    16 >= unsigned_types__unsigned16__first .
C2:    16 <= unsigned_types__unsigned16__last .
C3:    start_byte + 4 >= dns_types__packet_bytes_range__first .
C4:    start_byte + 4 <= dns_types__packet_bytes_range__last .
C5:    start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
C6:    start_byte + 4 >= dns_types__packet_bytes_range__base__first .
C7:    start_byte + 4 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_set_ttl_data_aaaa_ip_3.
H1:    start_byte <= dns_types__packet_bytes_range__last - 22 .
H2:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
H9:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
H10:   fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H11:   fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H12:   start_byte >= dns_types__packet_bytes_range__first .
H13:   start_byte <= dns_types__packet_bytes_range__last .
H14:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H15:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__1, [i___1]) >= dns_types__byte__first) and (element(
           bytes__1, [i___1]) <= dns_types__byte__last))) .
H16:   16 >= unsigned_types__unsigned16__first .
H17:   16 <= unsigned_types__unsigned16__last .
H18:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H19:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H20:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H21:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H22:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H23:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
        ->
C1:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__2, [i___1]) >= dns_types__byte__first) and (element(
           bytes__2, [i___1]) <= dns_types__byte__last))) .
C2:    start_byte >= dns_types__packet_bytes_range__first .
C3:    start_byte <= dns_types__packet_bytes_range__last .
C4:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
C5:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
C6:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
C7:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
C8:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
C9:    start_byte <= dns_types__packet_bytes_range__last - 22 .
C10:   rr_type__aaaa_record_type__ipv6addrtypeindex__first >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C11:   rr_type__aaaa_record_type__ipv6addrtypeindex__first <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C12:   rr_type__aaaa_record_type__ipv6addrtypeindex__first >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C13:   rr_type__aaaa_record_type__ipv6addrtypeindex__first <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
 

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

procedure_set_ttl_data_aaaa_ip_4.
H1:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H5:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H6:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
H7:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
H8:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
H9:    start_byte <= dns_types__packet_bytes_range__last - 22 .
H10:   loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H11:   loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H12:   loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H13:   loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H14:   element(fld_ipv6(aaaa_record), [loop__1__i]) >= 
           unsigned_types__unsigned16__first .
H15:   element(fld_ipv6(aaaa_record), [loop__1__i]) <= 
           unsigned_types__unsigned16__last .
H16:   start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) >= 
           dns_types__packet_bytes_range__first .
H17:   start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__last .
H18:   start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__last - 1 .
H19:   loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H20:   loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H21:   start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) >= 
           dns_types__packet_bytes_range__base__first .
H22:   start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__base__last .
H23:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           dns_types__packet_bytes_range__first .
H24:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           dns_types__packet_bytes_range__last .
H25:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           integer__base__first .
H26:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           integer__base__last .
H27:   2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           integer__base__first .
H28:   2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           integer__base__last .
H29:   loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first >= 
           integer__base__first .
H30:   loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first <= 
           integer__base__last .
H31:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
H32:   not (loop__1__i = 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last) .
        ->
C1:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes__3, [i___1]) >= dns_types__byte__first) and (element(
           bytes__3, [i___1]) <= dns_types__byte__last))) .
C2:    start_byte >= dns_types__packet_bytes_range__first .
C3:    start_byte <= dns_types__packet_bytes_range__last .
C4:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
C5:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
C6:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
C7:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
C8:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
C9:    start_byte <= dns_types__packet_bytes_range__last - 22 .
C10:   loop__1__i + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C11:   loop__1__i + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C12:   loop__1__i + 1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C13:   loop__1__i + 1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
 

For path(s) from assertion of line 397 to precondition check associated with statement of line 399:

procedure_set_ttl_data_aaaa_ip_5.
H1:    for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           bytes, [i___1]) >= dns_types__byte__first) and (element(
           bytes, [i___1]) <= dns_types__byte__last))) .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    fld_ttlinseconds(fld_inherit(aaaa_record)) >= 
           unsigned_types__unsigned32__first .
H5:    fld_ttlinseconds(fld_inherit(aaaa_record)) <= 
           unsigned_types__unsigned32__last .
H6:    fld_class(fld_inherit(aaaa_record)) >= 
           rr_type__classtype__first .
H7:    fld_class(fld_inherit(aaaa_record)) <= 
           rr_type__classtype__last .
H8:    for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           fld_ipv6(aaaa_record), [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(fld_ipv6(
           aaaa_record), [i___1]) <= 
           unsigned_types__unsigned16__last))) .
H9:    start_byte <= dns_types__packet_bytes_range__last - 22 .
H10:   loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H11:   loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
H12:   loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
H13:   loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
        ->
C1:    element(fld_ipv6(aaaa_record), [loop__1__i]) >= 
           unsigned_types__unsigned16__first .
C2:    element(fld_ipv6(aaaa_record), [loop__1__i]) <= 
           unsigned_types__unsigned16__last .
C3:    start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) >= 
           dns_types__packet_bytes_range__first .
C4:    start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__last .
C5:    start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__last - 1 .
C6:    loop__1__i >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first .
C7:    loop__1__i <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last .
C8:    start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) >= 
           dns_types__packet_bytes_range__base__first .
C9:    start_byte + (6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first)) <= 
           dns_types__packet_bytes_range__base__last .
C10:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           dns_types__packet_bytes_range__first .
C11:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           dns_types__packet_bytes_range__last .
C12:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           integer__base__first .
C13:   6 + 2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           integer__base__last .
C14:   2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) >= 
           integer__base__first .
C15:   2 * (loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) <= 
           integer__base__last .
C16:   loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first >= 
           integer__base__first .
C17:   loop__1__i - 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first <= 
           integer__base__last .
 

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

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


