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

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



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

procedure Process_Dns_Request.Set_TTL_Data_DNSKEY




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

procedure_set_ttl_data_dnskey_1.
H1:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H3:    start_byte >= 1 .
H4:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H5:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H6:    rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H7:    fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H8:    fld_flags(dnskey_record) >= 0 .
H9:    fld_flags(dnskey_record) <= 65535 .
H10:   fld_protocol(dnskey_record) >= 0 .
H11:   fld_protocol(dnskey_record) <= 255 .
H12:   fld_algorithm(dnskey_record) >= 0 .
H13:   fld_algorithm(dnskey_record) <= 255 .
H14:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H15:   fld_keylength(dnskey_record) >= 0 .
H16:   fld_keylength(dnskey_record) <= 1365 .
H17:   integer__size >= 0 .
H18:   character__size >= 0 .
H19:   positive__size >= 0 .
H20:   dns_types__packet_bytes_range__size >= 0 .
H21:   unsigned_types__unsigned8__size >= 0 .
H22:   unsigned_types__unsigned16__size >= 0 .
H23:   unsigned_types__unsigned32__size >= 0 .
H24:   rr_type__classtype__size >= 0 .
H25:   rr_type__resourcerecordtype__size >= 0 .
H26:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H27:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H28:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H29:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8177 .


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

procedure_set_ttl_data_dnskey_2.
H1:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H3:    start_byte >= 1 .
H4:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H5:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H6:    rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H7:    fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H8:    fld_flags(dnskey_record) >= 0 .
H9:    fld_flags(dnskey_record) <= 65535 .
H10:   fld_protocol(dnskey_record) >= 0 .
H11:   fld_protocol(dnskey_record) <= 255 .
H12:   fld_algorithm(dnskey_record) >= 0 .
H13:   fld_algorithm(dnskey_record) <= 255 .
H14:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H15:   fld_keylength(dnskey_record) >= 0 .
H16:   fld_keylength(dnskey_record) <= 1365 .
H17:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255) .
H18:   integer__size >= 0 .
H19:   character__size >= 0 .
H20:   positive__size >= 0 .
H21:   dns_types__packet_bytes_range__size >= 0 .
H22:   unsigned_types__unsigned8__size >= 0 .
H23:   unsigned_types__unsigned16__size >= 0 .
H24:   unsigned_types__unsigned32__size >= 0 .
H25:   rr_type__classtype__size >= 0 .
H26:   rr_type__resourcerecordtype__size >= 0 .
H27:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H28:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H29:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H30:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8176 .
C2:    start_byte <= 8175 .


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

procedure_set_ttl_data_dnskey_3.
H1:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H3:    start_byte >= 1 .
H4:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H5:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H6:    rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H7:    fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H8:    fld_flags(dnskey_record) >= 0 .
H9:    fld_flags(dnskey_record) <= 65535 .
H10:   fld_protocol(dnskey_record) >= 0 .
H11:   fld_protocol(dnskey_record) <= 255 .
H12:   fld_algorithm(dnskey_record) >= 0 .
H13:   fld_algorithm(dnskey_record) <= 255 .
H14:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H15:   fld_keylength(dnskey_record) >= 0 .
H16:   fld_keylength(dnskey_record) <= 1365 .
H17:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255) .
H18:   fld_keylength(dnskey_record) >= - 4 .
H19:   fld_keylength(dnskey_record) <= 65531 .
H20:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255) .
H21:   integer__size >= 0 .
H22:   character__size >= 0 .
H23:   positive__size >= 0 .
H24:   dns_types__packet_bytes_range__size >= 0 .
H25:   unsigned_types__unsigned8__size >= 0 .
H26:   unsigned_types__unsigned16__size >= 0 .
H27:   unsigned_types__unsigned32__size >= 0 .
H28:   rr_type__classtype__size >= 0 .
H29:   rr_type__resourcerecordtype__size >= 0 .
H30:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H31:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H32:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H33:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8174 .
C2:    start_byte <= 8173 .


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

