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

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


                    procedure Parser_Utilities.AddToKey




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

procedure_addtokey_1.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
        ->
C1:    1 >= rr_type__linelengthindex__first .
C2:    1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_2.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
        ->
C1:    (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
C2:    (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
 

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

procedure_addtokey_3.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
C2:    (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
 

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

procedure_addtokey_4.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   1 < length .
H24:   (element(s, [1]) = blank) or (element(s, [1]) = tab) .
        ->
C1:    1 >= 1 .
C2:    1 < length .
C3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C16:   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))) .
C17:   length >= rr_type__linelengthindex__first .
C18:   length <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_5.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   begidx + 1 < length .
H28:   (element(s, [begidx + 1]) = blank) or (element(s, [
           begidx + 1]) = tab) .
        ->
C1:    begidx + 1 >= 1 .
C2:    begidx + 1 < length .
C3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C16:   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))) .
C17:   length >= rr_type__linelengthindex__first .
C18:   length <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_6.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
        ->
C1:    begidx + 1 >= rr_type__linelengthindex__first .
C2:    begidx + 1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_7.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
        ->
C1:    1 >= rr_type__linelengthindex__first .
C2:    1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_8.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    begidx + 1 >= rr_type__linelengthindex__first .
C2:    begidx + 1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_9.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
        ->
C1:    (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
C2:    (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
 

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

procedure_addtokey_10.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
C2:    (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
 

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

procedure_addtokey_11.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
C2:    (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
 

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

procedure_addtokey_12.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   1 < length .
H33:   element(s, [1]) <> blank .
H34:   element(s, [1]) <> tab .
        ->
C1:    1 >= 1 .
C2:    1 <= 1 .
C3:    1 >= 1 .
C4:    1 < length .
C5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C18:   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))) .
C19:   length >= rr_type__linelengthindex__first .
C20:   length <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 791 to assertion of line 798:

procedure_addtokey_13.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   begidx + 1 < length .
H37:   element(s, [begidx + 1]) <> blank .
H38:   element(s, [begidx + 1]) <> tab .
        ->
C1:    begidx + 1 >= 1 .
C2:    begidx + 1 <= begidx + 1 .
C3:    begidx + 1 >= 1 .
C4:    begidx + 1 < length .
C5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C18:   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))) .
C19:   length >= rr_type__linelengthindex__first .
C20:   length <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_14.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   endidx + 1 < length .
H30:   element(s, [endidx + 1]) <> blank .
H31:   element(s, [endidx + 1]) <> tab .
        ->
C1:    begidx >= 1 .
C2:    begidx <= endidx + 1 .
C3:    endidx + 1 >= 1 .
C4:    endidx + 1 < length .
C5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C18:   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))) .
C19:   length >= rr_type__linelengthindex__first .
C20:   length <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_15.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
        ->
C1:    endidx + 1 >= rr_type__linelengthindex__first .
C2:    endidx + 1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_16.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   not ((1 < length) and ((element(s, [1]) <> blank) and (element(
           s, [1]) <> tab))) .
H33:   1 >= rr_type__linelengthindex__first .
H34:   1 <= rr_type__linelengthindex__last .
H35:   1 >= rr_type__linelengthindex__first .
H36:   1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (1 - 1 + 1) >= integer__base__first .
C2:    fld_keylength(dnskey_rec) + (1 - 1 + 1) <= integer__base__last .
C3:    1 - 1 + 1 >= integer__base__first .
C4:    1 - 1 + 1 <= integer__base__last .
C5:    1 - 1 >= integer__base__first .
C6:    1 - 1 <= integer__base__last .
 

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

procedure_addtokey_17.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) <> 
           blank) and (element(s, [begidx + 1]) <> tab))) .
H37:   begidx + 1 >= rr_type__linelengthindex__first .
H38:   begidx + 1 <= rr_type__linelengthindex__last .
H39:   begidx + 1 >= rr_type__linelengthindex__first .
H40:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           integer__base__first .
C2:    fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           integer__base__last .
C3:    begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
C4:    begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
C5:    begidx + 1 - (begidx + 1) >= integer__base__first .
C6:    begidx + 1 - (begidx + 1) <= integer__base__last .
 

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

procedure_addtokey_18.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   not ((endidx + 1 < length) and ((element(s, [endidx + 1]) <> 
           blank) and (element(s, [endidx + 1]) <> tab))) .
H30:   begidx >= rr_type__linelengthindex__first .
H31:   begidx <= rr_type__linelengthindex__last .
H32:   endidx + 1 >= rr_type__linelengthindex__first .
H33:   endidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           integer__base__first .
C2:    fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           integer__base__last .
C3:    endidx + 1 - begidx + 1 >= integer__base__first .
C4:    endidx + 1 - begidx + 1 <= integer__base__last .
C5:    endidx + 1 - begidx >= integer__base__first .
C6:    endidx + 1 - begidx <= integer__base__last .
 

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

