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

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


                     function Parser_Utilities.isClass




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

function_isclass_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    endidx - 1 >= integer__base__first .
C2:    endidx - 1 <= integer__base__last .
 

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

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

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

function_isclass_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx - 1 >= integer__base__first .
H7:    endidx - 1 <= integer__base__last .
H8:    begidx = endidx - 1 .
H9:    element(s, [begidx]) >= character__first .
H10:   element(s, [begidx]) <= character__last .
H11:   begidx >= rr_type__linelengthindex__first .
H12:   begidx <= rr_type__linelengthindex__last .
H13:   1 >= two_range__first .
H14:   1 <= two_range__last .
H15:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H16:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
        ->
C1:    ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
C2:    ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
 

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

function_isclass_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx - 1 >= integer__base__first .
H7:    endidx - 1 <= integer__base__last .
H8:    begidx = endidx - 1 .
H9:    element(s, [begidx]) >= character__first .
H10:   element(s, [begidx]) <= character__last .
H11:   begidx >= rr_type__linelengthindex__first .
H12:   begidx <= rr_type__linelengthindex__last .
H13:   1 >= two_range__first .
H14:   1 <= two_range__last .
H15:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H16:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H17:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H18:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
        ->
C1:    element(s, [endidx]) >= character__first .
C2:    element(s, [endidx]) <= character__last .
C3:    endidx >= rr_type__linelengthindex__first .
C4:    endidx <= rr_type__linelengthindex__last .
C5:    2 >= two_range__first .
C6:    2 <= two_range__last .
 

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

function_isclass_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx - 1 >= integer__base__first .
H7:    endidx - 1 <= integer__base__last .
H8:    begidx = endidx - 1 .
H9:    element(s, [begidx]) >= character__first .
H10:   element(s, [begidx]) <= character__last .
H11:   begidx >= rr_type__linelengthindex__first .
H12:   begidx <= rr_type__linelengthindex__last .
H13:   1 >= two_range__first .
H14:   1 <= two_range__last .
H15:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H16:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H17:   ada__characters__handling__to_upper(element(s, [
           begidx])) >= character__first .
H18:   ada__characters__handling__to_upper(element(s, [
           begidx])) <= character__last .
H19:   element(s, [endidx]) >= character__first .
H20:   element(s, [endidx]) <= character__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   2 >= two_range__first .
H24:   2 <= two_range__last .
H25:   ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
H26:   ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
        ->
C1:    ada__characters__handling__to_upper(element(s, [
           endidx])) >= character__first .
C2:    ada__characters__handling__to_upper(element(s, [
           endidx])) <= character__last .
 

For path(s) from start to finish:

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


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


