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

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


                    procedure Zone_File_Parser.parseIpv4




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

procedure_parseipv4_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

For path(s) from start to precondition check associated with statement of line 818:

procedure_parseipv4_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
        ->
C1:    1 >= rr_type__linelengthindex__first .
C2:    1 <= rr_type__linelengthindex__last .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
C5:    1 <= zlength .
 

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

procedure_parseipv4_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
        ->
C1:    foundtype__1 >= rr_type__rritemtype__first .
C2:    foundtype__1 <= rr_type__rritemtype__last .
C3:    endidx__1 >= rr_type__linelengthindex__first .
C4:    endidx__1 <= rr_type__linelengthindex__last .
C5:    begidx__1 >= rr_type__linelengthindex__first .
C6:    begidx__1 <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   endidx__1 >= rr_type__linelengthindex__first .
H30:   endidx__1 <= rr_type__linelengthindex__last .
H31:   foundtype__1 >= rr_type__rritemtype__first .
H32:   foundtype__1 <= rr_type__rritemtype__last .
H33:   foundtype__1 <> rr_type__ipv4 .
H34:   endidx__1 < zlength .
        ->
C1:    endidx__1 < zlength .
C2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_5.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H17:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H18:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H19:   zlength >= rr_type__linelengthindex__first .
H20:   zlength <= rr_type__linelengthindex__last .
H21:   begidx - begidx + endidx + 1 <= zlength .
H22:   begidx__2 <= endidx__2 .
H23:   begidx__2 <= zlength .
H24:   endidx__2 <= zlength .
H25:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H26:   begidx__2 >= rr_type__linelengthindex__first .
H27:   begidx__2 <= rr_type__linelengthindex__last .
H28:   endidx__2 >= rr_type__linelengthindex__first .
H29:   endidx__2 <= rr_type__linelengthindex__last .
H30:   foundtype__2 >= rr_type__rritemtype__first .
H31:   foundtype__2 <= rr_type__rritemtype__last .
H32:   foundtype__2 >= rr_type__rritemtype__first .
H33:   foundtype__2 <= rr_type__rritemtype__last .
H34:   endidx__2 >= rr_type__linelengthindex__first .
H35:   endidx__2 <= rr_type__linelengthindex__last .
H36:   begidx__2 >= rr_type__linelengthindex__first .
H37:   begidx__2 <= rr_type__linelengthindex__last .
H38:   endidx__2 >= rr_type__linelengthindex__first .
H39:   endidx__2 <= rr_type__linelengthindex__last .
H40:   foundtype__2 >= rr_type__rritemtype__first .
H41:   foundtype__2 <= rr_type__rritemtype__last .
H42:   foundtype__2 <> rr_type__ipv4 .
H43:   endidx__2 < zlength .
        ->
C1:    endidx__2 < zlength .
C2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_6.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
C2:    begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
C3:    begidx - begidx + endidx >= integer__base__first .
C4:    begidx - begidx + endidx <= integer__base__last .
C5:    begidx - begidx >= integer__base__first .
C6:    begidx - begidx <= integer__base__last .
 

For path(s) from assertion of line 821 to precondition check associated with statement of line 823:

procedure_parseipv4_7.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
        ->
C1:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
C2:    begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
C5:    begidx - begidx + endidx + 1 <= zlength .
 

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

procedure_parseipv4_8.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H17:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H18:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H19:   zlength >= rr_type__linelengthindex__first .
H20:   zlength <= rr_type__linelengthindex__last .
H21:   begidx - begidx + endidx + 1 <= zlength .
H22:   begidx__2 <= endidx__2 .
H23:   begidx__2 <= zlength .
H24:   endidx__2 <= zlength .
H25:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H26:   begidx__2 >= rr_type__linelengthindex__first .
H27:   begidx__2 <= rr_type__linelengthindex__last .
H28:   endidx__2 >= rr_type__linelengthindex__first .
H29:   endidx__2 <= rr_type__linelengthindex__last .
H30:   foundtype__2 >= rr_type__rritemtype__first .
H31:   foundtype__2 <= rr_type__rritemtype__last .
        ->