procedure_set_ttl_data_dnskey_4.
H1:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H3:    start_byte >= 1 .
H4:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H5:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H6:    rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H7:    fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H8:    fld_flags(dnskey_record) >= 0 .
H9:    fld_flags(dnskey_record) <= 65535 .
H10:   fld_protocol(dnskey_record) >= 0 .
H11:   fld_protocol(dnskey_record) <= 255 .
H12:   fld_algorithm(dnskey_record) >= 0 .
H13:   fld_algorithm(dnskey_record) <= 255 .
H14:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H15:   fld_keylength(dnskey_record) >= 0 .
H16:   fld_keylength(dnskey_record) <= 1365 .
H17:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255) .
H18:   fld_keylength(dnskey_record) >= - 4 .
H19:   fld_keylength(dnskey_record) <= 65531 .
H20:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255) .
H21:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__3, [i___1]) and element(bytes__3, [i___1]) <= 255) .
H22:   integer__size >= 0 .
H23:   character__size >= 0 .
H24:   positive__size >= 0 .
H25:   dns_types__packet_bytes_range__size >= 0 .
H26:   unsigned_types__unsigned8__size >= 0 .
H27:   unsigned_types__unsigned16__size >= 0 .
H28:   unsigned_types__unsigned32__size >= 0 .
H29:   rr_type__classtype__size >= 0 .
H30:   rr_type__resourcerecordtype__size >= 0 .
H31:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H32:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H33:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H34:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8172 .


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

procedure_set_ttl_data_dnskey_5.
H1:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H2:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H3:    start_byte >= 1 .
H4:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H5:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H6:    rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H7:    fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H8:    fld_flags(dnskey_record) >= 0 .
H9:    fld_flags(dnskey_record) <= 65535 .
H10:   fld_protocol(dnskey_record) >= 0 .
H11:   fld_protocol(dnskey_record) <= 255 .
H12:   fld_algorithm(dnskey_record) >= 0 .
H13:   fld_algorithm(dnskey_record) <= 255 .
H14:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H15:   fld_keylength(dnskey_record) >= 0 .
H16:   fld_keylength(dnskey_record) <= 1365 .
H17:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255) .
H18:   fld_keylength(dnskey_record) >= - 4 .
H19:   fld_keylength(dnskey_record) <= 65531 .
H20:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255) .
H21:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__3, [i___1]) and element(bytes__3, [i___1]) <= 255) .
H22:   integer__size >= 0 .
H23:   character__size >= 0 .
H24:   positive__size >= 0 .
H25:   dns_types__packet_bytes_range__size >= 0 .
H26:   unsigned_types__unsigned8__size >= 0 .
H27:   unsigned_types__unsigned16__size >= 0 .
H28:   unsigned_types__unsigned32__size >= 0 .
H29:   rr_type__classtype__size >= 0 .
H30:   rr_type__resourcerecordtype__size >= 0 .
H31:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H32:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H33:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H34:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8171 .


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

procedure_set_ttl_data_dnskey_6.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_7.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_8.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_9.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_10.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_11.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_12.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_13.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_14.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_15.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_16.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_17.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_18.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_19.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_20.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_21.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_22.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_23.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_24.
H1:    srcbyte + 3 <= fld_keylength(dnskey_record) .
H2:    fld_keylength(dnskey_record) <= 1365 .
H3:    dstbytes >= 1 .
H4:    dstbytes <= srcbyte .
H5:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H6:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H7:    start_byte >= 1 .
H8:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H9:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H10:   rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H11:   fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H12:   fld_flags(dnskey_record) >= 0 .
H13:   fld_flags(dnskey_record) <= 65535 .
H14:   fld_protocol(dnskey_record) >= 0 .
H15:   fld_protocol(dnskey_record) <= 255 .
H16:   fld_algorithm(dnskey_record) >= 0 .
H17:   fld_algorithm(dnskey_record) <= 255 .
H18:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H19:   fld_keylength(dnskey_record) >= 0 .
H20:   fld_keylength(dnskey_record) <= 1365 .
H21:   element(fld_key(dnskey_record), [srcbyte]) >= 0 .
H22:   element(fld_key(dnskey_record), [srcbyte]) <= 255 .
H23:   srcbyte >= 1 .
H24:   lookup(element(fld_key(dnskey_record), [srcbyte])) >= 0 .
H25:   lookup(element(fld_key(dnskey_record), [srcbyte])) <= 255 .
H26:   element(fld_key(dnskey_record), [srcbyte + 1]) >= 0 .
H27:   element(fld_key(dnskey_record), [srcbyte + 1]) <= 255 .
H28:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) >= 0 .
H29:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) <= 255 .
H30:   element(fld_key(dnskey_record), [srcbyte + 2]) >= 0 .
H31:   element(fld_key(dnskey_record), [srcbyte + 2]) <= 255 .
H32:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) >= 0 .
H33:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) <= 255 .
H34:   element(fld_key(dnskey_record), [srcbyte + 3]) >= 0 .
H35:   element(fld_key(dnskey_record), [srcbyte + 3]) <= 255 .
H36:   srcbyte <= 1362 .
H37:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) >= 0 .
H38:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) <= 255 .
H39:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 >= 0 .
H40:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 <= 
          255 .
