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

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


              procedure Parser_Utilities.convert16BitUnsigned




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

procedure_convert16bitunsigned_1.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

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

procedure_convert16bitunsigned_2.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    0 >= natural__first .
H8:    0 <= natural__last .
        ->
C1:    0 >= unsigned_types__unsigned16__first .
C2:    0 <= unsigned_types__unsigned16__last .
 

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

procedure_convert16bitunsigned_3.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    0 >= natural__first .
H8:    0 <= natural__last .
H9:    0 >= unsigned_types__unsigned16__first .
H10:   0 <= unsigned_types__unsigned16__last .
        ->
C1:    endidx >= integer__first .
C2:    endidx <= integer__last .
C3:    begidx >= integer__first .
C4:    begidx <= integer__last .
 

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

procedure_convert16bitunsigned_4.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    0 >= natural__first .
H8:    0 <= natural__last .
H9:    0 >= unsigned_types__unsigned16__first .
H10:   0 <= unsigned_types__unsigned16__last .
H11:   endidx >= integer__first .
H12:   endidx <= integer__last .
H13:   begidx >= integer__first .
H14:   begidx <= integer__last .
        ->
C1:    (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
C2:    (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
 

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

procedure_convert16bitunsigned_5.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    0 >= natural__first .
H8:    0 <= natural__last .
H9:    0 >= unsigned_types__unsigned16__first .
H10:   0 <= unsigned_types__unsigned16__last .
H11:   endidx >= integer__first .
H12:   endidx <= integer__last .
H13:   begidx >= integer__first .
H14:   begidx <= integer__last .
H15:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H16:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H17:   begidx <= endidx .
        ->
C1:    begidx >= 1 .
C2:    0 <= unsigned_types__max_16bit_val .
C3:    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))) .
C4:    begidx >= rr_type__linelengthindex__first .
C5:    begidx <= rr_type__linelengthindex__last .
C6:    endidx >= rr_type__linelengthindex__first .
C7:    endidx <= rr_type__linelengthindex__last .
C8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
C9:    begidx >= integer__first .
C10:   begidx <= integer__last .
C11:   begidx >= begidx .
C12:   begidx <= endidx .
 

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

procedure_convert16bitunsigned_6.
H1:    begidx >= 1 .
H2:    tmpval <= unsigned_types__max_16bit_val .
H3:    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))) .
H4:    begidx >= rr_type__linelengthindex__first .
H5:    begidx <= rr_type__linelengthindex__last .
H6:    endidx >= rr_type__linelengthindex__first .
H7:    endidx <= rr_type__linelengthindex__last .
H8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx .
H13:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H14:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H18:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H19:   tmpval >= natural__first .
H20:   tmpval <= natural__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H23:   10 * tmpval >= integer__base__first .
H24:   10 * tmpval <= integer__base__last .
H25:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H27:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) > 
           unsigned_types__max_16bit_val) .
H28:   not (loop__1__i = endidx) .
        ->
C1:    begidx >= 1 .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           unsigned_types__max_16bit_val .
C3:    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))) .
C4:    begidx >= rr_type__linelengthindex__first .
C5:    begidx <= rr_type__linelengthindex__last .
C6:    endidx >= rr_type__linelengthindex__first .
C7:    endidx <= rr_type__linelengthindex__last .
C8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
C9:    loop__1__i + 1 >= integer__first .
C10:   loop__1__i + 1 <= integer__last .
C11:   loop__1__i + 1 >= begidx .
C12:   loop__1__i + 1 <= endidx .
 

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

procedure_convert16bitunsigned_7.
H1:    begidx >= 1 .
H2:    tmpval <= unsigned_types__max_16bit_val .
H3:    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))) .
H4:    begidx >= rr_type__linelengthindex__first .
H5:    begidx <= rr_type__linelengthindex__last .
H6:    endidx >= rr_type__linelengthindex__first .
H7:    endidx <= rr_type__linelengthindex__last .
H8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx .
        ->
C1:    element(zonefileline, [loop__1__i]) - 48 >= natural__first .
C2:    element(zonefileline, [loop__1__i]) - 48 <= natural__last .
C3:    loop__1__i >= rr_type__linelengthindex__first .
C4:    loop__1__i <= rr_type__linelengthindex__last .
 

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

