with DNS_Types;
WITH DNS_Network;
with DNS_Network_Receive;
with DNS_Table_Pkg;
with RR_Type;
with RR_Type.a_record_type;
with RR_Type.Aaaa_Record_Type;
with RR_Type.Cname_Record_Type;
with RR_Type.ns_record_type;
with RR_Type.Mx_Record_Type;
with RR_Type.Ptr_Record_Type;
with RR_Type.soa_record_type;
with Unsigned_Types;
--# inherit DNS_types, DNS_Network, DNS_Network_Receive, System, Protected_SPARK_IO_05,
--#          RR_Type, RR_Type.a_record_type, RR_Type.aaaa_record_type,
--#          RR_Type.cname_record_type, RR_Type.ns_record_type,
--#          RR_type.mx_record_type, RR_Type.ptr_record_type,
--#          RR_type.soa_record_type,
--#          DNS_Table_Pkg, Unsigned_Types, ada.Unchecked_Conversion;
package Process_Dns_Request is
   procedure Process_Request_Tcp(
      Reply_Socket : in DNS_Network.DNS_Socket);
      --# global in out Protected_SPARK_IO_05.SPARK_IO_PO;
      --#        in out DNS_Network.Network;
      --#        in DNS_Table_Pkg.DNS_Table;
      --# derives DNS_Network.Network from DNS_Table_Pkg.DNS_Table, DNS_Network.Network, Reply_Socket &
      --#         Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, DNS_Network.Network, Reply_Socket;
   procedure Create_Response(
         Input_Packet  : in DNS_Types.DNS_Packet;
         Input_Bytes   : in DNS_Types.Packet_Length_Range;
         Output_Packet : in out DNS_Types.DNS_Packet;
         Output_Bytes  : out DNS_Types.Packet_Length_Range;
         Max_Transmit  : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --#        in out Protected_SPARK_IO_05.SPARK_IO_PO;
   --# derives Output_Packet from *, DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes &
   --#         Output_Bytes from  Output_Packet, Input_Bytes, Input_Packet, DNS_Table_Pkg.DNS_Table &
   --#         Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes &
   --#         Max_Transmit from DNS_Table_Pkg.DNS_Table, Input_Packet, Input_Bytes;
   --# pre Integer(Input_Bytes) >=DNS_Types.Header_Bits/8+1
   --#     and Integer(Input_Bytes) < 312;
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#      Integer(Max_Transmit) <= DNS_Types.Packet_Size and Max_Transmit >= DNS_Types.UDP_Max_Size;
private
   procedure Set_Unsigned_32(
         Bytes : in out DNS_Types.Bytes_Array_Type;
         Start_Byte : in DNS_Types.Packet_Bytes_Range;
         Value : in Unsigned_Types.Unsigned32);
   --# derives Bytes from *, Start_Byte, Value;
   --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-3;

   procedure Set_Unsigned_16(
         Bytes : in out DNS_Types.Bytes_Array_Type;
         Start_Byte : in DNS_Types.Packet_Bytes_Range;
         Value : in Unsigned_Types.Unsigned16);
   --# derives Bytes from *, Start_Byte, Value;
   --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-1;

   procedure Get_Query_Name_Type_Class(
      Input_Packet  : in DNS_Types.DNS_Packet;
      Input_Bytes   : in DNS_Types.Packet_Length_Range;
      Domainname    : out RR_Type.WireStringType;
      Query_Type    : out DNS_Types.Query_Type;
      Query_Class   : out DNS_Types.Query_Class;
      End_Byte      : out Dns_types.Packet_Bytes_Range);
   --# derives Domainname from Input_Packet,Input_Bytes &
   --#         Query_Type from Input_Packet,Input_Bytes &
   --#         Query_Class from Input_Packet,Input_Bytes &
   --#         End_Byte from Input_Packet,Input_Bytes;
   --# pre Input_Bytes >=DNS_Types.Header_Bits/8+1 and Input_Bytes < 1000;
   --# post Integer(End_Byte) <= Integer(Input_Bytes) and End_Byte >= 4;

   procedure Set_TTL_Data_IP(
      Bytes      : in out DNS_Types.Bytes_Array_Type;
      Start_Byte : in DNS_Types.Packet_Bytes_Range;
      A_Record   : in Rr_Type.A_Record_Type.ARecordType);
   --# derives Bytes from *, Start_Byte, A_Record;
   --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-10;

   procedure Set_TTL_Data_AAAA_IP(
      Bytes      : in out DNS_Types.Bytes_Array_Type;
      Start_Byte : in DNS_Types.Packet_Bytes_Range;
      AAAA_Record   : in Rr_Type.AAAA_Record_Type.AAAARecordType);
   --# derives Bytes from *, Start_Byte, AAAA_Record;
   --# pre Start_Byte <= DNS_Types.Packet_Bytes_Range'Last-22;


   procedure Set_TTL_Data_NS_Response(
         Bytes               : in out DNS_Types.Bytes_Array_Type;
         Start_Byte          : in DNS_Types.Packet_Bytes_Range;
         NS_Record           : in Rr_Type.ns_record_type.NSRecordType;
         Current_Name_Length : in RR_Type.WireStringTypeIndex);
   --# derives Bytes from *, Start_Byte, NS_Record, Current_Name_Length;
   --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
   --#     Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);

   procedure Set_TTL_Data_PTR_Response(
         Bytes                : in out DNS_Types.Bytes_Array_Type;
         Start_Byte           : in DNS_Types.Packet_Bytes_Range;
         PTR_Record           : in Rr_Type.ptr_record_type.PTRRecordType;
         Current_Name_Length  : in RR_Type.WireStringTypeIndex);
   --# derives Bytes from *, Start_Byte, PTR_Record, Current_Name_Length;
   --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
   --#     Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-6)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);

   procedure Set_TTL_Data_MX_Response(
         Bytes               : in out DNS_Types.Bytes_Array_Type;
         Start_Byte          : in DNS_Types.Packet_Bytes_Range;
         MX_Record           : in Rr_Type.MX_record_type.MXRecordType;
         Current_Name_Length : in RR_Type.WireStringTypeIndex);
   --# derives Bytes from *, Start_Byte, MX_Record, Current_Name_Length;
   --# pre Current_Name_Length >= 0 and Current_Name_Length<=RR_Type.WireStringTypeIndex'Last and
   --#     Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-8)-DNS_Types.Packet_Bytes_Range(Current_Name_Length);

   procedure Set_TTL_Data_SOA_Response(
         Bytes                  : in out DNS_Types.Bytes_Array_Type;
         Start_Byte             : in DNS_Types.Packet_Bytes_Range;
         SOA_Record             : in Rr_Type.SOA_record_type.SOARecordType;
         Nameserver_Name_Length : in RR_Type.WireStringTypeIndex;
         Mailbox_Name_Length    : in RR_Type.WireStringTypeIndex);
   --# derives Bytes from *, Start_Byte, SOA_Record, Nameserver_Name_Length, Mailbox_Name_Length;
   --# pre Nameserver_Name_Length >= 0 and Nameserver_Name_Length<=RR_Type.WireStringTypeIndex'Last and
   --#     Mailbox_Name_Length >= 0 and Mailbox_Name_Length<=RR_Type.WireStringTypeIndex'Last and
   --#     Start_Byte <= (DNS_Types.Packet_Bytes_Range'Last-26)-
   --#        DNS_Types.Packet_Bytes_Range(Nameserver_Name_Length+Mailbox_Name_Length);


   procedure Create_Response_EDNS(
         Input_Packet       : in DNS_Types.DNS_Packet;
         Input_Bytes        : in DNS_Types.Packet_Length_Range;
         Query_End_Byte     : in DNS_Types.Packet_Bytes_Range;
         Start_Byte         : in DNS_Types.Packet_Bytes_Range;
         Output_Packet      : in out DNS_Types.DNS_Packet;
         Output_Bytes       : out DNS_Types.Packet_Length_Range;
         Additional_Count   : in out DNS_Types.Unsigned_Short;
         DNSSEC             : out Boolean;
         Max_Transmit       : out DNS_Types.Packet_Length_Range);
   --# derives Output_Packet from *, Start_Byte, Input_Packet, Input_Bytes, Query_End_Byte &
   --#         Output_Bytes from Start_Byte, Input_Packet, Input_Bytes, Query_End_Byte &
   --#         Max_Transmit from Start_Byte, Input_Bytes, Input_Packet, Query_End_Byte &
   --#         DNSSEC from Start_Byte, Input_Bytes, Input_Packet, Query_End_Byte &
   --#         Additional_Count from *, Input_Packet, Start_Byte, Input_Bytes, Query_End_Byte;
   --# pre Additional_Count < DNS_Types.Unsigned_Short'Last;
   --# post Additional_Count >= Additional_Count~ and Additional_Count <= Additional_Count~+1 and
   --#      Max_Transmit >= DNS_Types.UDP_Max_Size and Max_Transmit <= DNS_Types.Packet_Size;

   procedure Create_Response_A(
         Start_Byte     : in DNS_Types.Packet_Bytes_Range;
         Domainname     : in RR_Type.WireStringType;
         Qname_Location : in DNS_Types.QNAME_PTR_RANGE;
         Output_Packet  : in out DNS_Types.DNS_Packet;
         Answer_Count   : in out DNS_Types.Unsigned_Short;
         Output_Bytes   : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Qname_Location, Start_Byte, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
   --# pre Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords)
   --#     and Integer(Start_Byte) <= DNS_Types.Packet_Size;
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#      Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);

   procedure Create_NXDOMAIN_Response(
         Start_Byte      : in DNS_Types.Packet_Bytes_Range;
         Domainname      : in RR_Type.WireStringType;
         Qname_Location  : in DNS_Types.QNAME_PTR_RANGE;
         Output_Packet   : in out DNS_Types.DNS_Packet;
         Output_Bytes    : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Qname_Location, Start_Byte, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Qname_Location, Start_Byte, DNS_Table_Pkg.DNS_Table;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size;
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size;


   procedure Create_Response_AAAA(
         Start_Byte     : in DNS_Types.Packet_Bytes_Range;
         Domainname     : in RR_Type.WireStringType;
         Qname_Location : in DNS_Types.QNAME_PTR_RANGE;
         Output_Packet  : in out DNS_Types.DNS_Packet;
         Answer_Count   : in out DNS_Types.Unsigned_Short;
         Output_Bytes   : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#      Answer_Count <= Answer_Count~ + DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);


   procedure Process_Response_Cname(
         Start_Byte     : in DNS_Types.Packet_Bytes_Range;
         Cnames         : in RR_Type.cname_record_type.CNAMERecordBucketType;
         Domainname     : out RR_Type.WireStringType;
         Qname_Location : in out DNS_Types.QNAME_PTR_RANGE;
         Output_Packet  : in out DNS_Types.DNS_Packet;
         Output_Bytes   : out DNS_Types.Packet_Length_Range);
   --# derives Domainname from Cnames &
   --#         Qname_Location from Start_Byte &
   --#         Output_Packet from *, Qname_Location, Start_Byte, Cnames &
   --#         Output_Bytes from Cnames, Start_Byte;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size
   --#     and Output_Packet.Header.ANCount = 0;
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#      Output_Packet.Header.ANCount <= 1;

   procedure Create_Response_Error(
         Input_Bytes   : in DNS_Types.Packet_Length_Range;
         Output_Packet : in out DNS_Types.DNS_Packet;
         Output_Bytes  : out DNS_Types.Packet_Length_Range);
   --# derives Output_Packet from * &
   --#         Output_Bytes from Input_Bytes;
   --# post Output_Bytes = Input_Bytes;

   type QNAME_PTR_RANGE_Array is array(RR_Type.ReturnedRecordsIndexType) of DNS_Types.QNAME_PTR_RANGE;

   procedure Create_Response_NS(
         Start_Byte      : in DNS_Types.Packet_Bytes_Range;
         Domainname      : in RR_Type.WireStringType;
         Num_Found       : out RR_Type.NumberOfRecordsType;
         Qname_Location  : in DNS_Types.QNAME_PTR_RANGE;
         Qname_Locations : out QNAME_PTR_RANGE_Array;
         Replies         : out RR_Type.ns_record_type.NSRecordBucketType;
         Output_Packet   : in out DNS_Types.DNS_Packet;
         Answer_Count    : in out DNS_Types.Unsigned_Short;
         Output_Bytes    : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Num_Found from DNS_Table_Pkg.DNS_Table, Domainname &
   --#         Replies from DNS_Table_Pkg.DNS_Table, Domainname &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Qname_Locations from Start_Byte, DNS_Table_Pkg.DNS_Table, Domainname ;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);

   procedure Create_Response_PTR(
         Start_Byte      : in DNS_Types.Packet_Bytes_Range;
         Domainname      : in RR_Type.WireStringType;
         Qname_Location  : in DNS_Types.QNAME_PTR_RANGE;
         Output_Packet   : in out DNS_Types.DNS_Packet;
         Answer_Count    : in out DNS_Types.Unsigned_Short;
         Output_Bytes    : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);

   procedure Create_Response_MX(
         Start_Byte      : in DNS_Types.Packet_Bytes_Range;
         Domainname      : in RR_Type.WireStringType;
         Num_Found       : out RR_Type.NumberOfRecordsType;
         Qname_Location  : in DNS_Types.QNAME_PTR_RANGE;
         Qname_Locations : out QNAME_PTR_RANGE_Array;
         Replies         : out RR_Type.mx_record_type.MXRecordBucketType;
         Output_Packet   : in out DNS_Types.DNS_Packet;
         Answer_Count    : in out DNS_Types.Unsigned_Short;
         Output_Bytes    : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Num_Found from DNS_Table_Pkg.DNS_Table, Domainname &
   --#         Replies from DNS_Table_Pkg.DNS_Table, Domainname &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Qname_Locations from Start_Byte, DNS_Table_Pkg.DNS_Table, Domainname ;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);

   procedure Create_Response_SOA(
         Start_Byte      : in DNS_Types.Packet_Bytes_Range;
         Domainname      : in RR_Type.WireStringType;
         Qname_Location  : in DNS_Types.QNAME_PTR_RANGE;
         Output_Packet   : in out DNS_Types.DNS_Packet;
         Answer_Count    : in out DNS_Types.Unsigned_Short;
         Output_Bytes    : out DNS_Types.Packet_Length_Range);
   --# global in DNS_Table_Pkg.DNS_Table;
   --# derives Output_Packet from *, Start_Byte, Qname_Location, Domainname, DNS_Table_Pkg.DNS_Table &
   --#         Output_Bytes from Domainname, Start_Byte, DNS_Table_Pkg.DNS_Table &
   --#         Answer_Count from *, Domainname, DNS_Table_Pkg.DNS_Table;
   --# pre Integer(Start_Byte) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= DNS_Types.Unsigned_Short'Last-DNS_types.Unsigned_Short(rr_type.MaxNumRecords);
   --# post Integer(Output_Bytes) >= DNS_Types.Header_Bits/8+1 and Integer(Output_Bytes) <= DNS_Types.Packet_Size and
   --#     Answer_Count <= Answer_Count~+DNS_Types.Unsigned_Short(rr_type.MaxNumRecords);

   procedure Trim_Name(
      Domainname         : in RR_Type.WireStringType;
      Trimmed_name       : out RR_Type.WireStringType;
      Qname_Location     : in DNS_Types.QNAME_PTR_RANGE;
      New_Qname_Location : out DNS_Types.QNAME_PTR_RANGE);
   --# derives Trimmed_Name from Domainname &
   --#         New_Qname_Location from Domainname, Qname_Location;
   --# pre Qname_Location <= DNS_Types.QNAME_PTR_RANGE(DNS_Types.Packet_Length_Range'Last);
end Process_Dns_Request;