H41:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          >= 0 .
H42:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          <= 255 .
H43:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 >= 0 .
H44:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 <= 
          255 .
H45:   integer__size >= 0 .
H46:   character__size >= 0 .
H47:   positive__size >= 0 .
H48:   dns_types__packet_bytes_range__size >= 0 .
H49:   unsigned_types__unsigned8__size >= 0 .
H50:   unsigned_types__unsigned16__size >= 0 .
H51:   unsigned_types__unsigned32__size >= 0 .
H52:   rr_type__classtype__size >= 0 .
H53:   rr_type__resourcerecordtype__size >= 0 .
H54:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H55:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H56:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H57:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte + 9 + dstbytes <= 8180 .


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

procedure_set_ttl_data_dnskey_25.
H1:    srcbyte + 3 <= fld_keylength(dnskey_record) .
H2:    fld_keylength(dnskey_record) <= 1365 .
H3:    dstbytes >= 1 .
H4:    dstbytes <= srcbyte .
H5:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H6:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H7:    start_byte >= 1 .
H8:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H9:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H10:   rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H11:   fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H12:   fld_flags(dnskey_record) >= 0 .
H13:   fld_flags(dnskey_record) <= 65535 .
H14:   fld_protocol(dnskey_record) >= 0 .
H15:   fld_protocol(dnskey_record) <= 255 .
H16:   fld_algorithm(dnskey_record) >= 0 .
H17:   fld_algorithm(dnskey_record) <= 255 .
H18:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H19:   fld_keylength(dnskey_record) >= 0 .
H20:   fld_keylength(dnskey_record) <= 1365 .
H21:   element(fld_key(dnskey_record), [srcbyte]) >= 0 .
H22:   element(fld_key(dnskey_record), [srcbyte]) <= 255 .
H23:   srcbyte >= 1 .
H24:   lookup(element(fld_key(dnskey_record), [srcbyte])) >= 0 .
H25:   lookup(element(fld_key(dnskey_record), [srcbyte])) <= 255 .
H26:   element(fld_key(dnskey_record), [srcbyte + 1]) >= 0 .
H27:   element(fld_key(dnskey_record), [srcbyte + 1]) <= 255 .
H28:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) >= 0 .
H29:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) <= 255 .
H30:   element(fld_key(dnskey_record), [srcbyte + 2]) >= 0 .
H31:   element(fld_key(dnskey_record), [srcbyte + 2]) <= 255 .
H32:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) >= 0 .
H33:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) <= 255 .
H34:   element(fld_key(dnskey_record), [srcbyte + 3]) >= 0 .
H35:   element(fld_key(dnskey_record), [srcbyte + 3]) <= 255 .
H36:   srcbyte <= 1362 .
H37:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) >= 0 .
H38:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) <= 255 .
H39:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 >= 0 .
H40:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 <= 
          255 .
H41:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          >= 0 .
H42:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          <= 255 .
H43:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 >= 0 .
H44:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 <= 
          255 .