procedure_addtokey_19.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   not ((1 < length) and ((element(s, [1]) <> blank) and (element(
           s, [1]) <> tab))) .
H33:   1 >= rr_type__linelengthindex__first .
H34:   1 <= rr_type__linelengthindex__last .
H35:   1 >= rr_type__linelengthindex__first .
H36:   1 <= rr_type__linelengthindex__last .
H37:   fld_keylength(dnskey_rec) + (1 - 1 + 1) >= integer__base__first .
H38:   fld_keylength(dnskey_rec) + (1 - 1 + 1) <= integer__base__last .
H39:   1 - 1 + 1 >= integer__base__first .
H40:   1 - 1 + 1 <= integer__base__last .
H41:   1 - 1 >= integer__base__first .
H42:   1 - 1 <= integer__base__last .
H43:   not (fld_keylength(dnskey_rec) + (1 - 1 + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H44:   1 >= rr_type__linelengthindex__first .
H45:   1 <= rr_type__linelengthindex__last .
H46:   1 >= rr_type__linelengthindex__first .
H47:   1 <= rr_type__linelengthindex__last .
        ->
C1:    1 >= integer__first .
C2:    1 <= integer__last .
C3:    1 >= integer__first .
C4:    1 <= integer__last .
 

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

procedure_addtokey_20.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) <> 
           blank) and (element(s, [begidx + 1]) <> tab))) .