C1:    foundtype__2 >= rr_type__rritemtype__first .
C2:    foundtype__2 <= rr_type__rritemtype__last .
C3:    endidx__2 >= rr_type__linelengthindex__first .
C4:    endidx__2 <= rr_type__linelengthindex__last .
C5:    begidx__2 >= rr_type__linelengthindex__first .
C6:    begidx__2 <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_9.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   endidx__1 >= rr_type__linelengthindex__first .
H30:   endidx__1 <= rr_type__linelengthindex__last .
H31:   foundtype__1 >= rr_type__rritemtype__first .
H32:   foundtype__1 <= rr_type__rritemtype__last .
H33:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 < 
           zlength)) .
H34:   endidx__1 >= rr_type__linelengthindex__first .
H35:   endidx__1 <= rr_type__linelengthindex__last .
H36:   foundtype__1 >= rr_type__rritemtype__first .
H37:   foundtype__1 <= rr_type__rritemtype__last .
H38:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 >= 
           zlength)) .
H39:   begidx__1 >= rr_type__linelengthindex__first .
H40:   begidx__1 <= rr_type__linelengthindex__last .
H41:   endidx__1 >= rr_type__linelengthindex__first .
H42:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 >= rr_type__linelengthindex__first .
C2:    endidx__1 <= rr_type__linelengthindex__last .
C3:    begidx__1 >= rr_type__linelengthindex__first .
C4:    begidx__1 <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_10.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H17:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H18:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H19:   zlength >= rr_type__linelengthindex__first .
H20:   zlength <= rr_type__linelengthindex__last .
H21:   begidx - begidx + endidx + 1 <= zlength .
H22:   begidx__2 <= endidx__2 .
H23:   begidx__2 <= zlength .
H24:   endidx__2 <= zlength .
H25:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H26:   begidx__2 >= rr_type__linelengthindex__first .
H27:   begidx__2 <= rr_type__linelengthindex__last .
H28:   endidx__2 >= rr_type__linelengthindex__first .
H29:   endidx__2 <= rr_type__linelengthindex__last .
H30:   foundtype__2 >= rr_type__rritemtype__first .
H31:   foundtype__2 <= rr_type__rritemtype__last .
H32:   foundtype__2 >= rr_type__rritemtype__first .
H33:   foundtype__2 <= rr_type__rritemtype__last .
H34:   endidx__2 >= rr_type__linelengthindex__first .
H35:   endidx__2 <= rr_type__linelengthindex__last .
H36:   begidx__2 >= rr_type__linelengthindex__first .
H37:   begidx__2 <= rr_type__linelengthindex__last .
H38:   endidx__2 >= rr_type__linelengthindex__first .
H39:   endidx__2 <= rr_type__linelengthindex__last .
H40:   foundtype__2 >= rr_type__rritemtype__first .
H41:   foundtype__2 <= rr_type__rritemtype__last .
H42:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 < 
           zlength)) .
H43:   endidx__2 >= rr_type__linelengthindex__first .
H44:   endidx__2 <= rr_type__linelengthindex__last .
H45:   foundtype__2 >= rr_type__rritemtype__first .
H46:   foundtype__2 <= rr_type__rritemtype__last .
H47:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 >= 
           zlength)) .
H48:   begidx__2 >= rr_type__linelengthindex__first .
H49:   begidx__2 <= rr_type__linelengthindex__last .
H50:   endidx__2 >= rr_type__linelengthindex__first .
H51:   endidx__2 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__2 >= rr_type__linelengthindex__first .
C2:    endidx__2 <= rr_type__linelengthindex__last .
C3:    begidx__2 >= rr_type__linelengthindex__first .
C4:    begidx__2 <= rr_type__linelengthindex__last .
 

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

procedure_parseipv4_11.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   endidx__1 >= rr_type__linelengthindex__first .
H30:   endidx__1 <= rr_type__linelengthindex__last .
H31:   foundtype__1 >= rr_type__rritemtype__first .
H32:   foundtype__1 <= rr_type__rritemtype__last .
H33:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 < 
           zlength)) .
H34:   endidx__1 >= rr_type__linelengthindex__first .
H35:   endidx__1 <= rr_type__linelengthindex__last .
H36:   foundtype__1 >= rr_type__rritemtype__first .
H37:   foundtype__1 <= rr_type__rritemtype__last .
H38:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 >= 
           zlength)) .
