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

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


            function Rr_Type.ConvertDomainNameToWire.FindPeriod




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

function_findperiod_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H2:    position >= linelengthindex__first .
H3:    position <= linelengthindex__last .
        ->
C1:    position >= linelengthindex__first .
C2:    position <= linelengthindex__last .
 

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

function_findperiod_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H2:    position >= linelengthindex__first .
H3:    position <= linelengthindex__last .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    position >= linelengthindex__first .
H7:    position <= linelengthindex__last .
        ->
C1:    (position < domainnamestringtypeindex__last) -> ((
           position >= domainnamestringtypeindex__first) and (
           position <= domainnamestringtypeindex__last)) .
 

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

function_findperiod_3.
H1:    result >= position .
H2:    result < linelengthindex__last .
H3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    result >= linelengthindex__first .
H7:    result <= linelengthindex__last .
H8:    result + 1 >= linelengthindex__first .
H9:    result + 1 <= linelengthindex__last .
H10:   result + 1 >= linelengthindex__first .
H11:   result + 1 <= linelengthindex__last .
        ->
C1:    (result + 1 < domainnamestringtypeindex__last) -> ((
           result + 1 >= domainnamestringtypeindex__first) and (
           result + 1 <= domainnamestringtypeindex__last)) .
 

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

function_findperiod_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H2:    position >= linelengthindex__first .
H3:    position <= linelengthindex__last .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    position >= linelengthindex__first .
H7:    position <= linelengthindex__last .
H8:    (position < domainnamestringtypeindex__last) -> ((
           position >= domainnamestringtypeindex__first) and (
           position <= domainnamestringtypeindex__last)) .
H9:    position < domainnamestringtypeindex__last .
H10:   element(token, [position]) <> 46 .
        ->
C1:    position >= position .
C2:    position < linelengthindex__last .
C3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
C4:    position >= linelengthindex__first .
C5:    position <= linelengthindex__last .
 

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

function_findperiod_5.
H1:    result >= position .
H2:    result < linelengthindex__last .
H3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    result >= linelengthindex__first .
H7:    result <= linelengthindex__last .
H8:    result + 1 >= linelengthindex__first .
H9:    result + 1 <= linelengthindex__last .
H10:   result + 1 >= linelengthindex__first .
H11:   result + 1 <= linelengthindex__last .
H12:   (result + 1 < domainnamestringtypeindex__last) -> ((
           result + 1 >= domainnamestringtypeindex__first) and (
           result + 1 <= domainnamestringtypeindex__last)) .
H13:   result + 1 < domainnamestringtypeindex__last .
H14:   element(token, [result + 1]) <> 46 .
        ->
C1:    result + 1 >= position .
C2:    result + 1 < linelengthindex__last .
C3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
C4:    position >= linelengthindex__first .
C5:    position <= linelengthindex__last .
 

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

function_findperiod_6.
H1:    result >= position .
H2:    result < linelengthindex__last .
H3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    result >= linelengthindex__first .
H7:    result <= linelengthindex__last .
        ->
C1:    result + 1 >= linelengthindex__first .
C2:    result + 1 <= linelengthindex__last .
 

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

function_findperiod_7.
H1:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H2:    position >= linelengthindex__first .
H3:    position <= linelengthindex__last .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    position >= linelengthindex__first .
H7:    position <= linelengthindex__last .
H8:    (position < domainnamestringtypeindex__last) -> ((
           position >= domainnamestringtypeindex__first) and (
           position <= domainnamestringtypeindex__last)) .
H9:    not ((position < domainnamestringtypeindex__last) and (element(
           token, [position]) <> 46)) .
H10:   position >= linelengthindex__first .
H11:   position <= linelengthindex__last .
        ->
C1:    position - position >= character__first .
C2:    position - position <= character__last .
C3:    position - position >= integer__base__first .
C4:    position - position <= integer__base__last .
 

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

function_findperiod_8.
H1:    result >= position .
H2:    result < linelengthindex__last .
H3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    result >= linelengthindex__first .
H7:    result <= linelengthindex__last .
H8:    result + 1 >= linelengthindex__first .
H9:    result + 1 <= linelengthindex__last .
H10:   result + 1 >= linelengthindex__first .
H11:   result + 1 <= linelengthindex__last .
H12:   (result + 1 < domainnamestringtypeindex__last) -> ((
           result + 1 >= domainnamestringtypeindex__first) and (
           result + 1 <= domainnamestringtypeindex__last)) .
H13:   not ((result + 1 < domainnamestringtypeindex__last) and (element(
           token, [result + 1]) <> 46)) .
H14:   result + 1 >= linelengthindex__first .
H15:   result + 1 <= linelengthindex__last .
        ->
C1:    result + 1 - position >= character__first .
C2:    result + 1 - position <= character__last .
C3:    result + 1 - position >= integer__base__first .
C4:    result + 1 - position <= integer__base__last .
 

For path(s) from start to finish:

function_findperiod_9.
H1:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H2:    position >= linelengthindex__first .
H3:    position <= linelengthindex__last .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    position >= linelengthindex__first .
H7:    position <= linelengthindex__last .
H8:    (position < domainnamestringtypeindex__last) -> ((
           position >= domainnamestringtypeindex__first) and (
           position <= domainnamestringtypeindex__last)) .
H9:    not ((position < domainnamestringtypeindex__last) and (element(
           token, [position]) <> 46)) .
H10:   position >= linelengthindex__first .
H11:   position <= linelengthindex__last .
H12:   position - position >= character__first .
H13:   position - position <= character__last .
H14:   position - position >= integer__base__first .
H15:   position - position <= integer__base__last .
        ->
C1:    position - position >= character__first .
C2:    position - position <= character__last .
 

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

function_findperiod_10.
H1:    result >= position .
H2:    result < linelengthindex__last .
H3:    for_all(i___1: integer, ((i___1 >= 
           domainnamestringtypeindex__first) and (i___1 <= 
           domainnamestringtypeindex__last)) -> ((element(
           token, [i___1]) >= character__first) and (element(
           token, [i___1]) <= character__last))) .
H4:    position >= linelengthindex__first .
H5:    position <= linelengthindex__last .
H6:    result >= linelengthindex__first .
H7:    result <= linelengthindex__last .
H8:    result + 1 >= linelengthindex__first .
H9:    result + 1 <= linelengthindex__last .
H10:   result + 1 >= linelengthindex__first .
H11:   result + 1 <= linelengthindex__last .
H12:   (result + 1 < domainnamestringtypeindex__last) -> ((
           result + 1 >= domainnamestringtypeindex__first) and (
           result + 1 <= domainnamestringtypeindex__last)) .
H13:   not ((result + 1 < domainnamestringtypeindex__last) and (element(
           token, [result + 1]) <> 46)) .
H14:   result + 1 >= linelengthindex__first .
H15:   result + 1 <= linelengthindex__last .
H16:   result + 1 - position >= character__first .
H17:   result + 1 - position <= character__last .
H18:   result + 1 - position >= integer__base__first .
H19:   result + 1 - position <= integer__base__last .
        ->
C1:    result + 1 - position >= character__first .
C2:    result + 1 - position <= character__last .
 