H37:   begidx + 1 >= rr_type__linelengthindex__first .
H38:   begidx + 1 <= rr_type__linelengthindex__last .
H39:   begidx + 1 >= rr_type__linelengthindex__first .
H40:   begidx + 1 <= rr_type__linelengthindex__last .
H41:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           integer__base__first .
H42:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           integer__base__last .
H43:   begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
H44:   begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
H45:   begidx + 1 - (begidx + 1) >= integer__base__first .
H46:   begidx + 1 - (begidx + 1) <= integer__base__last .
H47:   not (fld_keylength(dnskey_rec) + (begidx + 1 - (
           begidx + 1) + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H48:   begidx + 1 >= rr_type__linelengthindex__first .
H49:   begidx + 1 <= rr_type__linelengthindex__last .
H50:   begidx + 1 >= rr_type__linelengthindex__first .
H51:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    begidx + 1 >= integer__first .
C2:    begidx + 1 <= integer__last .
C3:    begidx + 1 >= integer__first .
C4:    begidx + 1 <= integer__last .
 

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

procedure_addtokey_21.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   not ((endidx + 1 < length) and ((element(s, [endidx + 1]) <> 
           blank) and (element(s, [endidx + 1]) <> tab))) .
H30:   begidx >= rr_type__linelengthindex__first .
H31:   begidx <= rr_type__linelengthindex__last .
H32:   endidx + 1 >= rr_type__linelengthindex__first .
H33:   endidx + 1 <= rr_type__linelengthindex__last .
H34:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           integer__base__first .
H35:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           integer__base__last .
H36:   endidx + 1 - begidx + 1 >= integer__base__first .
H37:   endidx + 1 - begidx + 1 <= integer__base__last .
H38:   endidx + 1 - begidx >= integer__base__first .
H39:   endidx + 1 - begidx <= integer__base__last .
H40:   not (fld_keylength(dnskey_rec) + (endidx + 1 - 
           begidx + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   endidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx + 1 >= integer__first .
C2:    endidx + 1 <= integer__last .
C3:    begidx >= integer__first .
C4:    begidx <= integer__last .
 

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

procedure_addtokey_22.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   not ((1 < length) and ((element(s, [1]) <> blank) and (element(
           s, [1]) <> tab))) .
H33:   1 >= rr_type__linelengthindex__first .
H34:   1 <= rr_type__linelengthindex__last .
H35:   1 >= rr_type__linelengthindex__first .
H36:   1 <= rr_type__linelengthindex__last .
H37:   fld_keylength(dnskey_rec) + (1 - 1 + 1) >= integer__base__first .
H38:   fld_keylength(dnskey_rec) + (1 - 1 + 1) <= integer__base__last .
H39:   1 - 1 + 1 >= integer__base__first .
H40:   1 - 1 + 1 <= integer__base__last .
H41:   1 - 1 >= integer__base__first .
H42:   1 - 1 <= integer__base__last .
H43:   not (fld_keylength(dnskey_rec) + (1 - 1 + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H44:   1 >= rr_type__linelengthindex__first .
H45:   1 <= rr_type__linelengthindex__last .
H46:   1 >= rr_type__linelengthindex__first .
H47:   1 <= rr_type__linelengthindex__last .
H48:   1 >= integer__first .
H49:   1 <= integer__last .
H50:   1 >= integer__first .
H51:   1 <= integer__last .
        ->
C1:    (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
C2:    (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
 

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

procedure_addtokey_23.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) <> 
           blank) and (element(s, [begidx + 1]) <> tab))) .
H37:   begidx + 1 >= rr_type__linelengthindex__first .
H38:   begidx + 1 <= rr_type__linelengthindex__last .
H39:   begidx + 1 >= rr_type__linelengthindex__first .
H40:   begidx + 1 <= rr_type__linelengthindex__last .
H41:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           integer__base__first .
H42:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           integer__base__last .
H43:   begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
H44:   begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
H45:   begidx + 1 - (begidx + 1) >= integer__base__first .
H46:   begidx + 1 - (begidx + 1) <= integer__base__last .
H47:   not (fld_keylength(dnskey_rec) + (begidx + 1 - (
           begidx + 1) + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H48:   begidx + 1 >= rr_type__linelengthindex__first .
H49:   begidx + 1 <= rr_type__linelengthindex__last .
H50:   begidx + 1 >= rr_type__linelengthindex__first .
H51:   begidx + 1 <= rr_type__linelengthindex__last .
H52:   begidx + 1 >= integer__first .
H53:   begidx + 1 <= integer__last .
H54:   begidx + 1 >= integer__first .
H55:   begidx + 1 <= integer__last .
        ->
C1:    (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
C2:    (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
 

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

procedure_addtokey_24.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   not ((endidx + 1 < length) and ((element(s, [endidx + 1]) <> 
           blank) and (element(s, [endidx + 1]) <> tab))) .
H30:   begidx >= rr_type__linelengthindex__first .
H31:   begidx <= rr_type__linelengthindex__last .
H32:   endidx + 1 >= rr_type__linelengthindex__first .
H33:   endidx + 1 <= rr_type__linelengthindex__last .
H34:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           integer__base__first .
H35:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           integer__base__last .
H36:   endidx + 1 - begidx + 1 >= integer__base__first .
H37:   endidx + 1 - begidx + 1 <= integer__base__last .
H38:   endidx + 1 - begidx >= integer__base__first .
H39:   endidx + 1 - begidx <= integer__base__last .
H40:   not (fld_keylength(dnskey_rec) + (endidx + 1 - 
           begidx + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   endidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx + 1 <= rr_type__linelengthindex__last .
H45:   endidx + 1 >= integer__first .
H46:   endidx + 1 <= integer__last .
H47:   begidx >= integer__first .
H48:   begidx <= integer__last .
        ->
C1:    (begidx <= endidx + 1) -> ((endidx + 1 >= integer__first) and (
           endidx + 1 <= integer__last)) .
C2:    (begidx <= endidx + 1) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
 

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

procedure_addtokey_25.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   not ((1 < length) and ((element(s, [1]) <> blank) and (element(
           s, [1]) <> tab))) .
H33:   1 >= rr_type__linelengthindex__first .
H34:   1 <= rr_type__linelengthindex__last .
H35:   1 >= rr_type__linelengthindex__first .
H36:   1 <= rr_type__linelengthindex__last .
H37:   fld_keylength(dnskey_rec) + (1 - 1 + 1) >= integer__base__first .
H38:   fld_keylength(dnskey_rec) + (1 - 1 + 1) <= integer__base__last .
H39:   1 - 1 + 1 >= integer__base__first .
H40:   1 - 1 + 1 <= integer__base__last .
H41:   1 - 1 >= integer__base__first .
H42:   1 - 1 <= integer__base__last .
H43:   not (fld_keylength(dnskey_rec) + (1 - 1 + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H44:   1 >= rr_type__linelengthindex__first .
H45:   1 <= rr_type__linelengthindex__last .
H46:   1 >= rr_type__linelengthindex__first .
H47:   1 <= rr_type__linelengthindex__last .
H48:   1 >= integer__first .
H49:   1 <= integer__last .
H50:   1 >= integer__first .
H51:   1 <= integer__last .
H52:   (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
H53:   (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
H54:   1 >= rr_type__linelengthindex__first .
H55:   1 <= rr_type__linelengthindex__last .
H56:   1 >= rr_type__linelengthindex__first .
H57:   1 <= rr_type__linelengthindex__last .
H58:   1 <= 1 .
        ->
C1:    1 = 1 .
C2:    1 = 1 .
C3:    1 >= 1 .
C4:    1 <= 1 .
C5:    1 >= 1 .
C6:    fld_keylength(dnskey_rec) + (1 - 1 + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
C7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C20:   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))) .
C21:   length >= rr_type__linelengthindex__first .
C22:   length <= rr_type__linelengthindex__last .
C23:   1 >= integer__first .
C24:   1 <= integer__last .
C25:   1 >= 1 .
C26:   1 <= 1 .
C27:   1 >= rr_type__linelengthindex__first .
C28:   1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 791 to assertion of line 808:

procedure_addtokey_26.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) <> 
           blank) and (element(s, [begidx + 1]) <> tab))) .
H37:   begidx + 1 >= rr_type__linelengthindex__first .
H38:   begidx + 1 <= rr_type__linelengthindex__last .
H39:   begidx + 1 >= rr_type__linelengthindex__first .
H40:   begidx + 1 <= rr_type__linelengthindex__last .
H41:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           integer__base__first .
H42:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           integer__base__last .
H43:   begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
H44:   begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
H45:   begidx + 1 - (begidx + 1) >= integer__base__first .
H46:   begidx + 1 - (begidx + 1) <= integer__base__last .
H47:   not (fld_keylength(dnskey_rec) + (begidx + 1 - (
           begidx + 1) + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H48:   begidx + 1 >= rr_type__linelengthindex__first .
H49:   begidx + 1 <= rr_type__linelengthindex__last .
H50:   begidx + 1 >= rr_type__linelengthindex__first .
H51:   begidx + 1 <= rr_type__linelengthindex__last .
H52:   begidx + 1 >= integer__first .
H53:   begidx + 1 <= integer__last .
H54:   begidx + 1 >= integer__first .
H55:   begidx + 1 <= integer__last .
H56:   (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
H57:   (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
H58:   begidx + 1 >= rr_type__linelengthindex__first .
H59:   begidx + 1 <= rr_type__linelengthindex__last .
H60:   begidx + 1 >= rr_type__linelengthindex__first .
H61:   begidx + 1 <= rr_type__linelengthindex__last .
H62:   begidx + 1 <= begidx + 1 .
        ->
C1:    begidx + 1 = begidx + 1 .
C2:    begidx + 1 = begidx + 1 .
C3:    begidx + 1 >= begidx + 1 .
C4:    begidx + 1 <= begidx + 1 .
C5:    begidx + 1 >= 1 .
C6:    fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
C7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C20:   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))) .
C21:   length >= rr_type__linelengthindex__first .
C22:   length <= rr_type__linelengthindex__last .
C23:   begidx + 1 >= integer__first .
C24:   begidx + 1 <= integer__last .
C25:   begidx + 1 >= begidx + 1 .
C26:   begidx + 1 <= begidx + 1 .
C27:   begidx + 1 >= rr_type__linelengthindex__first .
C28:   begidx + 1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 798 to assertion of line 808:

procedure_addtokey_27.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   not ((endidx + 1 < length) and ((element(s, [endidx + 1]) <> 
           blank) and (element(s, [endidx + 1]) <> tab))) .
H30:   begidx >= rr_type__linelengthindex__first .
H31:   begidx <= rr_type__linelengthindex__last .
H32:   endidx + 1 >= rr_type__linelengthindex__first .
H33:   endidx + 1 <= rr_type__linelengthindex__last .
H34:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           integer__base__first .
H35:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           integer__base__last .
H36:   endidx + 1 - begidx + 1 >= integer__base__first .
H37:   endidx + 1 - begidx + 1 <= integer__base__last .
H38:   endidx + 1 - begidx >= integer__base__first .
H39:   endidx + 1 - begidx <= integer__base__last .
H40:   not (fld_keylength(dnskey_rec) + (endidx + 1 - 
           begidx + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   endidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx + 1 <= rr_type__linelengthindex__last .
H45:   endidx + 1 >= integer__first .
H46:   endidx + 1 <= integer__last .
H47:   begidx >= integer__first .
H48:   begidx <= integer__last .
H49:   (begidx <= endidx + 1) -> ((endidx + 1 >= integer__first) and (
           endidx + 1 <= integer__last)) .
H50:   (begidx <= endidx + 1) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H51:   begidx >= rr_type__linelengthindex__first .
H52:   begidx <= rr_type__linelengthindex__last .
H53:   endidx + 1 >= rr_type__linelengthindex__first .
H54:   endidx + 1 <= rr_type__linelengthindex__last .
H55:   begidx <= endidx + 1 .
        ->
C1:    begidx = begidx .
C2:    endidx + 1 = endidx + 1 .
C3:    begidx >= begidx .
C4:    begidx <= endidx + 1 .
C5:    begidx >= 1 .
C6:    fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
C7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
C11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
C12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
C13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
C14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
C15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
C16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
C18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C20:   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))) .
C21:   length >= rr_type__linelengthindex__first .
C22:   length <= rr_type__linelengthindex__last .
C23:   begidx >= integer__first .
C24:   begidx <= integer__last .
C25:   begidx >= begidx .
C26:   begidx <= endidx + 1 .
C27:   endidx + 1 >= rr_type__linelengthindex__first .
C28:   endidx + 1 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_28.
H1:    begidx = begidx .
H2:    endidx = endidx__entry__loop__3 .
H3:    loop__3__i >= begidx .
H4:    loop__3__i <= endidx .
H5:    begidx >= 1 .
H6:    fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
H7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H20:   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))) .
H21:   length >= rr_type__linelengthindex__first .
H22:   length <= rr_type__linelengthindex__last .
H23:   loop__3__i >= integer__first .
H24:   loop__3__i <= integer__last .
H25:   loop__3__i >= begidx .
H26:   loop__3__i <= endidx__entry__loop__3 .
H27:   endidx__entry__loop__3 >= rr_type__linelengthindex__first .
H28:   endidx__entry__loop__3 <= rr_type__linelengthindex__last .
H29:   element(s, [loop__3__i]) >= character__first .
H30:   element(s, [loop__3__i]) <= character__last .
H31:   loop__3__i >= rr_type__linelengthindex__first .
H32:   loop__3__i <= rr_type__linelengthindex__last .
H33:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first .
H34:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last .
H35:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           integer__base__first .
H36:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           integer__base__last .
H37:   loop__3__i - begidx + 1 >= integer__base__first .
H38:   loop__3__i - begidx + 1 <= integer__base__last .
H39:   loop__3__i - begidx >= integer__base__first .
H40:   loop__3__i - begidx <= integer__base__last .
H41:   not (loop__3__i = endidx__entry__loop__3) .
        ->
C1:    begidx = begidx .
C2:    endidx = endidx__entry__loop__3 .
C3:    loop__3__i + 1 >= begidx .
C4:    loop__3__i + 1 <= endidx .
C5:    begidx >= 1 .
C6:    fld_keylength(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) + (
           endidx - begidx + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
C7:    fld_ttlinseconds(fld_inherit(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i]))))) >= 
           unsigned_types__unsigned32__first .
C8:    fld_ttlinseconds(fld_inherit(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i]))))) <= 
           unsigned_types__unsigned32__last .