H39:   begidx__1 >= rr_type__linelengthindex__first .
H40:   begidx__1 <= rr_type__linelengthindex__last .
H41:   endidx__1 >= rr_type__linelengthindex__first .
H42:   endidx__1 <= rr_type__linelengthindex__last .
H43:   endidx__1 >= rr_type__linelengthindex__first .
H44:   endidx__1 <= rr_type__linelengthindex__last .
H45:   begidx__1 >= rr_type__linelengthindex__first .
H46:   begidx__1 <= rr_type__linelengthindex__last .
H47:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
H48:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
C2:    parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
 

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

procedure_parseipv4_12.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H17:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H18:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H19:   zlength >= rr_type__linelengthindex__first .
H20:   zlength <= rr_type__linelengthindex__last .
H21:   begidx - begidx + endidx + 1 <= zlength .
H22:   begidx__2 <= endidx__2 .
H23:   begidx__2 <= zlength .
H24:   endidx__2 <= zlength .
H25:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H26:   begidx__2 >= rr_type__linelengthindex__first .
H27:   begidx__2 <= rr_type__linelengthindex__last .
H28:   endidx__2 >= rr_type__linelengthindex__first .
H29:   endidx__2 <= rr_type__linelengthindex__last .
H30:   foundtype__2 >= rr_type__rritemtype__first .
H31:   foundtype__2 <= rr_type__rritemtype__last .
H32:   foundtype__2 >= rr_type__rritemtype__first .
H33:   foundtype__2 <= rr_type__rritemtype__last .
H34:   endidx__2 >= rr_type__linelengthindex__first .
H35:   endidx__2 <= rr_type__linelengthindex__last .
H36:   begidx__2 >= rr_type__linelengthindex__first .
H37:   begidx__2 <= rr_type__linelengthindex__last .
H38:   endidx__2 >= rr_type__linelengthindex__first .
H39:   endidx__2 <= rr_type__linelengthindex__last .
H40:   foundtype__2 >= rr_type__rritemtype__first .
H41:   foundtype__2 <= rr_type__rritemtype__last .
H42:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 < 
           zlength)) .
H43:   endidx__2 >= rr_type__linelengthindex__first .
H44:   endidx__2 <= rr_type__linelengthindex__last .
H45:   foundtype__2 >= rr_type__rritemtype__first .
H46:   foundtype__2 <= rr_type__rritemtype__last .
H47:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 >= 
           zlength)) .
H48:   begidx__2 >= rr_type__linelengthindex__first .
H49:   begidx__2 <= rr_type__linelengthindex__last .
H50:   endidx__2 >= rr_type__linelengthindex__first .
H51:   endidx__2 <= rr_type__linelengthindex__last .
H52:   endidx__2 >= rr_type__linelengthindex__first .
H53:   endidx__2 <= rr_type__linelengthindex__last .
H54:   begidx__2 >= rr_type__linelengthindex__first .
H55:   begidx__2 <= rr_type__linelengthindex__last .
H56:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
H57:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
C2:    parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
 

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

procedure_parseipv4_13.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   endidx__1 >= rr_type__linelengthindex__first .
H30:   endidx__1 <= rr_type__linelengthindex__last .
H31:   foundtype__1 >= rr_type__rritemtype__first .
H32:   foundtype__1 <= rr_type__rritemtype__last .
H33:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 < 
           zlength)) .
H34:   endidx__1 >= rr_type__linelengthindex__first .
H35:   endidx__1 <= rr_type__linelengthindex__last .
H36:   foundtype__1 >= rr_type__rritemtype__first .
H37:   foundtype__1 <= rr_type__rritemtype__last .
H38:   not ((foundtype__1 <> rr_type__ipv4) and (endidx__1 >= 
           zlength)) .
H39:   begidx__1 >= rr_type__linelengthindex__first .
H40:   begidx__1 <= rr_type__linelengthindex__last .
H41:   endidx__1 >= rr_type__linelengthindex__first .
H42:   endidx__1 <= rr_type__linelengthindex__last .
H43:   endidx__1 >= rr_type__linelengthindex__first .
H44:   endidx__1 <= rr_type__linelengthindex__last .
H45:   begidx__1 >= rr_type__linelengthindex__first .
H46:   begidx__1 <= rr_type__linelengthindex__last .
H47:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
H48:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
H49:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
H50:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
H51:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
H52:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
H53:   not (parser_utilities__convertipv4(zonefileline, begidx__1, 
           endidx__1) = 0) .
