84 lines
3.4 KiB
Plaintext
84 lines
3.4 KiB
Plaintext
|
*******************************************************
|
||
|
Listing of SPARK Text
|
||
|
Examiner GPL Edition
|
||
|
|
||
|
*******************************************************
|
||
|
|
||
|
|
||
|
Line
|
||
|
----------------------------------------------------------------
|
||
|
-- IRONSIDES - DNS SERVER
|
||
|
--
|
||
|
-- By: Martin C. Carlisle and Barry S. Fagin
|
||
|
-- Department of Computer Science
|
||
|
-- United States Air Force Academy
|
||
|
--
|
||
|
-- This is free software; you can redistribute it and/or
|
||
|
-- modify without restriction. We do ask that you please keep
|
||
|
-- the original author information, and clearly indicate if the
|
||
|
-- software has been modified.
|
||
|
--
|
||
|
-- This software is distributed in the hope that it will be useful,
|
||
|
-- but WITHOUT ANY WARRANTY; without even the implied warranty
|
||
|
-- of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
|
||
|
----------------------------------------------------------------
|
||
|
|
||
|
with Process_Dns_Request;
|
||
|
with Task_Limit;
|
||
|
^
|
||
|
--- Warning :391: If the identifier Task_Limit represents a
|
||
|
package which contains a task or an interrupt handler then the
|
||
|
partition-level analysis performed by the Examiner will be
|
||
|
incomplete. Such packages must be inherited as well as withed.
|
||
|
|
||
|
package body Multitask_Process_Dns_Request is
|
||
|
--# hide Multitask_Process_Dns_Request;
|
||
|
Task_Limit_Object : Task_Limit.Task_Count_Type;
|
||
|
task type Handle_Tcp_Request
|
||
|
--# global in out Protected_SPARK_IO_05.SPARK_IO_PO;
|
||
|
--# in out DNS_Network.Network;
|
||
|
--# derives DNS_Network.Network from DNS_Network.Network, Reply_Socket &
|
||
|
--# Protected_SPARK_IO_05.SPARK_IO_PO from *, DNS_Network.Network, Reply_Socket;
|
||
|
is
|
||
|
entry start(Reply_Socket : in DNS_Network.DNS_Socket);
|
||
|
pragma Priority(0);
|
||
|
end Handle_Tcp_Request;
|
||
|
type Task_Ptr is access all Handle_Tcp_Request;
|
||
|
|
||
|
task body Handle_Tcp_Request is
|
||
|
The_Socket : DNS_Network.DNS_Socket;
|
||
|
begin
|
||
|
accept Start(Reply_Socket : in DNS_Network.DNS_Socket) do
|
||
|
The_Socket := Reply_Socket;
|
||
|
end Start;
|
||
|
|
||
|
Process_Dns_Request.Process_Request_Tcp(Reply_Socket => The_Socket);
|
||
|
Task_Limit_Object.Decrement;
|
||
|
end Handle_Tcp_Request;
|
||
|
|
||
|
procedure Process_Request_Tcp(
|
||
|
Reply_Socket : in DNS_Network.DNS_Socket) is
|
||
|
T : Task_Ptr;
|
||
|
Success : Boolean;
|
||
|
begin
|
||
|
Task_Limit_Object.Increment(Success);
|
||
|
if Success then
|
||
|
T := new Handle_Tcp_Request;
|
||
|
T.Start(Reply_Socket);
|
||
|
else
|
||
|
DNS_Network.Discard_Socket(Reply_Socket);
|
||
|
end if;
|
||
|
--Process_Dns_Request.Process_Request_Tcp(Reply_Socket => Reply_Socket);
|
||
|
end Process_Request_Tcp;
|
||
|
|
||
|
|
||
|
end Multitask_Process_Dns_Request;
|
||
|
|
||
|
--- Warning : 10: The body of package
|
||
|
Multitask_Process_Dns_Request is hidden - hidden text is ignored by
|
||
|
the Examiner.
|
||
|
|
||
|
|
||
|
|
||
|
--End of file--------------------------------------------------
|