C9:    fld_class(fld_inherit(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i]))))) >= 
           rr_type__classtype__first .
C10:   fld_class(fld_inherit(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i]))))) <= 
           rr_type__classtype__last .
C11:   fld_flags(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) >= 
           unsigned_types__unsigned16__first .
C12:   fld_flags(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) <= 
           unsigned_types__unsigned16__last .
C13:   fld_protocol(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) >= 
           unsigned_types__unsigned8__first .
C14:   fld_protocol(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) <= 
           unsigned_types__unsigned8__last .
C15:   fld_algorithm(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) >= 
           unsigned_types__unsigned8__first .
C16:   fld_algorithm(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) <= 
           unsigned_types__unsigned8__last .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))), [
           i___1]) >= character__first) and (element(fld_key(upf_key(
           dnskey_rec, update(fld_key(dnskey_rec), [fld_keylength(
           dnskey_rec) + (loop__3__i - begidx + 1)], element(
           s, [loop__3__i])))), [i___1]) <= character__last))) .
C18:   fld_keylength(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C19:   fld_keylength(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C20:   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))) .
C21:   length >= rr_type__linelengthindex__first .
C22:   length <= rr_type__linelengthindex__last .
C23:   loop__3__i + 1 >= integer__first .
C24:   loop__3__i + 1 <= integer__last .
C25:   loop__3__i + 1 >= begidx .
C26:   loop__3__i + 1 <= endidx__entry__loop__3 .
C27:   endidx__entry__loop__3 >= rr_type__linelengthindex__first .
C28:   endidx__entry__loop__3 <= rr_type__linelengthindex__last .
 

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

