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

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


               procedure Process_Dns_Request.Set_Unsigned_16




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

procedure_set_unsigned_16_1.
H1:    start_byte <= dns_types__packet_bytes_range__last - 1 .
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:    value >= unsigned_types__unsigned16__first .
H6:    value <= unsigned_types__unsigned16__last .
        ->
C1:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
C2:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
C3:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
C4:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
C5:    256 <> 0 .
C6:    2 ** 8 <> 0 .
C7:    2 ** 8 >= system__min_int .
C8:    2 ** 8 <= system__max_int .
C9:    8 >= 0 .
C10:   start_byte >= dns_types__packet_bytes_range__first .
C11:   start_byte <= dns_types__packet_bytes_range__last .
 

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

procedure_set_unsigned_16_2.
H1:    start_byte <= dns_types__packet_bytes_range__last - 1 .
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:    value >= unsigned_types__unsigned16__first .
H6:    value <= unsigned_types__unsigned16__last .
H7:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
H8:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
H9:    value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
H10:   value div 2 ** 8 mod unsigned_types__unsigned16__modulus mod 256 mod 
           unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
H11:   256 <> 0 .
H12:   2 ** 8 <> 0 .
H13:   2 ** 8 >= system__min_int .
H14:   2 ** 8 <= system__max_int .
H15:   8 >= 0 .
H16:   start_byte >= dns_types__packet_bytes_range__first .
H17:   start_byte <= dns_types__packet_bytes_range__last .
        ->
C1:    value mod 256 mod unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
C2:    value mod 256 mod unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
C3:    value mod 256 mod unsigned_types__unsigned16__modulus >= 
           dns_types__byte__first .
C4:    value mod 256 mod unsigned_types__unsigned16__modulus <= 
           dns_types__byte__last .
C5:    256 <> 0 .
C6:    start_byte + 1 >= dns_types__packet_bytes_range__first .
C7:    start_byte + 1 <= dns_types__packet_bytes_range__last .
C8:    start_byte + 1 >= dns_types__packet_bytes_range__base__first .
C9:    start_byte + 1 <= dns_types__packet_bytes_range__base__last .
 

For path(s) from start to finish:

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