H45:   start_byte + 9 + dstbytes >= 1 .
H46:   start_byte + 9 + dstbytes <= 8180 .
H47:   integer__size >= 0 .
H48:   character__size >= 0 .
H49:   positive__size >= 0 .
H50:   dns_types__packet_bytes_range__size >= 0 .
H51:   unsigned_types__unsigned8__size >= 0 .
H52:   unsigned_types__unsigned16__size >= 0 .
H53:   unsigned_types__unsigned32__size >= 0 .
H54:   rr_type__classtype__size >= 0 .
H55:   rr_type__resourcerecordtype__size >= 0 .
H56:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H57:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H58:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H59:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte + 9 + (dstbytes + 1) <= 8180 .


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

procedure_set_ttl_data_dnskey_26.
H1:    srcbyte + 3 <= fld_keylength(dnskey_record) .
H2:    fld_keylength(dnskey_record) <= 1365 .
H3:    dstbytes >= 1 .
H4:    dstbytes <= srcbyte .
H5:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H6:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H7:    start_byte >= 1 .
H8:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H9:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H10:   rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H11:   fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H12:   fld_flags(dnskey_record) >= 0 .
H13:   fld_flags(dnskey_record) <= 65535 .
H14:   fld_protocol(dnskey_record) >= 0 .
H15:   fld_protocol(dnskey_record) <= 255 .
H16:   fld_algorithm(dnskey_record) >= 0 .
H17:   fld_algorithm(dnskey_record) <= 255 .
H18:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H19:   fld_keylength(dnskey_record) >= 0 .
H20:   fld_keylength(dnskey_record) <= 1365 .
H21:   element(fld_key(dnskey_record), [srcbyte]) >= 0 .
H22:   element(fld_key(dnskey_record), [srcbyte]) <= 255 .
H23:   srcbyte >= 1 .
H24:   lookup(element(fld_key(dnskey_record), [srcbyte])) >= 0 .
H25:   lookup(element(fld_key(dnskey_record), [srcbyte])) <= 255 .
H26:   element(fld_key(dnskey_record), [srcbyte + 1]) >= 0 .
H27:   element(fld_key(dnskey_record), [srcbyte + 1]) <= 255 .
H28:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) >= 0 .
H29:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) <= 255 .
H30:   element(fld_key(dnskey_record), [srcbyte + 2]) >= 0 .
H31:   element(fld_key(dnskey_record), [srcbyte + 2]) <= 255 .
H32:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) >= 0 .
H33:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) <= 255 .
H34:   element(fld_key(dnskey_record), [srcbyte + 3]) >= 0 .
H35:   element(fld_key(dnskey_record), [srcbyte + 3]) <= 255 .
H36:   srcbyte <= 1362 .
H37:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) >= 0 .
H38:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) <= 255 .
H39:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 >= 0 .
H40:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 <= 
          255 .
H41:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          >= 0 .
H42:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          <= 255 .
H43:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 >= 0 .
H44:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 <= 
          255 .
H45:   start_byte + 9 + dstbytes >= 1 .
H46:   start_byte + 9 + (dstbytes + 1) <= 8180 .
H47:   integer__size >= 0 .
H48:   character__size >= 0 .
H49:   positive__size >= 0 .
H50:   dns_types__packet_bytes_range__size >= 0 .
H51:   unsigned_types__unsigned8__size >= 0 .
H52:   unsigned_types__unsigned16__size >= 0 .
H53:   unsigned_types__unsigned32__size >= 0 .
H54:   rr_type__classtype__size >= 0 .
H55:   rr_type__resourcerecordtype__size >= 0 .
H56:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H57:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H58:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H59:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte + 9 + (dstbytes + 2) <= 8180 .


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

procedure_set_ttl_data_dnskey_27.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_28.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_29.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_30.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_31.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_32.
H1:    srcbyte + 3 <= fld_keylength(dnskey_record) .
H2:    fld_keylength(dnskey_record) <= 1365 .
H3:    dstbytes >= 1 .
H4:    dstbytes <= srcbyte .
H5:    start_byte <= 8170 - fld_keylength(dnskey_record) .
H6:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H7:    start_byte >= 1 .
H8:    fld_ttlinseconds(fld_inherit(dnskey_record)) >= 0 .
H9:    fld_ttlinseconds(fld_inherit(dnskey_record)) <= 4294967295 .
H10:   rr_type__internet <= fld_class(fld_inherit(dnskey_record)) .
H11:   fld_class(fld_inherit(dnskey_record)) <= rr_type__hs .
H12:   fld_flags(dnskey_record) >= 0 .
H13:   fld_flags(dnskey_record) <= 65535 .
H14:   fld_protocol(dnskey_record) >= 0 .
H15:   fld_protocol(dnskey_record) <= 255 .
H16:   fld_algorithm(dnskey_record) >= 0 .
H17:   fld_algorithm(dnskey_record) <= 255 .
H18:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= element(
          fld_key(dnskey_record), [i___1]) and element(fld_key(dnskey_record), [
          i___1]) <= 255) .
