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

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


                    function Process_Dns_Request.Lookup




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

function_lookup_1.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 65 .
H4:    arg <= 90 .
        ->
C1:    (arg - 65) mod dns_types__byte__modulus >= 
           dns_types__byte__first .
C2:    (arg - 65) mod dns_types__byte__modulus <= 
           dns_types__byte__last .
 

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

function_lookup_2.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 97 .
H4:    arg <= 122 .
        ->
C1:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
C2:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
 

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

function_lookup_3.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 48 .
H4:    arg <= 57 .
        ->
C1:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
C2:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
 

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

function_lookup_4.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg = 43 .
        ->
C1:    62 >= dns_types__byte__first .
C2:    62 <= dns_types__byte__last .
 

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

function_lookup_5.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg = 47 .
        ->
C1:    63 >= dns_types__byte__first .
C2:    63 <= dns_types__byte__last .
 

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

function_lookup_6.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    not ((arg >= 65) and (arg <= 90)) .
H4:    not ((arg >= 97) and (arg <= 122)) .
H5:    not ((arg >= 48) and (arg <= 57)) .
H6:    not (arg = 43) .
H7:    not (arg = 47) .
        ->
C1:    0 >= dns_types__byte__first .
C2:    0 <= dns_types__byte__last .
 

For path(s) from start to finish:

function_lookup_7.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 65 .
H4:    arg <= 90 .
H5:    (arg - 65) mod dns_types__byte__modulus >= 
           dns_types__byte__first .
H6:    (arg - 65) mod dns_types__byte__modulus <= 
           dns_types__byte__last .
H7:    (arg - 65) mod dns_types__byte__modulus >= 
           dns_types__byte__first .
H8:    (arg - 65) mod dns_types__byte__modulus <= 
           dns_types__byte__last .
        ->
C1:    (arg - 65) mod dns_types__byte__modulus >= 
           dns_types__byte__first .
C2:    (arg - 65) mod dns_types__byte__modulus <= 
           dns_types__byte__last .
 

function_lookup_8.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 97 .
H4:    arg <= 122 .
H5:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
H6:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
H7:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
H8:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
        ->
C1:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
C2:    ((arg - 97) mod dns_types__byte__modulus + 26) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
 

function_lookup_9.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg >= 48 .
H4:    arg <= 57 .
H5:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
H6:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
H7:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
H8:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
        ->
C1:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus >= dns_types__byte__first .
C2:    ((arg - 48) mod dns_types__byte__modulus + 52) mod 
           dns_types__byte__modulus <= dns_types__byte__last .
 

function_lookup_10.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg = 43 .
H4:    62 >= dns_types__byte__first .
H5:    62 <= dns_types__byte__last .
H6:    62 >= dns_types__byte__first .
H7:    62 <= dns_types__byte__last .
        ->
C1:    62 >= dns_types__byte__first .
C2:    62 <= dns_types__byte__last .
 

function_lookup_11.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    arg = 47 .
H4:    63 >= dns_types__byte__first .
H5:    63 <= dns_types__byte__last .
H6:    63 >= dns_types__byte__first .
H7:    63 <= dns_types__byte__last .
        ->
C1:    63 >= dns_types__byte__first .
C2:    63 <= dns_types__byte__last .
 

function_lookup_12.
H1:    arg >= character__first .
H2:    arg <= character__last .
H3:    not ((arg >= 65) and (arg <= 90)) .
H4:    not ((arg >= 97) and (arg <= 122)) .
H5:    not ((arg >= 48) and (arg <= 57)) .
H6:    not (arg = 43) .
H7:    not (arg = 47) .
H8:    0 >= dns_types__byte__first .
H9:    0 <= dns_types__byte__last .
H10:   0 >= dns_types__byte__first .
H11:   0 <= dns_types__byte__last .
        ->
C1:    0 >= dns_types__byte__first .
C2:    0 <= dns_types__byte__last .
 

