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

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


               procedure Parser_Utilities.checkValidHostName




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

procedure_checkvalidhostname_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H3:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H4:    ((rr_type__domainnamelength(name) = 1) and ((element(
           name, [1]) = 32) or (element(name, [2]) = 32))) or ((
           rr_type__domainnamelength(name) = 
           rr_type__maxdomainnamelength) or ((element(name, [
           rr_type__domainnamelength(name) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(name))) -> (element(
           name, [q_]) <> 32))))) .
        ->
C1:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
C2:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H3:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H4:    ((rr_type__domainnamelength(name) = 1) and ((element(
           name, [1]) = 32) or (element(name, [2]) = 32))) or ((
           rr_type__domainnamelength(name) = 
           rr_type__maxdomainnamelength) or ((element(name, [
           rr_type__domainnamelength(name) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(name))) -> (element(
           name, [q_]) <> 32))))) .
H5:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H6:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H7:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H8:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
        ->
C1:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
C2:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
C3:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
C4:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
C5:    1 >= rr_type__domainnamestringtypeindex__first .
C6:    1 <= rr_type__domainnamestringtypeindex__last .
C7:    1 >= rr_type__domainnamestringtypeindex__first .
C8:    1 <= rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H3:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H4:    ((rr_type__domainnamelength(name) = 1) and ((element(
           name, [1]) = 32) or (element(name, [2]) = 32))) or ((
           rr_type__domainnamelength(name) = 
           rr_type__maxdomainnamelength) or ((element(name, [
           rr_type__domainnamelength(name) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(name))) -> (element(
           name, [q_]) <> 32))))) .
H5:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H6:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H7:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H8:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H9:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H10:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H11:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H12:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H13:   1 >= rr_type__domainnamestringtypeindex__first .
H14:   1 <= rr_type__domainnamestringtypeindex__last .
H15:   1 >= rr_type__domainnamestringtypeindex__first .
H16:   1 <= rr_type__domainnamestringtypeindex__last .
H17:   not ((element(name, [1]) = 46) or ((element(name, [1]) = 45) or ((
           rr_type__domainnamelength(name) > 1) and ((element(
           name, [rr_type__domainnamelength(name) - 1]) = 46) or (element(
           name, [rr_type__domainnamelength(name) - 1]) = 45))))) .
H18:   rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H19:   rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
        ->
C1:    rr_type__domainnamelength(name) - 2 >= integer__first .
C2:    rr_type__domainnamelength(name) - 2 <= integer__last .
C3:    rr_type__domainnamelength(name) - 2 >= integer__base__first .
C4:    rr_type__domainnamelength(name) - 2 <= integer__base__last .
C5:    2 >= integer__first .
C6:    2 <= integer__last .
 

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

procedure_checkvalidhostname_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H3:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H4:    ((rr_type__domainnamelength(name) = 1) and ((element(
           name, [1]) = 32) or (element(name, [2]) = 32))) or ((
           rr_type__domainnamelength(name) = 
           rr_type__maxdomainnamelength) or ((element(name, [
           rr_type__domainnamelength(name) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(name))) -> (element(
           name, [q_]) <> 32))))) .
H5:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H6:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H7:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H8:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H9:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H10:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H11:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H12:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H13:   1 >= rr_type__domainnamestringtypeindex__first .
H14:   1 <= rr_type__domainnamestringtypeindex__last .
H15:   1 >= rr_type__domainnamestringtypeindex__first .
H16:   1 <= rr_type__domainnamestringtypeindex__last .
H17:   not ((element(name, [1]) = 46) or ((element(name, [1]) = 45) or ((
           rr_type__domainnamelength(name) > 1) and ((element(
           name, [rr_type__domainnamelength(name) - 1]) = 46) or (element(
           name, [rr_type__domainnamelength(name) - 1]) = 45))))) .
H18:   rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H19:   rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H20:   rr_type__domainnamelength(name) - 2 >= integer__first .
H21:   rr_type__domainnamelength(name) - 2 <= integer__last .
H22:   rr_type__domainnamelength(name) - 2 >= integer__base__first .
H23:   rr_type__domainnamelength(name) - 2 <= integer__base__last .
H24:   2 >= integer__first .
H25:   2 <= integer__last .
        ->
C1:    (2 <= rr_type__domainnamelength(name) - 2) -> ((
           rr_type__domainnamelength(name) - 2 >= integer__first) and (
           rr_type__domainnamelength(name) - 2 <= integer__last)) .