H19:   fld_keylength(dnskey_record) >= 0 .
H20:   fld_keylength(dnskey_record) <= 1365 .
H21:   element(fld_key(dnskey_record), [srcbyte]) >= 0 .
H22:   element(fld_key(dnskey_record), [srcbyte]) <= 255 .
H23:   srcbyte >= 1 .
H24:   lookup(element(fld_key(dnskey_record), [srcbyte])) >= 0 .
H25:   lookup(element(fld_key(dnskey_record), [srcbyte])) <= 255 .
H26:   element(fld_key(dnskey_record), [srcbyte + 1]) >= 0 .
H27:   element(fld_key(dnskey_record), [srcbyte + 1]) <= 255 .
H28:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) >= 0 .
H29:   lookup(element(fld_key(dnskey_record), [srcbyte + 1])) <= 255 .
H30:   element(fld_key(dnskey_record), [srcbyte + 2]) >= 0 .
H31:   element(fld_key(dnskey_record), [srcbyte + 2]) <= 255 .
H32:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) >= 0 .
H33:   lookup(element(fld_key(dnskey_record), [srcbyte + 2])) <= 255 .
H34:   element(fld_key(dnskey_record), [srcbyte + 3]) >= 0 .
H35:   element(fld_key(dnskey_record), [srcbyte + 3]) <= 255 .
H36:   srcbyte <= 1362 .
H37:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) >= 0 .
H38:   lookup(element(fld_key(dnskey_record), [srcbyte + 3])) <= 255 .
H39:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 >= 0 .
H40:   (lookup(element(fld_key(dnskey_record), [srcbyte])) * 4 mod 256 + lookup(
          element(fld_key(dnskey_record), [srcbyte + 1])) div 16) mod 256 <= 
          255 .
H41:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          >= 0 .
H42:   (lookup(element(fld_key(dnskey_record), [srcbyte + 1])) * 16 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 2])) div 4) mod 256 
          <= 255 .
H43:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 >= 0 .
H44:   (lookup(element(fld_key(dnskey_record), [srcbyte + 2])) * 64 mod 256 + 
          lookup(element(fld_key(dnskey_record), [srcbyte + 3]))) mod 256 <= 
          255 .
H45:   start_byte + 9 + dstbytes >= 1 .
H46:   start_byte + 9 + (dstbytes + 2) <= 8180 .
H47:   dstbytes <= 1362 .
H48:   fld_keylength(dnskey_record) < srcbyte + 7 .
H49:   integer__size >= 0 .
H50:   character__size >= 0 .
H51:   positive__size >= 0 .
H52:   dns_types__packet_bytes_range__size >= 0 .
H53:   unsigned_types__unsigned8__size >= 0 .
H54:   unsigned_types__unsigned16__size >= 0 .
H55:   unsigned_types__unsigned32__size >= 0 .
H56:   rr_type__classtype__size >= 0 .
H57:   rr_type__resourcerecordtype__size >= 0 .
H58:   rr_type__dnskey_record_type__keylengthvaluetype__size >= 0 .
H59:   rr_type__dnskey_record_type__dnskeystringtypeindex__size >= 0 .
H60:   rr_type__dnskey_record_type__dnskeystringtype__size >= 0 .
H61:   rr_type__dnskey_record_type__dnskeyrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8176 .
C2:    start_byte <= 8175 .


For path(s) from start to finish:

procedure_set_ttl_data_dnskey_33.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_dnskey_34.
*** true .          /* all conclusions proved */