procedure_addtokey_29.
H1:    begidx = begidx .
H2:    endidx = endidx__entry__loop__3 .
H3:    loop__3__i >= begidx .
H4:    loop__3__i <= endidx .
H5:    begidx >= 1 .
H6:    fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
H7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H20:   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))) .
H21:   length >= rr_type__linelengthindex__first .
H22:   length <= rr_type__linelengthindex__last .
H23:   loop__3__i >= integer__first .
H24:   loop__3__i <= integer__last .
H25:   loop__3__i >= begidx .
H26:   loop__3__i <= endidx__entry__loop__3 .
H27:   endidx__entry__loop__3 >= rr_type__linelengthindex__first .
H28:   endidx__entry__loop__3 <= rr_type__linelengthindex__last .
        ->
C1:    element(s, [loop__3__i]) >= character__first .
C2:    element(s, [loop__3__i]) <= character__last .
C3:    loop__3__i >= rr_type__linelengthindex__first .
C4:    loop__3__i <= rr_type__linelengthindex__last .
C5:    fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first .
C6:    fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last .
C7:    fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           integer__base__first .
C8:    fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           integer__base__last .
C9:    loop__3__i - begidx + 1 >= integer__base__first .
C10:   loop__3__i - begidx + 1 <= integer__base__last .
C11:   loop__3__i - begidx >= integer__base__first .
C12:   loop__3__i - begidx <= integer__base__last .
 

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

