*****************************************************************************
                       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_MX_Response




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

procedure_set_ttl_data_mx_response_1.
H1:    current_name_length <= 129 .
H2:    start_byte <= 8172 - current_name_length .
H3:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H4:    start_byte >= 1 .
H5:    fld_ttlinseconds(fld_inherit(mx_record)) >= 0 .
H6:    fld_ttlinseconds(fld_inherit(mx_record)) <= 4294967295 .
H7:    rr_type__internet <= fld_class(fld_inherit(mx_record)) .
H8:    fld_class(fld_inherit(mx_record)) <= rr_type__hs .
H9:    fld_pref(mx_record) >= 0 .
H10:   fld_pref(mx_record) <= 65535 .
H11:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_mailexchanger(mx_record), [i___1]) and element(fld_mailexchanger(
          mx_record), [i___1]) <= 255) .
H12:   current_name_length >= 1 .
H13:   integer__size >= 0 .
H14:   character__size >= 0 .
H15:   positive__size >= 0 .
H16:   dns_types__packet_bytes_range__size >= 0 .
H17:   unsigned_types__unsigned16__size >= 0 .
H18:   unsigned_types__unsigned32__size >= 0 .
H19:   rr_type__classtype__size >= 0 .
H20:   rr_type__wirestringtypeindex__size >= 0 .
H21:   rr_type__wirestringtype__size >= 0 .
H22:   rr_type__resourcerecordtype__size >= 0 .
H23:   rr_type__mx_record_type__mxrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8177 .


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

procedure_set_ttl_data_mx_response_2.
H1:    current_name_length <= 129 .
H2:    start_byte <= 8172 - current_name_length .
H3:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H4:    start_byte >= 1 .
H5:    fld_ttlinseconds(fld_inherit(mx_record)) >= 0 .
H6:    fld_ttlinseconds(fld_inherit(mx_record)) <= 4294967295 .
H7:    rr_type__internet <= fld_class(fld_inherit(mx_record)) .
H8:    fld_class(fld_inherit(mx_record)) <= rr_type__hs .
H9:    fld_pref(mx_record) >= 0 .
H10:   fld_pref(mx_record) <= 65535 .
H11:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_mailexchanger(mx_record), [i___1]) and element(fld_mailexchanger(
          mx_record), [i___1]) <= 255) .
H12:   current_name_length >= 1 .
H13:   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) .
H14:   integer__size >= 0 .
H15:   character__size >= 0 .
H16:   positive__size >= 0 .
H17:   dns_types__packet_bytes_range__size >= 0 .
H18:   unsigned_types__unsigned16__size >= 0 .
H19:   unsigned_types__unsigned32__size >= 0 .
H20:   rr_type__classtype__size >= 0 .
H21:   rr_type__wirestringtypeindex__size >= 0 .
H22:   rr_type__wirestringtype__size >= 0 .
H23:   rr_type__resourcerecordtype__size >= 0 .
H24:   rr_type__mx_record_type__mxrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8176 .
C2:    start_byte <= 8175 .


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

procedure_set_ttl_data_mx_response_3.
H1:    current_name_length <= 129 .
H2:    start_byte <= 8172 - current_name_length .
H3:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H4:    start_byte >= 1 .
H5:    fld_ttlinseconds(fld_inherit(mx_record)) >= 0 .
H6:    fld_ttlinseconds(fld_inherit(mx_record)) <= 4294967295 .
H7:    rr_type__internet <= fld_class(fld_inherit(mx_record)) .
H8:    fld_class(fld_inherit(mx_record)) <= rr_type__hs .
H9:    fld_pref(mx_record) >= 0 .
H10:   fld_pref(mx_record) <= 65535 .
H11:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_mailexchanger(mx_record), [i___1]) and element(fld_mailexchanger(
          mx_record), [i___1]) <= 255) .
H12:   current_name_length >= 1 .
H13:   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) .
H14:   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) .
H15:   integer__size >= 0 .
H16:   character__size >= 0 .
H17:   positive__size >= 0 .
H18:   dns_types__packet_bytes_range__size >= 0 .
H19:   unsigned_types__unsigned16__size >= 0 .
H20:   unsigned_types__unsigned32__size >= 0 .
H21:   rr_type__classtype__size >= 0 .
H22:   rr_type__wirestringtypeindex__size >= 0 .
H23:   rr_type__wirestringtype__size >= 0 .
H24:   rr_type__resourcerecordtype__size >= 0 .
H25:   rr_type__mx_record_type__mxrecordtype__size >= 0 .
       ->
C1:    start_byte <= 8173 .


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

procedure_set_ttl_data_mx_response_4.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_mx_response_5.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_mx_response_6.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_mx_response_7.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_mx_response_8.
H1:    start_byte <= 8172 - current_name_length .
H2:    loop__1__i >= 1 .
H3:    loop__1__i <= 129 .
H4:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H5:    start_byte >= 1 .
H6:    fld_ttlinseconds(fld_inherit(mx_record)) >= 0 .
H7:    fld_ttlinseconds(fld_inherit(mx_record)) <= 4294967295 .
H8:    rr_type__internet <= fld_class(fld_inherit(mx_record)) .
H9:    fld_class(fld_inherit(mx_record)) <= rr_type__hs .
H10:   fld_pref(mx_record) >= 0 .
H11:   fld_pref(mx_record) <= 65535 .
H12:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_mailexchanger(mx_record), [i___1]) and element(fld_mailexchanger(
          mx_record), [i___1]) <= 255) .
H13:   current_name_length >= 1 .
H14:   current_name_length <= 129 .
H15:   loop__1__i <= current_name_length .
H16:   integer__size >= 0 .
H17:   character__size >= 0 .
H18:   positive__size >= 0 .
H19:   dns_types__packet_bytes_range__size >= 0 .
H20:   unsigned_types__unsigned16__size >= 0 .
H21:   unsigned_types__unsigned32__size >= 0 .
H22:   rr_type__classtype__size >= 0 .
H23:   rr_type__wirestringtypeindex__size >= 0 .
H24:   rr_type__wirestringtype__size >= 0 .
H25:   rr_type__resourcerecordtype__size >= 0 .
H26:   rr_type__mx_record_type__mxrecordtype__size >= 0 .
       ->
C1:    start_byte + 7 + loop__1__i <= 8180 .


For path(s) from start to finish:

procedure_set_ttl_data_mx_response_9.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_mx_response_10.
*** true .          /* all conclusions proved */


