123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142 |
- with GNAT.Sockets;
- with WolfSSL;
- package SPARK_Sockets with SPARK_Mode is
- subtype Byte_Array is WolfSSL.Byte_Array;
- subtype Byte_Index is WolfSSL.Byte_Index; use type Byte_Index;
- subtype Port_Type is GNAT.Sockets.Port_Type;
- subtype Level_Type is GNAT.Sockets.Level_Type;
- subtype Socket_Type is GNAT.Sockets.Socket_Type;
- subtype Option_Name is GNAT.Sockets.Option_Name;
- subtype Option_Type is GNAT.Sockets.Option_Type;
- subtype Family_Type is GNAT.Sockets.Family_Type;
- subtype Sock_Addr_Type is GNAT.Sockets.Sock_Addr_Type;
- subtype Inet_Addr_Type is GNAT.Sockets.Inet_Addr_Type;
- Socket_Error : exception renames GNAT.Sockets.Socket_Error;
- Reuse_Address : Option_Name renames GNAT.Sockets.Reuse_Address;
- Socket_Level : Level_Type renames GNAT.Sockets.Socket_Level;
- Family_Inet : Family_Type renames GNAT.Sockets.Family_Inet;
- use type GNAT.Sockets.Family_Type;
- Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr;
- subtype Subprogram_Result is WolfSSL.Subprogram_Result;
- use type Subprogram_Result;
- Success : Subprogram_Result renames WolfSSL.Success;
- Failure : Subprogram_Result renames WolfSSL.Failure;
- type Optional_Inet_Addr (Exists : Boolean := False) is record
- case Exists is
- when True => Addr : Inet_Addr_Type;
- when False => null;
- end case;
- end record;
- function Inet_Addr (Image : String) return Optional_Inet_Addr;
- type Optional_Socket (Exists : Boolean := False) is record
- case Exists is
- when True => Socket : Socket_Type;
- when False => null;
- end case;
- end record;
- procedure Create_Stream_Socket (Socket : in out Optional_Socket) with
- Pre => not Socket.Exists;
- procedure Create_Datagram_Socket (Socket : in out Optional_Socket) with
- Pre => not Socket.Exists;
- function Connect_Socket (Socket : Socket_Type;
- Server : Sock_Addr_Type)
- return Subprogram_Result;
- function To_C (Socket : Socket_Type) return Integer with Inline;
-
- procedure Close_Socket (Socket : in out Optional_Socket) with
- Pre => Socket.Exists,
- Post => not Socket.Exists;
- function Set_Socket_Option (Socket : Socket_Type;
- Level : Level_Type;
- Option : Option_Type)
- return Subprogram_Result;
-
- function Bind_Socket (Socket : Socket_Type;
- Address : Sock_Addr_Type)
- return Subprogram_Result;
- function Listen_Socket (Socket : Socket_Type;
- Length : Natural) return Subprogram_Result;
-
-
-
-
-
-
- function Receive_Socket (Socket : Socket_Type) return Subprogram_Result;
- procedure Accept_Socket (Server : Socket_Type;
- Socket : out Optional_Socket;
- Address : out Sock_Addr_Type;
- Result : out Subprogram_Result) with
- Post => (if Result = Success then Socket.Exists else not Socket.Exists);
- procedure To_C (Item : String;
- Target : out Byte_Array;
- Count : out Byte_Index) with
- Pre => Item'Length <= Target'Length,
- Post => Count <= Target'Last;
- procedure To_Ada (Item : Byte_Array;
- Target : out String;
- Count : out Natural) with
- Pre => Item'Length <= Target'Length,
- Post => Count <= Target'Last;
- end SPARK_Sockets;
|