*****************************************************************************
                       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.Create_Response_Error






@@@@@@@@@@  VC: procedure_create_response_error_1.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  dns_types__response_code__first <= dns_types__not_implemented
-S-  Applied substitution rule create_respo_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H7:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New C1:  true
-S-  Applied substitution rule create_respo_rules(53).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H8:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_response_error_2.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  dns_types__response_code__first <= dns_types__not_implemented
-S-  Applied substitution rule create_respo_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H9:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H11:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H13:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New C1:  true
-S-  Applied substitution rule create_respo_rules(21).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H10:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H12:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_response_error_3.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  dns_types__response_code__first <= dns_types__not_implemented
***  Proved C1:  input_bytes >= dns_types__packet_length_range__first
     using hypothesis H1.
***  Proved C2:  input_bytes <= dns_types__packet_length_range__last
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_response_error_4.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  dns_types__response_code__first <= dns_types__not_implemented
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H2)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
***  Proved C1:  true
***  PROVED VC.

