ironsides/parser_utilities/isrecord.vcg

5251 lines
255 KiB
Plaintext

*******************************************************
Semantic Analysis of SPARK Text
Examiner GPL Edition
*******************************************************
function Parser_Utilities.isRecord
For path(s) from start to run-time check associated with statement of line 70:
function_isrecord_1.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
C2: element(s, [begidx]) <= character__last .
C3: begidx >= rr_type__linelengthindex__first .
C4: begidx <= rr_type__linelengthindex__last .
For path(s) from start to run-time check associated with statement of line 70:
function_isrecord_2.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: 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 71:
function_isrecord_3.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: 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 .
For path(s) from start to run-time check associated with statement of line 71:
function_isrecord_4.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: 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 run-time check associated with statement of line 72:
function_isrecord_5.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - begidx + 1 >= rr_type__linelengthindex__first .
C2: endidx - begidx + 1 <= rr_type__linelengthindex__last .
C3: endidx - begidx >= integer__base__first .
C4: endidx - begidx <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 88:
function_isrecord_6.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 2 >= integer__base__first .
C2: endidx - 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 89:
function_isrecord_7.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: ada__characters__handling__to_upper(element(s, [
begidx])) = 80 .
H60: ada__characters__handling__to_upper(element(s, [
endidx])) = 82 .
H61: begidx <= endidx - 2 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 96:
function_isrecord_8.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 2 >= integer__base__first .
C2: endidx - 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 97:
function_isrecord_9.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: ada__characters__handling__to_upper(element(s, [
begidx])) = 83 .
H67: ada__characters__handling__to_upper(element(s, [
endidx])) = 65 .
H68: begidx <= endidx - 2 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 104:
function_isrecord_10.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 2 >= integer__base__first .
C2: endidx - 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 105:
function_isrecord_11.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: ada__characters__handling__to_upper(element(s, [
begidx])) = 83 .
H74: ada__characters__handling__to_upper(element(s, [
endidx])) = 86 .
H75: begidx <= endidx - 2 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 112:
function_isrecord_12.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 2 >= integer__base__first .
C2: endidx - 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 113:
function_isrecord_13.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: ada__characters__handling__to_upper(element(s, [
begidx])) = 84 .
H81: ada__characters__handling__to_upper(element(s, [
endidx])) = 84 .
H82: begidx <= endidx - 2 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 120:
function_isrecord_14.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 3 >= integer__base__first .
C2: endidx - 3 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 121:
function_isrecord_15.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: ada__characters__handling__to_upper(element(s, [
begidx])) = 65 .
H88: ada__characters__handling__to_upper(element(s, [
endidx])) = 65 .
H89: begidx <= endidx - 3 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 121:
function_isrecord_16.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: ada__characters__handling__to_upper(element(s, [
begidx])) = 65 .
H88: ada__characters__handling__to_upper(element(s, [
endidx])) = 65 .
H89: begidx <= endidx - 3 .
H90: element(s, [begidx + 1]) >= character__first .
H91: element(s, [begidx + 1]) <= character__last .
H92: begidx + 1 >= rr_type__linelengthindex__first .
H93: begidx + 1 <= rr_type__linelengthindex__last .
H94: begidx + 1 >= integer__base__first .
H95: begidx + 1 <= integer__base__last .
H96: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H97: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
->
C1: element(s, [begidx + 2]) >= character__first .
C2: element(s, [begidx + 2]) <= character__last .
C3: begidx + 2 >= rr_type__linelengthindex__first .
C4: begidx + 2 <= rr_type__linelengthindex__last .
C5: begidx + 2 >= integer__base__first .
C6: begidx + 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 130:
function_isrecord_17.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 3 >= integer__base__first .
C2: endidx - 3 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 131:
function_isrecord_18.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: ada__characters__handling__to_upper(element(s, [
begidx])) = 78 .
H95: ada__characters__handling__to_upper(element(s, [
endidx])) = 67 .
H96: begidx <= endidx - 3 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 131:
function_isrecord_19.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: ada__characters__handling__to_upper(element(s, [
begidx])) = 78 .
H95: ada__characters__handling__to_upper(element(s, [
endidx])) = 67 .
H96: begidx <= endidx - 3 .
H97: element(s, [begidx + 1]) >= character__first .
H98: element(s, [begidx + 1]) <= character__last .
H99: begidx + 1 >= rr_type__linelengthindex__first .
H100: begidx + 1 <= rr_type__linelengthindex__last .
H101: begidx + 1 >= integer__base__first .
H102: begidx + 1 <= integer__base__last .
H103: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H104: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
->
C1: element(s, [begidx + 2]) >= character__first .
C2: element(s, [begidx + 2]) <= character__last .
C3: begidx + 2 >= rr_type__linelengthindex__first .
C4: begidx + 2 <= rr_type__linelengthindex__last .
C5: begidx + 2 >= integer__base__first .
C6: begidx + 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 140:
function_isrecord_20.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 4 >= integer__base__first .
C2: endidx - 4 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 141:
function_isrecord_21.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: ada__characters__handling__to_upper(element(s, [
begidx])) = 67 .
H102: ada__characters__handling__to_upper(element(s, [
endidx])) = 69 .
H103: begidx <= endidx - 4 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 141:
function_isrecord_22.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: ada__characters__handling__to_upper(element(s, [
begidx])) = 67 .
H102: ada__characters__handling__to_upper(element(s, [
endidx])) = 69 .
H103: begidx <= endidx - 4 .
H104: element(s, [begidx + 1]) >= character__first .
H105: element(s, [begidx + 1]) <= character__last .
H106: begidx + 1 >= rr_type__linelengthindex__first .
H107: begidx + 1 <= rr_type__linelengthindex__last .
H108: begidx + 1 >= integer__base__first .
H109: begidx + 1 <= integer__base__last .
H110: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H111: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
->
C1: element(s, [begidx + 2]) >= character__first .
C2: element(s, [begidx + 2]) <= character__last .
C3: begidx + 2 >= rr_type__linelengthindex__first .
C4: begidx + 2 <= rr_type__linelengthindex__last .
C5: begidx + 2 >= integer__base__first .
C6: begidx + 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 141:
function_isrecord_23.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: ada__characters__handling__to_upper(element(s, [
begidx])) = 67 .
H102: ada__characters__handling__to_upper(element(s, [
endidx])) = 69 .
H103: begidx <= endidx - 4 .
H104: element(s, [begidx + 1]) >= character__first .
H105: element(s, [begidx + 1]) <= character__last .
H106: begidx + 1 >= rr_type__linelengthindex__first .
H107: begidx + 1 <= rr_type__linelengthindex__last .
H108: begidx + 1 >= integer__base__first .
H109: begidx + 1 <= integer__base__last .
H110: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H111: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
H112: element(s, [begidx + 2]) >= character__first .
H113: element(s, [begidx + 2]) <= character__last .
H114: begidx + 2 >= rr_type__linelengthindex__first .
H115: begidx + 2 <= rr_type__linelengthindex__last .
H116: begidx + 2 >= integer__base__first .
H117: begidx + 2 <= integer__base__last .
H118: ada__characters__handling__to_upper(element(s, [
begidx + 2])) >= character__first .
H119: ada__characters__handling__to_upper(element(s, [
begidx + 2])) <= character__last .
->
C1: element(s, [begidx + 3]) >= character__first .
C2: element(s, [begidx + 3]) <= character__last .
C3: begidx + 3 >= rr_type__linelengthindex__first .
C4: begidx + 3 <= rr_type__linelengthindex__last .
C5: begidx + 3 >= integer__base__first .
C6: begidx + 3 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 151:
function_isrecord_24.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 4 >= integer__base__first .
C2: endidx - 4 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 152:
function_isrecord_25.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: ada__characters__handling__to_upper(element(s, [
begidx])) = 82 .
H109: ada__characters__handling__to_upper(element(s, [
endidx])) = 71 .
H110: begidx <= endidx - 4 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 152:
function_isrecord_26.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: ada__characters__handling__to_upper(element(s, [
begidx])) = 82 .
H109: ada__characters__handling__to_upper(element(s, [
endidx])) = 71 .
H110: begidx <= endidx - 4 .
H111: element(s, [begidx + 1]) >= character__first .
H112: element(s, [begidx + 1]) <= character__last .
H113: begidx + 1 >= rr_type__linelengthindex__first .
H114: begidx + 1 <= rr_type__linelengthindex__last .
H115: begidx + 1 >= integer__base__first .
H116: begidx + 1 <= integer__base__last .
H117: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H118: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
->
C1: element(s, [begidx + 2]) >= character__first .
C2: element(s, [begidx + 2]) <= character__last .
C3: begidx + 2 >= rr_type__linelengthindex__first .
C4: begidx + 2 <= rr_type__linelengthindex__last .
C5: begidx + 2 >= integer__base__first .
C6: begidx + 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 152:
function_isrecord_27.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: ada__characters__handling__to_upper(element(s, [
begidx])) = 82 .
H109: ada__characters__handling__to_upper(element(s, [
endidx])) = 71 .
H110: begidx <= endidx - 4 .
H111: element(s, [begidx + 1]) >= character__first .
H112: element(s, [begidx + 1]) <= character__last .
H113: begidx + 1 >= rr_type__linelengthindex__first .
H114: begidx + 1 <= rr_type__linelengthindex__last .
H115: begidx + 1 >= integer__base__first .
H116: begidx + 1 <= integer__base__last .
H117: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H118: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
H119: element(s, [begidx + 2]) >= character__first .
H120: element(s, [begidx + 2]) <= character__last .
H121: begidx + 2 >= rr_type__linelengthindex__first .
H122: begidx + 2 <= rr_type__linelengthindex__last .
H123: begidx + 2 >= integer__base__first .
H124: begidx + 2 <= integer__base__last .
H125: ada__characters__handling__to_upper(element(s, [
begidx + 2])) >= character__first .
H126: ada__characters__handling__to_upper(element(s, [
begidx + 2])) <= character__last .
->
C1: element(s, [begidx + 3]) >= character__first .
C2: element(s, [begidx + 3]) <= character__last .
C3: begidx + 3 >= rr_type__linelengthindex__first .
C4: begidx + 3 <= rr_type__linelengthindex__last .
C5: begidx + 3 >= integer__base__first .
C6: begidx + 3 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 162:
function_isrecord_28.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 71) and (begidx <= endidx - 4))) .
H109: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H110: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H111: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H112: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
->
C1: endidx - 5 >= integer__base__first .
C2: endidx - 5 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 163:
function_isrecord_29.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 71) and (begidx <= endidx - 4))) .
H109: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H110: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H111: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H112: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H113: endidx - 5 >= integer__base__first .
H114: endidx - 5 <= integer__base__last .
H115: ada__characters__handling__to_upper(element(s, [
begidx])) = 68 .
H116: ada__characters__handling__to_upper(element(s, [
endidx])) = 89 .
H117: begidx <= endidx - 5 .
->
C1: element(s, [begidx + 1]) >= character__first .
C2: element(s, [begidx + 1]) <= character__last .
C3: begidx + 1 >= rr_type__linelengthindex__first .
C4: begidx + 1 <= rr_type__linelengthindex__last .
C5: begidx + 1 >= integer__base__first .
C6: begidx + 1 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 163:
function_isrecord_30.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 71) and (begidx <= endidx - 4))) .
H109: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H110: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H111: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H112: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H113: endidx - 5 >= integer__base__first .
H114: endidx - 5 <= integer__base__last .
H115: ada__characters__handling__to_upper(element(s, [
begidx])) = 68 .
H116: ada__characters__handling__to_upper(element(s, [
endidx])) = 89 .
H117: begidx <= endidx - 5 .
H118: element(s, [begidx + 1]) >= character__first .
H119: element(s, [begidx + 1]) <= character__last .
H120: begidx + 1 >= rr_type__linelengthindex__first .
H121: begidx + 1 <= rr_type__linelengthindex__last .
H122: begidx + 1 >= integer__base__first .
H123: begidx + 1 <= integer__base__last .
H124: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H125: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
->
C1: element(s, [begidx + 2]) >= character__first .
C2: element(s, [begidx + 2]) <= character__last .
C3: begidx + 2 >= rr_type__linelengthindex__first .
C4: begidx + 2 <= rr_type__linelengthindex__last .
C5: begidx + 2 >= integer__base__first .
C6: begidx + 2 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 163:
function_isrecord_31.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 71) and (begidx <= endidx - 4))) .
H109: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H110: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H111: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H112: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H113: endidx - 5 >= integer__base__first .
H114: endidx - 5 <= integer__base__last .
H115: ada__characters__handling__to_upper(element(s, [
begidx])) = 68 .
H116: ada__characters__handling__to_upper(element(s, [
endidx])) = 89 .
H117: begidx <= endidx - 5 .
H118: element(s, [begidx + 1]) >= character__first .
H119: element(s, [begidx + 1]) <= character__last .
H120: begidx + 1 >= rr_type__linelengthindex__first .
H121: begidx + 1 <= rr_type__linelengthindex__last .
H122: begidx + 1 >= integer__base__first .
H123: begidx + 1 <= integer__base__last .
H124: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H125: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
H126: element(s, [begidx + 2]) >= character__first .
H127: element(s, [begidx + 2]) <= character__last .
H128: begidx + 2 >= rr_type__linelengthindex__first .
H129: begidx + 2 <= rr_type__linelengthindex__last .
H130: begidx + 2 >= integer__base__first .
H131: begidx + 2 <= integer__base__last .
H132: ada__characters__handling__to_upper(element(s, [
begidx + 2])) >= character__first .
H133: ada__characters__handling__to_upper(element(s, [
begidx + 2])) <= character__last .
->
C1: element(s, [begidx + 3]) >= character__first .
C2: element(s, [begidx + 3]) <= character__last .
C3: begidx + 3 >= rr_type__linelengthindex__first .
C4: begidx + 3 <= rr_type__linelengthindex__last .
C5: begidx + 3 >= integer__base__first .
C6: begidx + 3 <= integer__base__last .
For path(s) from start to run-time check associated with statement of line 163:
function_isrecord_32.
H1: begidx <= endidx .
H2: 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))) .
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: element(s, [begidx]) >= character__first .
H8: element(s, [begidx]) <= character__last .
H9: begidx >= rr_type__linelengthindex__first .
H10: begidx <= rr_type__linelengthindex__last .
H11: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H12: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H13: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H14: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H15: element(s, [endidx]) >= character__first .
H16: element(s, [endidx]) <= character__last .
H17: endidx >= rr_type__linelengthindex__first .
H18: endidx <= rr_type__linelengthindex__last .
H19: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H20: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H21: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H22: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H23: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H24: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H25: endidx - begidx >= integer__base__first .
H26: endidx - begidx <= integer__base__last .
H27: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H28: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H29: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H30: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H31: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and (endidx - begidx + 1 = 1)) .
H32: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H33: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H34: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H35: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H36: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H37: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H38: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 83) and (endidx - begidx + 1 = 2))) .
H39: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H40: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H41: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H42: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H43: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H44: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H45: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 77) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 88) and (endidx - begidx + 1 = 2))) .
H46: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H47: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H48: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H49: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H50: endidx - begidx + 1 >= rr_type__linelengthindex__first .
H51: endidx - begidx + 1 <= rr_type__linelengthindex__last .
H52: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 80) and (endidx - begidx + 1 = 2))) .
H53: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H54: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H55: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H56: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H57: endidx - 2 >= integer__base__first .
H58: endidx - 2 <= integer__base__last .
H59: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 80) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 82) and (begidx <= endidx - 2))) .
H60: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H61: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H62: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H63: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H64: endidx - 2 >= integer__base__first .
H65: endidx - 2 <= integer__base__last .
H66: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 2))) .
H67: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H68: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H69: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H70: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H71: endidx - 2 >= integer__base__first .
H72: endidx - 2 <= integer__base__last .
H73: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 83) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 86) and (begidx <= endidx - 2))) .
H74: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H75: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H76: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H77: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H78: endidx - 2 >= integer__base__first .
H79: endidx - 2 <= integer__base__last .
H80: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 84) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 84) and (begidx <= endidx - 2))) .
H81: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H82: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H83: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H84: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H85: endidx - 3 >= integer__base__first .
H86: endidx - 3 <= integer__base__last .
H87: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 65) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 65) and (begidx <= endidx - 3))) .
H88: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H89: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H90: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H91: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H92: endidx - 3 >= integer__base__first .
H93: endidx - 3 <= integer__base__last .
H94: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 78) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 67) and (begidx <= endidx - 3))) .
H95: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H96: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H97: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H98: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H99: endidx - 4 >= integer__base__first .
H100: endidx - 4 <= integer__base__last .
H101: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 67) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 69) and (begidx <= endidx - 4))) .
H102: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H103: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H104: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H105: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H106: endidx - 4 >= integer__base__first .
H107: endidx - 4 <= integer__base__last .
H108: not ((ada__characters__handling__to_upper(element(s, [
begidx])) = 82) and ((
ada__characters__handling__to_upper(element(s, [
endidx])) = 71) and (begidx <= endidx - 4))) .
H109: ada__characters__handling__to_upper(element(s, [
begidx])) >= character__first .
H110: ada__characters__handling__to_upper(element(s, [
begidx])) <= character__last .
H111: ada__characters__handling__to_upper(element(s, [
endidx])) >= character__first .
H112: ada__characters__handling__to_upper(element(s, [
endidx])) <= character__last .
H113: endidx - 5 >= integer__base__first .
H114: endidx - 5 <= integer__base__last .
H115: ada__characters__handling__to_upper(element(s, [
begidx])) = 68 .
H116: ada__characters__handling__to_upper(element(s, [
endidx])) = 89 .
H117: begidx <= endidx - 5 .
H118: element(s, [begidx + 1]) >= character__first .
H119: element(s, [begidx + 1]) <= character__last .
H120: begidx + 1 >= rr_type__linelengthindex__first .
H121: begidx + 1 <= rr_type__linelengthindex__last .
H122: begidx + 1 >= integer__base__first .
H123: begidx + 1 <= integer__base__last .
H124: ada__characters__handling__to_upper(element(s, [
begidx + 1])) >= character__first .
H125: ada__characters__handling__to_upper(element(s, [
begidx + 1])) <= character__last .
H126: element(s, [begidx + 2]) >= character__first .
H127: element(s, [begidx + 2]) <= character__last .
H128: begidx + 2 >= rr_type__linelengthindex__first .
H129: begidx + 2 <= rr_type__linelengthindex__last .
H130: begidx + 2 >= integer__base__first .
H131: begidx + 2 <= integer__base__last .
H132: ada__characters__handling__to_upper(element(s, [
begidx + 2])) >= character__first .
H133: ada__characters__handling__to_upper(element(s, [
begidx + 2])) <= character__last .
H134: element(s, [begidx + 3]) >= character__first .
H135: element(s, [begidx + 3]) <= character__last .
H136: begidx + 3 >= rr_type__linelengthindex__first .
H137: begidx + 3 <= rr_type__linelengthindex__last .
H138: begidx + 3 >= integer__base__first .
H139: begidx + 3 <= integer__base__last .
H140: ada__characters__handling__to_upper(element(s, [
begidx + 3])) >= character__first .
H141: ada__characters__handling__to_upper(element(s, [
begidx + 3])) <= character__last .
->
C1: element(s, [begidx + 4]) >= character__first .
C2: element(s, [begidx + 4]) <= character__last .
C3: begidx + 4 >= rr_type__linelengthindex__first .
C4: begidx + 4 <= rr_type__linelengthindex__last .
C5: begidx + 4 >= integer__base__first .
C6: begidx + 4 <= integer__base__last .
For path(s) from start to finish:
function_isrecord_33.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_34.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_35.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_36.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_37.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_38.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_39.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_40.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_41.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_42.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_43.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_44.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_45.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_46.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_47.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_48.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_49.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_50.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_51.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_52.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_53.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_54.
*** true . /* trivially true VC removed by Examiner */
function_isrecord_55.
*** true . /* trivially true VC removed by Examiner */