procedure_convert16bitunsigned_8.
H1:    begidx >= 1 .
H2:    tmpval <= unsigned_types__max_16bit_val .
H3:    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))) .
H4:    begidx >= rr_type__linelengthindex__first .
H5:    begidx <= rr_type__linelengthindex__last .
H6:    endidx >= rr_type__linelengthindex__first .
H7:    endidx <= rr_type__linelengthindex__last .
H8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx .
H13:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H14:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H18:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H19:   tmpval >= natural__first .
H20:   tmpval <= natural__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * tmpval >= integer__base__first .
C4:    10 * tmpval <= integer__base__last .
 

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

procedure_convert16bitunsigned_9.
H1:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
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:    begidx >= rr_type__linelengthindex__first .
H4:    begidx <= rr_type__linelengthindex__last .
H5:    endidx >= rr_type__linelengthindex__first .
H6:    endidx <= rr_type__linelengthindex__last .
H7:    0 >= natural__first .
H8:    0 <= natural__last .
H9:    0 >= unsigned_types__unsigned16__first .
H10:   0 <= unsigned_types__unsigned16__last .
H11:   endidx >= integer__first .
H12:   endidx <= integer__last .
H13:   begidx >= integer__first .
H14:   begidx <= integer__last .
H15:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H16:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H17:   not (begidx <= endidx) .
H18:   0 >= natural__first .
H19:   0 <= natural__last .
H20:   not (0 > unsigned_types__max_16bit_val) .
H21:   0 >= natural__first .
H22:   0 <= natural__last .
        ->
C1:    0 >= unsigned_types__unsigned16__first .
C2:    0 <= unsigned_types__unsigned16__last .
C3:    0 >= unsigned_types__unsigned16__first .
C4:    0 <= unsigned_types__unsigned16__last .
 

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

procedure_convert16bitunsigned_10.
H1:    begidx >= 1 .
H2:    tmpval <= unsigned_types__max_16bit_val .
H3:    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))) .
H4:    begidx >= rr_type__linelengthindex__first .
H5:    begidx <= rr_type__linelengthindex__last .
H6:    endidx >= rr_type__linelengthindex__first .
H7:    endidx <= rr_type__linelengthindex__last .
H8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx .
H13:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H14:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H18:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H19:   tmpval >= natural__first .
H20:   tmpval <= natural__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H23:   10 * tmpval >= integer__base__first .
H24:   10 * tmpval <= integer__base__last .
H25:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) > 
           unsigned_types__max_16bit_val .
H28:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H29:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H30:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) > 
           unsigned_types__max_16bit_val) .
H31:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H32:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned16__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned16__last .
C3:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned16__first .
C4:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned16__last .
 

procedure_convert16bitunsigned_11.
H1:    begidx >= 1 .
H2:    tmpval <= unsigned_types__max_16bit_val .
H3:    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))) .
H4:    begidx >= rr_type__linelengthindex__first .
H5:    begidx <= rr_type__linelengthindex__last .
H6:    endidx >= rr_type__linelengthindex__first .
H7:    endidx <= rr_type__linelengthindex__last .
H8:    for_all(i_: integer, ((i_ >= begidx) and (i_ <= 
           endidx)) -> ((element(zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57))) .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx .
H13:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H14:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   element(zonefileline, [loop__1__i]) - 48 >= natural__first .
H18:   element(zonefileline, [loop__1__i]) - 48 <= natural__last .
H19:   tmpval >= natural__first .
H20:   tmpval <= natural__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H23:   10 * tmpval >= integer__base__first .
H24:   10 * tmpval <= integer__base__last .
H25:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H27:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) > 
           unsigned_types__max_16bit_val) .
H28:   loop__1__i = endidx .
H29:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
H31:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) > 
           unsigned_types__max_16bit_val) .
H32:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           natural__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned16__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned16__last .
C3:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned16__first .
C4:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned16__last .
 

For path(s) from start to finish:

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


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


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

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


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


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


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


