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

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


                 function dns_table_pkg.DNS_Table_Type.hash




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

function_hash_1.
H1:    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))) .
        ->
C1:    numcharsinhashfunction >= integer__first .
C2:    numcharsinhashfunction <= integer__last .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
 

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

function_hash_2.
H1:    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))) .
H2:    numcharsinhashfunction >= integer__first .
H3:    numcharsinhashfunction <= integer__last .
H4:    1 >= integer__first .
H5:    1 <= integer__last .
        ->
C1:    (1 <= numcharsinhashfunction) -> ((
           numcharsinhashfunction >= integer__first) and (
           numcharsinhashfunction <= integer__last)) .
C2:    (1 <= numcharsinhashfunction) -> ((1 >= integer__first) and (1 <= 
           integer__last)) .
 

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

function_hash_3.
H1:    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))) .
H2:    numcharsinhashfunction >= integer__first .
H3:    numcharsinhashfunction <= integer__last .
H4:    1 >= integer__first .
H5:    1 <= integer__last .
H6:    (1 <= numcharsinhashfunction) -> ((
           numcharsinhashfunction >= integer__first) and (
           numcharsinhashfunction <= integer__last)) .
H7:    (1 <= numcharsinhashfunction) -> ((1 >= integer__first) and (1 <= 
           integer__last)) .
H8:    1 <= numcharsinhashfunction .
        ->
C1:    0 <= (1 - 1) * character__last .
C2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
C3:    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))) .
C4:    1 >= integer__first .
C5:    1 <= integer__last .
C6:    1 >= 1 .
C7:    1 <= numcharsinhashfunction .
 

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

function_hash_4.
H1:    val <= (loop__1__i - 1) * character__last .
H2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
H3:    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))) .
H4:    loop__1__i >= integer__first .
H5:    loop__1__i <= integer__last .
H6:    loop__1__i >= 1 .
H7:    loop__1__i <= numcharsinhashfunction .
H8:    val >= natural__first .
H9:    val <= natural__last .
H10:   val + element(domainname, [loop__1__i]) >= natural__first .
H11:   val + element(domainname, [loop__1__i]) <= natural__last .
H12:   loop__1__i >= rr_type__wirestringtypeindex__first .
H13:   loop__1__i <= rr_type__wirestringtypeindex__last .
H14:   not (loop__1__i = numcharsinhashfunction) .
        ->
C1:    val + element(domainname, [loop__1__i]) <= (loop__1__i + 1 - 1) * 
           character__last .
C2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
C3:    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))) .
C4:    loop__1__i + 1 >= integer__first .
C5:    loop__1__i + 1 <= integer__last .
C6:    loop__1__i + 1 >= 1 .
C7:    loop__1__i + 1 <= numcharsinhashfunction .
 

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

function_hash_5.
H1:    val <= (loop__1__i - 1) * character__last .
H2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
H3:    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))) .
H4:    loop__1__i >= integer__first .
H5:    loop__1__i <= integer__last .
H6:    loop__1__i >= 1 .
H7:    loop__1__i <= numcharsinhashfunction .
H8:    val >= natural__first .
H9:    val <= natural__last .
        ->
C1:    val + element(domainname, [loop__1__i]) >= natural__first .
C2:    val + element(domainname, [loop__1__i]) <= natural__last .
C3:    loop__1__i >= rr_type__wirestringtypeindex__first .
C4:    loop__1__i <= rr_type__wirestringtypeindex__last .
 

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

function_hash_6.
H1:    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))) .
H2:    numcharsinhashfunction >= integer__first .
H3:    numcharsinhashfunction <= integer__last .
H4:    1 >= integer__first .
H5:    1 <= integer__last .
H6:    (1 <= numcharsinhashfunction) -> ((
           numcharsinhashfunction >= integer__first) and (
           numcharsinhashfunction <= integer__last)) .
H7:    (1 <= numcharsinhashfunction) -> ((1 >= integer__first) and (1 <= 
           integer__last)) .
H8:    not (1 <= numcharsinhashfunction) .
H9:    0 >= natural__first .
H10:   0 <= natural__last .
        ->