procedure_addtokey_30.
H1:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H2:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H3:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H4:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H5:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H6:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H7:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H8:    fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H9:    fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H12:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H13:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H14:   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))) .
H15:   length >= rr_type__linelengthindex__first .
H16:   length <= rr_type__linelengthindex__last .
H17:   1 >= rr_type__linelengthindex__first .
H18:   1 <= rr_type__linelengthindex__last .
H19:   1 >= rr_type__linelengthindex__first .
H20:   1 <= rr_type__linelengthindex__last .
H21:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H22:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H23:   not ((1 < length) and ((element(s, [1]) = blank) or (element(
           s, [1]) = tab))) .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   1 >= rr_type__linelengthindex__first .
H27:   1 <= rr_type__linelengthindex__last .
H28:   1 >= rr_type__linelengthindex__first .
H29:   1 <= rr_type__linelengthindex__last .
H30:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H31:   (1 < length) -> ((1 >= rr_type__linelengthindex__first) and (1 <= 
           rr_type__linelengthindex__last)) .
H32:   not ((1 < length) and ((element(s, [1]) <> blank) and (element(
           s, [1]) <> tab))) .
H33:   1 >= rr_type__linelengthindex__first .
H34:   1 <= rr_type__linelengthindex__last .
H35:   1 >= rr_type__linelengthindex__first .
H36:   1 <= rr_type__linelengthindex__last .
H37:   fld_keylength(dnskey_rec) + (1 - 1 + 1) >= integer__base__first .
H38:   fld_keylength(dnskey_rec) + (1 - 1 + 1) <= integer__base__last .
H39:   1 - 1 + 1 >= integer__base__first .
H40:   1 - 1 + 1 <= integer__base__last .
H41:   1 - 1 >= integer__base__first .
H42:   1 - 1 <= integer__base__last .
H43:   not (fld_keylength(dnskey_rec) + (1 - 1 + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H44:   1 >= rr_type__linelengthindex__first .
H45:   1 <= rr_type__linelengthindex__last .
H46:   1 >= rr_type__linelengthindex__first .
H47:   1 <= rr_type__linelengthindex__last .
H48:   1 >= integer__first .
H49:   1 <= integer__last .
H50:   1 >= integer__first .
H51:   1 <= integer__last .
H52:   (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
H53:   (1 <= 1) -> ((1 >= integer__first) and (1 <= integer__last)) .
H54:   1 >= rr_type__linelengthindex__first .
H55:   1 <= rr_type__linelengthindex__last .
H56:   1 >= rr_type__linelengthindex__first .
H57:   1 <= rr_type__linelengthindex__last .
H58:   not (1 <= 1) .
H59:   1 >= rr_type__linelengthindex__first .
H60:   1 <= rr_type__linelengthindex__last .
H61:   1 >= rr_type__linelengthindex__first .
H62:   1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (1 - 1 + 1) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C2:    fld_keylength(dnskey_rec) + (1 - 1 + 1) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C3:    1 - 1 + 1 >= integer__base__first .
C4:    1 - 1 + 1 <= integer__base__last .
C5:    1 - 1 >= integer__base__first .
C6:    1 - 1 <= integer__base__last .
 

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

procedure_addtokey_31.
H1:    begidx >= 1 .
H2:    begidx < length .
H3:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H4:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H5:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H6:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H7:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H8:    fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H9:    fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H10:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H11:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H14:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H15:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H16:   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))) .
H17:   length >= rr_type__linelengthindex__first .
H18:   length <= rr_type__linelengthindex__last .
H19:   begidx >= rr_type__linelengthindex__first .
H20:   begidx <= rr_type__linelengthindex__last .
H21:   begidx + 1 >= rr_type__linelengthindex__first .
H22:   begidx + 1 <= rr_type__linelengthindex__last .
H23:   begidx + 1 >= rr_type__linelengthindex__first .
H24:   begidx + 1 <= rr_type__linelengthindex__last .
H25:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H26:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H27:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) = 
           blank) or (element(s, [begidx + 1]) = tab))) .
H28:   begidx + 1 >= rr_type__linelengthindex__first .
H29:   begidx + 1 <= rr_type__linelengthindex__last .
H30:   begidx + 1 >= rr_type__linelengthindex__first .
H31:   begidx + 1 <= rr_type__linelengthindex__last .
H32:   begidx + 1 >= rr_type__linelengthindex__first .
H33:   begidx + 1 <= rr_type__linelengthindex__last .
H34:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H35:   (begidx + 1 < length) -> ((begidx + 1 >= 
           rr_type__linelengthindex__first) and (begidx + 1 <= 
           rr_type__linelengthindex__last)) .