C2:    (2 <= rr_type__domainnamelength(name) - 2) -> ((2 >= 
           integer__first) and (2 <= integer__last)) .
 

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

procedure_checkvalidhostname_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H3:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H4:    ((rr_type__domainnamelength(name) = 1) and ((element(
           name, [1]) = 32) or (element(name, [2]) = 32))) or ((
           rr_type__domainnamelength(name) = 
           rr_type__maxdomainnamelength) or ((element(name, [
           rr_type__domainnamelength(name) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(name))) -> (element(
           name, [q_]) <> 32))))) .
H5:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H6:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H7:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H8:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H9:    (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H10:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H11:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           rr_type__domainnamelength(name) - 1 <= 
           rr_type__domainnamestringtypeindex__last)) .
H12:   (rr_type__domainnamelength(name) > 1) -> ((
           rr_type__domainnamelength(name) - 1 >= integer__base__first) and (
           rr_type__domainnamelength(name) - 1 <= integer__base__last)) .
H13:   1 >= rr_type__domainnamestringtypeindex__first .
H14:   1 <= rr_type__domainnamestringtypeindex__last .
H15:   1 >= rr_type__domainnamestringtypeindex__first .
H16:   1 <= rr_type__domainnamestringtypeindex__last .
H17:   not ((element(name, [1]) = 46) or ((element(name, [1]) = 45) or ((
           rr_type__domainnamelength(name) > 1) and ((element(
           name, [rr_type__domainnamelength(name) - 1]) = 46) or (element(
           name, [rr_type__domainnamelength(name) - 1]) = 45))))) .
H18:   rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H19:   rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H20:   rr_type__domainnamelength(name) - 2 >= integer__first .
H21:   rr_type__domainnamelength(name) - 2 <= integer__last .
H22:   rr_type__domainnamelength(name) - 2 >= integer__base__first .
H23:   rr_type__domainnamelength(name) - 2 <= integer__base__last .
H24:   2 >= integer__first .
H25:   2 <= integer__last .
H26:   (2 <= rr_type__domainnamelength(name) - 2) -> ((
           rr_type__domainnamelength(name) - 2 >= integer__first) and (
           rr_type__domainnamelength(name) - 2 <= integer__last)) .
H27:   (2 <= rr_type__domainnamelength(name) - 2) -> ((2 >= 
           integer__first) and (2 <= integer__last)) .
H28:   rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
H29:   rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
H30:   2 <= rr_type__domainnamelength(name) - 2 .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
C2:    2 >= integer__first .
C3:    2 <= integer__last .
C4:    2 >= 2 .
C5:    2 <= rr_type__domainnamelength(name) - 2 .
C6:    rr_type__domainnamelength(name) >= 
           rr_type__domainnamestringtypeindex__first .
C7:    rr_type__domainnamelength(name) <= 
           rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_6.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   element(name, [loop__1__i]) = 46 .
H11:   loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
H12:   loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
H13:   loop__1__i - 1 >= integer__base__first .
H14:   loop__1__i - 1 <= integer__base__last .
H15:   loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
H16:   loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
H17:   loop__1__i - 1 >= integer__base__first .
H18:   loop__1__i - 1 <= integer__base__last .
H19:   (element(name, [loop__1__i - 1]) = 46) or (element(
           name, [loop__1__i - 1]) = 45) .
H20:   not (loop__1__i = length__entry__loop__1 - 2) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
C2:    loop__1__i + 1 >= integer__first .
C3:    loop__1__i + 1 <= integer__last .
C4:    loop__1__i + 1 >= 2 .
C5:    loop__1__i + 1 <= length__entry__loop__1 - 2 .
C6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
C7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
 

procedure_checkvalidhostname_7.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   element(name, [loop__1__i]) = 46 .
H11:   loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
H12:   loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
H13:   loop__1__i - 1 >= integer__base__first .
H14:   loop__1__i - 1 <= integer__base__last .
H15:   loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
H16:   loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
H17:   loop__1__i - 1 >= integer__base__first .
H18:   loop__1__i - 1 <= integer__base__last .
H19:   not ((element(name, [loop__1__i - 1]) = 46) or (element(
           name, [loop__1__i - 1]) = 45)) .