C1:    0 mod rr_type__numbuckets + 1 >= integer__base__first .
C2:    0 mod rr_type__numbuckets + 1 <= integer__base__last .
C3:    0 mod rr_type__numbuckets >= integer__base__first .
C4:    0 mod rr_type__numbuckets <= integer__base__last .
C5:    rr_type__numbuckets <> 0 .
 

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

function_hash_7.
H1:    val <= (loop__1__i - 1) * character__last .
H2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
H3:    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))) .
H4:    loop__1__i >= integer__first .
H5:    loop__1__i <= integer__last .
H6:    loop__1__i >= 1 .
H7:    loop__1__i <= numcharsinhashfunction .
H8:    val >= natural__first .
H9:    val <= natural__last .
H10:   val + element(domainname, [loop__1__i]) >= natural__first .
H11:   val + element(domainname, [loop__1__i]) <= natural__last .
H12:   loop__1__i >= rr_type__wirestringtypeindex__first .
H13:   loop__1__i <= rr_type__wirestringtypeindex__last .
H14:   loop__1__i = numcharsinhashfunction .
H15:   val + element(domainname, [loop__1__i]) >= natural__first .
H16:   val + element(domainname, [loop__1__i]) <= natural__last .
        ->
C1:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 >= integer__base__first .
C2:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 <= integer__base__last .
C3:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets >= integer__base__first .
C4:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets <= integer__base__last .
C5:    rr_type__numbuckets <> 0 .
 

For path(s) from start to finish:

function_hash_8.
H1:    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))) .
H2:    numcharsinhashfunction >= integer__first .
H3:    numcharsinhashfunction <= integer__last .
H4:    1 >= integer__first .
H5:    1 <= integer__last .
H6:    (1 <= numcharsinhashfunction) -> ((
           numcharsinhashfunction >= integer__first) and (
           numcharsinhashfunction <= integer__last)) .
H7:    (1 <= numcharsinhashfunction) -> ((1 >= integer__first) and (1 <= 
           integer__last)) .
H8:    not (1 <= numcharsinhashfunction) .
H9:    0 >= natural__first .
H10:   0 <= natural__last .
H11:   0 mod rr_type__numbuckets + 1 >= integer__base__first .
H12:   0 mod rr_type__numbuckets + 1 <= integer__base__last .
H13:   0 mod rr_type__numbuckets >= integer__base__first .
H14:   0 mod rr_type__numbuckets <= integer__base__last .
H15:   rr_type__numbuckets <> 0 .
        ->
C1:    0 mod rr_type__numbuckets + 1 >= 
           rr_type__numbucketsindextype__first .
C2:    0 mod rr_type__numbuckets + 1 <= 
           rr_type__numbucketsindextype__last .
 

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

function_hash_9.
H1:    val <= (loop__1__i - 1) * character__last .
H2:    for_all(q_: integer, ((q_ >= 
           rr_type__wirestringtypeindex__first) and (q_ <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [q_]) <= 255) and (element(
           domainname, [q_]) >= 0))) .
H3:    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))) .
H4:    loop__1__i >= integer__first .
H5:    loop__1__i <= integer__last .
H6:    loop__1__i >= 1 .
H7:    loop__1__i <= numcharsinhashfunction .
H8:    val >= natural__first .
H9:    val <= natural__last .
H10:   val + element(domainname, [loop__1__i]) >= natural__first .
H11:   val + element(domainname, [loop__1__i]) <= natural__last .
H12:   loop__1__i >= rr_type__wirestringtypeindex__first .
H13:   loop__1__i <= rr_type__wirestringtypeindex__last .
H14:   loop__1__i = numcharsinhashfunction .
H15:   val + element(domainname, [loop__1__i]) >= natural__first .
H16:   val + element(domainname, [loop__1__i]) <= natural__last .
H17:   (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 >= integer__base__first .
H18:   (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 <= integer__base__last .
H19:   (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets >= integer__base__first .
H20:   (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets <= integer__base__last .
H21:   rr_type__numbuckets <> 0 .
        ->
C1:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 >= 
           rr_type__numbucketsindextype__first .
C2:    (val + element(domainname, [loop__1__i])) mod 
           rr_type__numbuckets + 1 <= 
           rr_type__numbucketsindextype__last .
 

