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

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


               procedure Process_Dns_Request.Set_TTL_Data_IP




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

procedure_set_ttl_data_ip_1.
H1:    start_byte <= dns_types__packet_bytes_range__last - 10 .
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(a_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(a_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(a_record)) >= rr_type__classtype__first .
H8:    fld_class(fld_inherit(a_record)) <= rr_type__classtype__last .
H9:    fld_ipv4(a_record) >= unsigned_types__unsigned32__first .
H10:   fld_ipv4(a_record) <= unsigned_types__unsigned32__last .
        ->
C1:    fld_ttlinseconds(fld_inherit(a_record)) >= 
           unsigned_types__unsigned32__first .
C2:    fld_ttlinseconds(fld_inherit(a_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 63:

procedure_set_ttl_data_ip_2.
H1:    start_byte <= dns_types__packet_bytes_range__last - 10 .
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(a_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(a_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(a_record)) >= rr_type__classtype__first .
H8:    fld_class(fld_inherit(a_record)) <= rr_type__classtype__last .
H9:    fld_ipv4(a_record) >= unsigned_types__unsigned32__first .
H10:   fld_ipv4(a_record) <= unsigned_types__unsigned32__last .
H11:   fld_ttlinseconds(fld_inherit(a_record)) >= 
           unsigned_types__unsigned32__first .
H12:   fld_ttlinseconds(fld_inherit(a_record)) <= 
           unsigned_types__unsigned32__last .
H13:   start_byte >= dns_types__packet_bytes_range__first .
H14:   start_byte <= dns_types__packet_bytes_range__last .
H15:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H16:   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:    4 >= unsigned_types__unsigned16__first .
C2:    4 <= 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 precondition check associated with statement of line 65:

procedure_set_ttl_data_ip_3.
H1:    start_byte <= dns_types__packet_bytes_range__last - 10 .
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(a_record)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(a_record)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(a_record)) >= rr_type__classtype__first .
H8:    fld_class(fld_inherit(a_record)) <= rr_type__classtype__last .
H9:    fld_ipv4(a_record) >= unsigned_types__unsigned32__first .
H10:   fld_ipv4(a_record) <= unsigned_types__unsigned32__last .
H11:   fld_ttlinseconds(fld_inherit(a_record)) >= 
           unsigned_types__unsigned32__first .
H12:   fld_ttlinseconds(fld_inherit(a_record)) <= 
           unsigned_types__unsigned32__last .
H13:   start_byte >= dns_types__packet_bytes_range__first .
H14:   start_byte <= dns_types__packet_bytes_range__last .
H15:   start_byte <= dns_types__packet_bytes_range__last - 3 .
H16:   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))) .
H17:   4 >= unsigned_types__unsigned16__first .
H18:   4 <= unsigned_types__unsigned16__last .
H19:   start_byte + 4 >= dns_types__packet_bytes_range__first .
H20:   start_byte + 4 <= dns_types__packet_bytes_range__last .
H21:   start_byte + 4 <= dns_types__packet_bytes_range__last - 1 .
H22:   start_byte + 4 >= dns_types__packet_bytes_range__base__first .
H23:   start_byte + 4 <= dns_types__packet_bytes_range__base__last .
H24:   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:    fld_ipv4(a_record) >= unsigned_types__unsigned32__first .
C2:    fld_ipv4(a_record) <= unsigned_types__unsigned32__last .
C3:    start_byte + 6 >= dns_types__packet_bytes_range__first .
C4:    start_byte + 6 <= dns_types__packet_bytes_range__last .
C5:    start_byte + 6 <= dns_types__packet_bytes_range__last - 3 .
C6:    start_byte + 6 >= dns_types__packet_bytes_range__base__first .
C7:    start_byte + 6 <= dns_types__packet_bytes_range__base__last .
 

For path(s) from start to finish:

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