H36:   not ((begidx + 1 < length) and ((element(s, [begidx + 1]) <> 
           blank) and (element(s, [begidx + 1]) <> tab))) .
H37:   begidx + 1 >= rr_type__linelengthindex__first .
H38:   begidx + 1 <= rr_type__linelengthindex__last .
H39:   begidx + 1 >= rr_type__linelengthindex__first .
H40:   begidx + 1 <= rr_type__linelengthindex__last .
H41:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           integer__base__first .
H42:   fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           integer__base__last .
H43:   begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
H44:   begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
H45:   begidx + 1 - (begidx + 1) >= integer__base__first .
H46:   begidx + 1 - (begidx + 1) <= integer__base__last .
H47:   not (fld_keylength(dnskey_rec) + (begidx + 1 - (
           begidx + 1) + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H48:   begidx + 1 >= rr_type__linelengthindex__first .
H49:   begidx + 1 <= rr_type__linelengthindex__last .
H50:   begidx + 1 >= rr_type__linelengthindex__first .
H51:   begidx + 1 <= rr_type__linelengthindex__last .
H52:   begidx + 1 >= integer__first .
H53:   begidx + 1 <= integer__last .
H54:   begidx + 1 >= integer__first .
H55:   begidx + 1 <= integer__last .
H56:   (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
H57:   (begidx + 1 <= begidx + 1) -> ((begidx + 1 >= 
           integer__first) and (begidx + 1 <= integer__last)) .
H58:   begidx + 1 >= rr_type__linelengthindex__first .
H59:   begidx + 1 <= rr_type__linelengthindex__last .
H60:   begidx + 1 >= rr_type__linelengthindex__first .
H61:   begidx + 1 <= rr_type__linelengthindex__last .
H62:   not (begidx + 1 <= begidx + 1) .
H63:   begidx + 1 >= rr_type__linelengthindex__first .
H64:   begidx + 1 <= rr_type__linelengthindex__last .
H65:   begidx + 1 >= rr_type__linelengthindex__first .
H66:   begidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C2:    fld_keylength(dnskey_rec) + (begidx + 1 - (begidx + 1) + 1) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C3:    begidx + 1 - (begidx + 1) + 1 >= integer__base__first .
C4:    begidx + 1 - (begidx + 1) + 1 <= integer__base__last .
C5:    begidx + 1 - (begidx + 1) >= integer__base__first .
C6:    begidx + 1 - (begidx + 1) <= integer__base__last .
 

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

procedure_addtokey_32.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    endidx >= 1 .
H4:    endidx < length .
H5:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H6:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H7:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H8:    fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H9:    fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H10:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H11:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H12:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H13:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H16:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H17:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H18:   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))) .
H19:   length >= rr_type__linelengthindex__first .
H20:   length <= rr_type__linelengthindex__last .
H21:   endidx >= rr_type__linelengthindex__first .
H22:   endidx <= rr_type__linelengthindex__last .
H23:   endidx + 1 >= rr_type__linelengthindex__first .
H24:   endidx + 1 <= rr_type__linelengthindex__last .
H25:   endidx + 1 >= rr_type__linelengthindex__first .
H26:   endidx + 1 <= rr_type__linelengthindex__last .
H27:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H28:   (endidx + 1 < length) -> ((endidx + 1 >= 
           rr_type__linelengthindex__first) and (endidx + 1 <= 
           rr_type__linelengthindex__last)) .
H29:   not ((endidx + 1 < length) and ((element(s, [endidx + 1]) <> 
           blank) and (element(s, [endidx + 1]) <> tab))) .
H30:   begidx >= rr_type__linelengthindex__first .
H31:   begidx <= rr_type__linelengthindex__last .
H32:   endidx + 1 >= rr_type__linelengthindex__first .
H33:   endidx + 1 <= rr_type__linelengthindex__last .
H34:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           integer__base__first .
H35:   fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           integer__base__last .
H36:   endidx + 1 - begidx + 1 >= integer__base__first .
H37:   endidx + 1 - begidx + 1 <= integer__base__last .
H38:   endidx + 1 - begidx >= integer__base__first .
H39:   endidx + 1 - begidx <= integer__base__last .
H40:   not (fld_keylength(dnskey_rec) + (endidx + 1 - 
           begidx + 1) > 
           rr_type__dnskey_record_type__maxdnskeylength) .