H20:   not (loop__1__i = length__entry__loop__1 - 2) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
C2:    loop__1__i + 1 >= integer__first .
C3:    loop__1__i + 1 <= integer__last .
C4:    loop__1__i + 1 >= 2 .
C5:    loop__1__i + 1 <= length__entry__loop__1 - 2 .
C6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
C7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
 

procedure_checkvalidhostname_8.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   not (element(name, [loop__1__i]) = 46) .
H11:   element(name, [loop__1__i]) >= character__first .
H12:   element(name, [loop__1__i]) <= character__last .
H13:   loop__1__i >= rr_type__domainnamestringtypeindex__first .
H14:   loop__1__i <= rr_type__domainnamestringtypeindex__last .
H15:   true .
H16:   loop__1__i >= rr_type__domainnamestringtypeindex__first .
H17:   loop__1__i <= rr_type__domainnamestringtypeindex__last .
H18:   not (ada__characters__handling__is_alphanumeric(element(
           name, [loop__1__i]))) .
H19:   element(name, [loop__1__i]) <> 45 .
H20:   not (loop__1__i = length__entry__loop__1 - 2) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
C2:    loop__1__i + 1 >= integer__first .
C3:    loop__1__i + 1 <= integer__last .
C4:    loop__1__i + 1 >= 2 .
C5:    loop__1__i + 1 <= length__entry__loop__1 - 2 .
C6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
C7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
 

procedure_checkvalidhostname_9.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   not (element(name, [loop__1__i]) = 46) .
H11:   element(name, [loop__1__i]) >= character__first .
H12:   element(name, [loop__1__i]) <= character__last .
H13:   loop__1__i >= rr_type__domainnamestringtypeindex__first .
H14:   loop__1__i <= rr_type__domainnamestringtypeindex__last .
H15:   true .
H16:   loop__1__i >= rr_type__domainnamestringtypeindex__first .
H17:   loop__1__i <= rr_type__domainnamestringtypeindex__last .
H18:   not ((not (ada__characters__handling__is_alphanumeric(element(
           name, [loop__1__i])))) and (element(name, [
           loop__1__i]) <> 45)) .
H19:   not (loop__1__i = length__entry__loop__1 - 2) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
C2:    loop__1__i + 1 >= integer__first .
C3:    loop__1__i + 1 <= integer__last .
C4:    loop__1__i + 1 >= 2 .
C5:    loop__1__i + 1 <= length__entry__loop__1 - 2 .
C6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
C7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_10.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
        ->
C1:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
C2:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_11.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   element(name, [loop__1__i]) = 46 .
        ->
C1:    loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
C2:    loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
C3:    loop__1__i - 1 >= integer__base__first .
C4:    loop__1__i - 1 <= integer__base__last .
C5:    loop__1__i - 1 >= rr_type__domainnamestringtypeindex__first .
C6:    loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last .
C7:    loop__1__i - 1 >= integer__base__first .
C8:    loop__1__i - 1 <= integer__base__last .
 

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

procedure_checkvalidhostname_12.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   not (element(name, [loop__1__i]) = 46) .
        ->
C1:    element(name, [loop__1__i]) >= character__first .
C2:    element(name, [loop__1__i]) <= character__last .
C3:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
C4:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkvalidhostname_13.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           name, [i___1]) >= character__first) and (element(
           name, [i___1]) <= character__last))) .
H2:    loop__1__i >= integer__first .
H3:    loop__1__i <= integer__last .
H4:    loop__1__i >= 2 .
H5:    loop__1__i <= length__entry__loop__1 - 2 .
H6:    length__entry__loop__1 >= 
           rr_type__domainnamestringtypeindex__first .
H7:    length__entry__loop__1 <= 
           rr_type__domainnamestringtypeindex__last .
H8:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
H9:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
H10:   not (element(name, [loop__1__i]) = 46) .
H11:   element(name, [loop__1__i]) >= character__first .
H12:   element(name, [loop__1__i]) <= character__last .
H13:   loop__1__i >= rr_type__domainnamestringtypeindex__first .
H14:   loop__1__i <= rr_type__domainnamestringtypeindex__last .
H15:   true .
        ->
C1:    loop__1__i >= rr_type__domainnamestringtypeindex__first .
C2:    loop__1__i <= rr_type__domainnamestringtypeindex__last .
 

For path(s) from start to finish:

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


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


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

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


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


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


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


