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

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


              procedure Parser_Utilities.CheckAndAppendOrigin




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

procedure_checkandappendorigin_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           target, [i___1]) >= character__first) and (element(
           target, [i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           origin, [i___1]) >= character__first) and (element(
           origin, [i___1]) <= character__last))) .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H4:    lastpos >= rr_type__linelengthindex__first .
H5:    lastpos <= rr_type__linelengthindex__last .
H6:    linecount >= unsigned_types__unsigned32__first .
H7:    linecount <= unsigned_types__unsigned32__last .
H8:    rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
H9:    rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
H10:   ((rr_type__domainnamelength(target) = 1) and ((element(
           target, [1]) = 32) or (element(target, [2]) = 32))) or ((
           rr_type__domainnamelength(target) = 
           rr_type__maxdomainnamelength) or ((element(
           target, [rr_type__domainnamelength(target) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(target))) -> (element(
           target, [q_]) <> 32))))) .
        ->
C1:    rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
C2:    rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
 

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

procedure_checkandappendorigin_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           target, [i___1]) >= character__first) and (element(
           target, [i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           origin, [i___1]) >= character__first) and (element(
           origin, [i___1]) <= character__last))) .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H4:    lastpos >= rr_type__linelengthindex__first .
H5:    lastpos <= rr_type__linelengthindex__last .
H6:    linecount >= unsigned_types__unsigned32__first .
H7:    linecount <= unsigned_types__unsigned32__last .
H8:    rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
H9:    rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
H10:   ((rr_type__domainnamelength(target) = 1) and ((element(
           target, [1]) = 32) or (element(target, [2]) = 32))) or ((
           rr_type__domainnamelength(target) = 
           rr_type__maxdomainnamelength) or ((element(
           target, [rr_type__domainnamelength(target) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(target))) -> (element(
           target, [q_]) <> 32))))) .
H11:   rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
H12:   rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
H13:   element(target, [rr_type__domainnamelength(target)]) <> 46 .
H14:   origin = rr_type__blankdomainname .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= natural__first .
C4:    lastpos <= natural__last .
 

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

procedure_checkandappendorigin_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           target, [i___1]) >= character__first) and (element(
           target, [i___1]) <= character__last))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           origin, [i___1]) >= character__first) and (element(
           origin, [i___1]) <= character__last))) .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H4:    lastpos >= rr_type__linelengthindex__first .
H5:    lastpos <= rr_type__linelengthindex__last .
H6:    linecount >= unsigned_types__unsigned32__first .
H7:    linecount <= unsigned_types__unsigned32__last .
H8:    rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
H9:    rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
H10:   ((rr_type__domainnamelength(target) = 1) and ((element(
           target, [1]) = 32) or (element(target, [2]) = 32))) or ((
           rr_type__domainnamelength(target) = 
           rr_type__maxdomainnamelength) or ((element(
           target, [rr_type__domainnamelength(target) + 1]) = 32) and (for_all(
           q_: integer, ((q_ >= 1) and (q_ <= 
           rr_type__domainnamelength(target))) -> (element(
           target, [q_]) <> 32))))) .
H11:   rr_type__domainnamelength(target) >= 
           rr_type__domainnamestringtypeindex__first .
H12:   rr_type__domainnamelength(target) <= 
           rr_type__domainnamestringtypeindex__last .
H13:   element(target, [rr_type__domainnamelength(target)]) <> 46 .
H14:   not (origin = rr_type__blankdomainname) .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           target__2, [i___1]) >= character__first) and (element(
           target__2, [i___1]) <= character__last))) .
H16:   not success__2 .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= natural__first .
C4:    lastpos <= natural__last .
 

For path(s) from start to finish:

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


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


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


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


