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

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



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

task_type Udp_Dns_Package.Udp_Dns_Task




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

task_type_udp_dns_task_1.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_2.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_3.
*** true .          /* all conclusions proved */


task_type_udp_dns_task_4.
*** true .          /* all conclusions proved */


task_type_udp_dns_task_5.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_6.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_7.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_8.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_9.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_10.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_11.
H1:    fld_messageid(fld_header(input_packet__3)) >= 0 .
H2:    fld_messageid(fld_header(input_packet__3)) <= 65535 .
H3:    dns_types__query <= fld_opcode(fld_header(input_packet__3)) .
H4:    fld_opcode(fld_header(input_packet__3)) <= dns_types__status .
H5:    dns_types__no_error <= fld_rcode(fld_header(input_packet__3)) .
H6:    fld_rcode(fld_header(input_packet__3)) <= dns_types__refused .
H7:    fld_qdcount(fld_header(input_packet__3)) >= 0 .
H8:    fld_qdcount(fld_header(input_packet__3)) <= 65535 .
H9:    fld_ancount(fld_header(input_packet__3)) >= 0 .
H10:   fld_ancount(fld_header(input_packet__3)) <= 65535 .
H11:   fld_nscount(fld_header(input_packet__3)) >= 0 .
H12:   fld_nscount(fld_header(input_packet__3)) <= 65535 .
H13:   fld_arcount(fld_header(input_packet__3)) >= 0 .
H14:   fld_arcount(fld_header(input_packet__3)) <= 65535 .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= 255) .
H16:   fld_messageid(fld_header(output_packet)) >= 0 .
H17:   fld_messageid(fld_header(output_packet)) <= 65535 .
H18:   dns_types__query <= fld_opcode(fld_header(output_packet)) .
H19:   fld_opcode(fld_header(output_packet)) <= dns_types__status .
H20:   dns_types__no_error <= fld_rcode(fld_header(output_packet)) .
H21:   fld_rcode(fld_header(output_packet)) <= dns_types__refused .
H22:   fld_qdcount(fld_header(output_packet)) >= 0 .
H23:   fld_qdcount(fld_header(output_packet)) <= 65535 .
H24:   fld_ancount(fld_header(output_packet)) >= 0 .
H25:   fld_ancount(fld_header(output_packet)) <= 65535 .
H26:   fld_nscount(fld_header(output_packet)) >= 0 .
H27:   fld_nscount(fld_header(output_packet)) <= 65535 .
H28:   fld_arcount(fld_header(output_packet)) >= 0 .
H29:   fld_arcount(fld_header(output_packet)) <= 65535 .
H30:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255) .
H31:   input_bytes__3 >= 13 .
H32:   input_bytes__3 < 312 .
H33:   output_bytes__5 >= 13 .
H34:   output_bytes__5 <= 8192 .
H35:   max_transmit__5 <= 8192 .
H36:   max_transmit__5 >= 512 .
H37:   fld_messageid(fld_header(output_packet__5)) >= 0 .
H38:   fld_messageid(fld_header(output_packet__5)) <= 65535 .
H39:   dns_types__query <= fld_opcode(fld_header(output_packet__5)) .
H40:   fld_opcode(fld_header(output_packet__5)) <= dns_types__status .
H41:   dns_types__no_error <= fld_rcode(fld_header(output_packet__5)) .
H42:   fld_rcode(fld_header(output_packet__5)) <= dns_types__refused .
H43:   fld_qdcount(fld_header(output_packet__5)) >= 0 .
H44:   fld_qdcount(fld_header(output_packet__5)) <= 65535 .
H45:   fld_ancount(fld_header(output_packet__5)) >= 0 .
H46:   fld_ancount(fld_header(output_packet__5)) <= 65535 .
H47:   fld_nscount(fld_header(output_packet__5)) >= 0 .
H48:   fld_nscount(fld_header(output_packet__5)) <= 65535 .
H49:   fld_arcount(fld_header(output_packet__5)) >= 0 .
H50:   fld_arcount(fld_header(output_packet__5)) <= 65535 .
H51:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          fld_bytes(output_packet__5), [i___1]) and element(fld_bytes(
          output_packet__5), [i___1]) <= 255) .
H52:   dns_types__packet_length_range__min(max_transmit__5, output_bytes__5) >= 
          0 .
H53:   dns_types__packet_length_range__min(max_transmit__5, output_bytes__5) <= 
          8192 .
H54:   input_bytes__3 <= 311 .
H55:   integer__size >= 0 .
H56:   natural__size >= 0 .
H57:   system__bit_order__size >= 0 .
H58:   dns_types__packet_length_range__size >= 0 .
H59:   dns_types__packet_bytes_range__size >= 0 .
H60:   dns_types__dns_packet__size >= 0 .
       ->
C1:    dns_types__packet_length_range__min(max_transmit__5, output_bytes__5) > 
          12 .


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

task_type_udp_dns_task_12.
*** true .          /* all conclusions proved */


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

task_type_udp_dns_task_13.
*** true .          /* all conclusions proved */


task_type_udp_dns_task_14.
*** true .          /* all conclusions proved */


task_type_udp_dns_task_15.
*** true .          /* all conclusions proved */


