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






@@@@@@@@@@  VC: procedure_set_unsigned_16_1.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus >= dns_types__byte__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus <= dns_types__byte__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus >= dns_types__byte__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus <= dns_types__byte__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  true
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  256 >= system__min_int
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  256 <= system__max_int
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C5:  true
***  Proved C6:  true
***  Proved C9:  true
***  Proved C10:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H3.
***  Proved C11:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H4.
-S-  Applied substitution rule set_unsigned_rules(10).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H2:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New C1:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus >= 0
<S>  New C3:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus >= 0
-S-  Applied substitution rule set_unsigned_rules(11).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New C2:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus <= 255
<S>  New C4:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus <= 255
-S-  Applied substitution rule set_unsigned_rules(1).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New C7:  true
-S-  Applied substitution rule set_unsigned_rules(2).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New C8:  true
***  Proved C7:  true
***  Proved C8:  true
-S-  Applied substitution rule set_unsigned_rules(4).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> 0 <= element(bytes, [i___1]) 
          and element(bytes, [i___1]) <= 255)
<S>  New H3:  start_byte >= 1
-S-  Applied substitution rule set_unsigned_rules(5).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H1:  start_byte <= 8179
<S>  New H4:  start_byte <= 8180
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S-  Applied substitution rule set_unsigned_rules(16).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H5:  value >= 0
-S-  Applied substitution rule set_unsigned_rules(17).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H6:  value <= 65535
-S-  Applied substitution rule set_unsigned_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__modulus by:
          65536.
<S>  New C1:  value div 256 mod 65536 mod 256 mod 65536 >= 0
<S>  New C3:  value div 256 mod 65536 mod 256 mod 65536 >= 0
<S>  New C2:  value div 256 mod 65536 mod 256 mod 65536 <= 255
<S>  New C4:  value div 256 mod 65536 mod 256 mod 65536 <= 255
***  Proved C1:  value div 256 mod 65536 mod 256 mod 65536 >= 0
***  Proved C3:  value div 256 mod 65536 mod 256 mod 65536 >= 0
---  Eliminated hypothesis H4 (redundant, given H1).
---  Eliminated conclusion C4, which is a duplicate of C2.
***  Proved C2:  value div 256 mod 65536 mod 256 mod 65536 <= 255
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_unsigned_16_2.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus >= dns_types__byte__first
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 
          mod unsigned_types__unsigned16__modulus <= dns_types__byte__last
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H7).
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H8)
          .
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  true
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  true
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  256 >= system__min_int
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  256 <= system__max_int
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  true
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
***  Proved C5:  true
***  Proved C6:  start_byte + 1 >= dns_types__packet_bytes_range__first
     using hypothesis H3.
***  Proved C7:  start_byte + 1 <= dns_types__packet_bytes_range__last
     using hypothesis H1.
-S-  Applied substitution rule set_unsigned_rules(10).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H2:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H7:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus >= 0
<S>  New C1:  value mod 256 mod unsigned_types__unsigned16__modulus >= 0
<S>  New C3:  value mod 256 mod unsigned_types__unsigned16__modulus >= 0
-S-  Applied substitution rule set_unsigned_rules(11).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H8:  value div 256 mod unsigned_types__unsigned16__modulus mod 256 mod 
          unsigned_types__unsigned16__modulus <= 255
<S>  New H2:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New C2:  value mod 256 mod unsigned_types__unsigned16__modulus <= 255
<S>  New C4:  value mod 256 mod unsigned_types__unsigned16__modulus <= 255
-S-  Applied substitution rule set_unsigned_rules(6).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New C8:  start_byte >= - 2147483649
-S-  Applied substitution rule set_unsigned_rules(7).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New C9:  start_byte <= 2147483646
-S-  Applied substitution rule set_unsigned_rules(1).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H13:  true
-S-  Applied substitution rule set_unsigned_rules(2).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H14:  true
-S-  Applied substitution rule set_unsigned_rules(4).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> 0 <= element(bytes, [i___1]) 
          and element(bytes, [i___1]) <= 255)
<S>  New H3:  start_byte >= 1
-S-  Applied substitution rule set_unsigned_rules(5).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H1:  start_byte <= 8179
<S>  New H4:  start_byte <= 8180
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S-  Applied substitution rule set_unsigned_rules(16).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H5:  value >= 0
-S-  Applied substitution rule set_unsigned_rules(17).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H6:  value <= 65535
-S-  Applied substitution rule set_unsigned_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__modulus by:
          65536.
<S>  New H7:  value div 256 mod 65536 mod 256 mod 65536 >= 0
<S>  New H8:  value div 256 mod 65536 mod 256 mod 65536 <= 255
<S>  New C1:  value mod 256 mod 65536 >= 0
<S>  New C3:  value mod 256 mod 65536 >= 0
<S>  New C2:  value mod 256 mod 65536 <= 255
<S>  New C4:  value mod 256 mod 65536 <= 255
***  Proved C8:  start_byte >= - 2147483649
     using hypothesis H3.
***  Proved C9:  start_byte <= 2147483646
     using hypothesis H1.
***  Proved C1:  value mod 256 mod 65536 >= 0
***  Proved C3:  value mod 256 mod 65536 >= 0
---  Eliminated hypothesis H9 (true-hypothesis).
---  Eliminated hypothesis H10 (true-hypothesis).
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H17 (true-hypothesis).
---  Eliminated hypothesis H13 (true-hypothesis).
---  Eliminated hypothesis H14 (true-hypothesis).
---  Eliminated hypothesis H4 (redundant, given H1).
---  Eliminated conclusion C4, which is a duplicate of C2.
***  Proved C2:  value mod 256 mod 65536 <= 255
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_unsigned_16_3.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.