H54:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
H55:   parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) >= 
           unsigned_types__unsigned32__first .
C2:    parser_utilities__convertipv4(zonefileline, begidx__1, endidx__1) <= 
           unsigned_types__unsigned32__last .
 

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

procedure_parseipv4_14.
H1:    endidx < zlength .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H3:    zlength >= rr_type__linelengthindex__first .
H4:    zlength <= rr_type__linelengthindex__last .
H5:    begidx >= rr_type__linelengthindex__first .
H6:    begidx <= rr_type__linelengthindex__last .
H7:    endidx >= rr_type__linelengthindex__first .
H8:    endidx <= rr_type__linelengthindex__last .
H9:    begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H10:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H11:   begidx - begidx + endidx >= integer__base__first .
H12:   begidx - begidx + endidx <= integer__base__last .
H13:   begidx - begidx >= integer__base__first .
H14:   begidx - begidx <= integer__base__last .
H15:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H16:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H17:   begidx - begidx + endidx + 1 >= 
           rr_type__linelengthindex__first .
H18:   begidx - begidx + endidx + 1 <= 
           rr_type__linelengthindex__last .
H19:   zlength >= rr_type__linelengthindex__first .
H20:   zlength <= rr_type__linelengthindex__last .
H21:   begidx - begidx + endidx + 1 <= zlength .
H22:   begidx__2 <= endidx__2 .
H23:   begidx__2 <= zlength .
H24:   endidx__2 <= zlength .
H25:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H26:   begidx__2 >= rr_type__linelengthindex__first .
H27:   begidx__2 <= rr_type__linelengthindex__last .
H28:   endidx__2 >= rr_type__linelengthindex__first .
H29:   endidx__2 <= rr_type__linelengthindex__last .
H30:   foundtype__2 >= rr_type__rritemtype__first .
H31:   foundtype__2 <= rr_type__rritemtype__last .
H32:   foundtype__2 >= rr_type__rritemtype__first .
H33:   foundtype__2 <= rr_type__rritemtype__last .
H34:   endidx__2 >= rr_type__linelengthindex__first .
H35:   endidx__2 <= rr_type__linelengthindex__last .
H36:   begidx__2 >= rr_type__linelengthindex__first .
H37:   begidx__2 <= rr_type__linelengthindex__last .
H38:   endidx__2 >= rr_type__linelengthindex__first .
H39:   endidx__2 <= rr_type__linelengthindex__last .
H40:   foundtype__2 >= rr_type__rritemtype__first .
H41:   foundtype__2 <= rr_type__rritemtype__last .
H42:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 < 
           zlength)) .
H43:   endidx__2 >= rr_type__linelengthindex__first .
H44:   endidx__2 <= rr_type__linelengthindex__last .
H45:   foundtype__2 >= rr_type__rritemtype__first .
H46:   foundtype__2 <= rr_type__rritemtype__last .
H47:   not ((foundtype__2 <> rr_type__ipv4) and (endidx__2 >= 
           zlength)) .
H48:   begidx__2 >= rr_type__linelengthindex__first .
H49:   begidx__2 <= rr_type__linelengthindex__last .
H50:   endidx__2 >= rr_type__linelengthindex__first .
H51:   endidx__2 <= rr_type__linelengthindex__last .
H52:   endidx__2 >= rr_type__linelengthindex__first .
H53:   endidx__2 <= rr_type__linelengthindex__last .
H54:   begidx__2 >= rr_type__linelengthindex__first .
H55:   begidx__2 <= rr_type__linelengthindex__last .
H56:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
H57:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
H58:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
H59:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
H60:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
H61:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
H62:   not (parser_utilities__convertipv4(zonefileline, begidx__2, 
           endidx__2) = 0) .
H63:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
H64:   parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) >= 
           unsigned_types__unsigned32__first .
C2:    parser_utilities__convertipv4(zonefileline, begidx__2, endidx__2) <= 
           unsigned_types__unsigned32__last .
 

For path(s) from start to finish:

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


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


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


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

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


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


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