H41:   begidx >= rr_type__linelengthindex__first .
H42:   begidx <= rr_type__linelengthindex__last .
H43:   endidx + 1 >= rr_type__linelengthindex__first .
H44:   endidx + 1 <= rr_type__linelengthindex__last .
H45:   endidx + 1 >= integer__first .
H46:   endidx + 1 <= integer__last .
H47:   begidx >= integer__first .
H48:   begidx <= integer__last .
H49:   (begidx <= endidx + 1) -> ((endidx + 1 >= integer__first) and (
           endidx + 1 <= integer__last)) .
H50:   (begidx <= endidx + 1) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H51:   begidx >= rr_type__linelengthindex__first .
H52:   begidx <= rr_type__linelengthindex__last .
H53:   endidx + 1 >= rr_type__linelengthindex__first .
H54:   endidx + 1 <= rr_type__linelengthindex__last .
H55:   not (begidx <= endidx + 1) .
H56:   begidx >= rr_type__linelengthindex__first .
H57:   begidx <= rr_type__linelengthindex__last .
H58:   endidx + 1 >= rr_type__linelengthindex__first .
H59:   endidx + 1 <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C2:    fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C3:    endidx + 1 - begidx + 1 >= integer__base__first .
C4:    endidx + 1 - begidx + 1 <= integer__base__last .
C5:    endidx + 1 - begidx >= integer__base__first .
C6:    endidx + 1 - begidx <= integer__base__last .
 

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

procedure_addtokey_33.
H1:    begidx = begidx .
H2:    endidx = endidx__entry__loop__3 .
H3:    loop__3__i >= begidx .
H4:    loop__3__i <= endidx .
H5:    begidx >= 1 .
H6:    fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
           rr_type__dnskey_record_type__maxdnskeylength .
H7:    fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
           unsigned_types__unsigned32__first .
H8:    fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
           unsigned_types__unsigned32__last .
H9:    fld_class(fld_inherit(dnskey_rec)) >= 
           rr_type__classtype__first .
H10:   fld_class(fld_inherit(dnskey_rec)) <= 
           rr_type__classtype__last .
H11:   fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first .
H12:   fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last .
H13:   fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first .
H14:   fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last .
H15:   fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first .
H16:   fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first) and (
           i___1 <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last)) -> ((element(
           fld_key(dnskey_rec), [i___1]) >= character__first) and (element(
           fld_key(dnskey_rec), [i___1]) <= character__last))) .
H18:   fld_keylength(dnskey_rec) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
H19:   fld_keylength(dnskey_rec) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
H20:   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))) .
H21:   length >= rr_type__linelengthindex__first .
H22:   length <= rr_type__linelengthindex__last .
H23:   loop__3__i >= integer__first .
H24:   loop__3__i <= integer__last .
H25:   loop__3__i >= begidx .
H26:   loop__3__i <= endidx__entry__loop__3 .
H27:   endidx__entry__loop__3 >= rr_type__linelengthindex__first .
H28:   endidx__entry__loop__3 <= rr_type__linelengthindex__last .
H29:   element(s, [loop__3__i]) >= character__first .
H30:   element(s, [loop__3__i]) <= character__last .
H31:   loop__3__i >= rr_type__linelengthindex__first .
H32:   loop__3__i <= rr_type__linelengthindex__last .
H33:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__first .
H34:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           rr_type__dnskey_record_type__dnskeystringtypeindex__last .
H35:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 
           integer__base__first .
H36:   fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
           integer__base__last .
H37:   loop__3__i - begidx + 1 >= integer__base__first .
H38:   loop__3__i - begidx + 1 <= integer__base__last .
H39:   loop__3__i - begidx >= integer__base__first .
H40:   loop__3__i - begidx <= integer__base__last .
H41:   loop__3__i = endidx__entry__loop__3 .
H42:   begidx >= rr_type__linelengthindex__first .
H43:   begidx <= rr_type__linelengthindex__last .
H44:   endidx >= rr_type__linelengthindex__first .
H45:   endidx <= rr_type__linelengthindex__last .
        ->
C1:    fld_keylength(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) + (
           endidx - begidx + 1) >= 
           rr_type__dnskey_record_type__keylengthvaluetype__first .
C2:    fld_keylength(upf_key(dnskey_rec, update(fld_key(
           dnskey_rec), [fld_keylength(dnskey_rec) + (
           loop__3__i - begidx + 1)], element(s, [loop__3__i])))) + (
           endidx - begidx + 1) <= 
           rr_type__dnskey_record_type__keylengthvaluetype__last .
C3:    endidx - begidx + 1 >= integer__base__first .
C4:    endidx - begidx + 1 <= integer__base__last .
C5:    endidx - begidx >= integer__base__first .
C6:    endidx - begidx <= integer__base__last .
 

For path(s) from start to finish:

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


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


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

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


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


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

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


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


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

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


