diff --git a/src/ada/net_mem_interface.adb b/src/ada/net_mem_interface.adb index 53017c6..00a1c14 100644 --- a/src/ada/net_mem_interface.adb +++ b/src/ada/net_mem_interface.adb @@ -46,8 +46,8 @@ is Error : out Error_T) is begin - Error := Error_T'Enum_Val(netBufferSetLength - (Buffer'Address, unsigned_long(Length))); + Error := Error_T'Enum_Val (netBufferSetLength + (Buffer'Address, unsigned_long (Length))); end Net_Rx_Buffer_Set_Length; procedure Mem_Pool_Free diff --git a/src/ada/socket_helper.adb b/src/ada/socket_helper.adb index 27bbe05..df55cdd 100644 --- a/src/ada/socket_helper.adb +++ b/src/ada/socket_helper.adb @@ -38,8 +38,8 @@ is Sock := getSocketFromTable (unsigned (Index)); end Get_Socket_From_Table; - -- Temporaire, à supprimer. - -- Juste pour faire tourner gnatprove pour le moment + -- Temporaire, à supprimer. + -- Juste pour faire tourner gnatprove pour le moment procedure Get_Host_By_Name_H (Server_Name : char_array; Server_Ip_Addr : out IpAddr; diff --git a/src/ada/socket_interface.adb b/src/ada/socket_interface.adb index 5df26d8..e0eb46f 100644 --- a/src/ada/socket_interface.adb +++ b/src/ada/socket_interface.adb @@ -36,7 +36,8 @@ is Flags : Host_Resolver; Error : out Error_T) is begin - Get_Host_By_Name_H (Server_Name, Server_Ip_Addr, unsigned (Flags), Error); + Get_Host_By_Name_H + (Server_Name, Server_Ip_Addr, unsigned (Flags), Error); end Get_Host_By_Name; ----------------- @@ -52,21 +53,21 @@ is P : Port; Protocol : Socket_Protocol := S_Protocol; begin - -- Initialize socket handle + -- Initialize socket handle Sock := null; Os_Acquire_Mutex (Net_Mutex); case S_Type is when SOCKET_TYPE_STREAM => - -- Always use TCP as underlying transport protocol + -- Always use TCP as underlying transport protocol Protocol := SOCKET_IP_PROTO_TCP; - -- Get an ephemeral port number + -- Get an ephemeral port number Tcp_Get_Dynamic_Port (P); Error := NO_ERROR; when SOCKET_TYPE_DGRAM => - -- Always use UDP as underlying transport protocol + -- Always use UDP as underlying transport protocol Protocol := SOCKET_IP_PROTO_UDP; - -- Get an ephemeral port number + -- Get an ephemeral port number P := Udp_Get_Dynamic_Port; Error := NO_ERROR; when SOCKET_TYPE_RAW_IP | SOCKET_TYPE_RAW_ETH => @@ -81,23 +82,23 @@ is for I in Socket_Table'Range loop if Socket_Table (I).S_Type = SOCKET_TYPE_UNUSED then - -- Save socket handle + -- Save socket handle Get_Socket_From_Table (I, Sock); - -- We are done + -- We are done exit; end if; end loop; if Sock = null then - -- Kill the oldest connection in the TIME-WAIT state whenever the - -- socket table runs out of space + -- Kill the oldest connection in the TIME-WAIT state whenever the + -- socket table runs out of space Tcp_Kill_Oldest_Connection (Sock); end if; - -- Check whether the current entry is free + -- Check whether the current entry is free if Sock /= null then - -- Reset Socket - -- Maybe there is a simplest way to perform that in Ada + -- Reset Socket + -- Maybe there is a simplest way to perform that in Ada Sock.S_Type := S_Type; Sock.S_Protocol := Protocol; Sock.S_Local_Port := P; @@ -113,7 +114,8 @@ is Sock.S_Event_Flags := 0; Sock.S_User_Event := null; pragma Annotate (GNATprove, False_Positive, - "memory leak might occur", "Memory should already be free"); + "memory leak might occur", + "Memory should already be free"); Sock.State := TCP_STATE_CLOSED; Sock.owned_Flag := False; Sock.closed_Flag := False; @@ -152,8 +154,9 @@ is Sock.retransmitCount := 0; Sock.synQueue := null; pragma Annotate (GNATprove, False_Positive, - "memory leak might occur", "Memory should already be free"); - -- Limit the number of pending connections + "memory leak might occur", + "Memory should already be free"); + -- Limit the number of pending connections Sock.synQueueSize := TCP_DEFAULT_SYN_QUEUE_SIZE; Sock.wndProbeCount := 0; Sock.wndProbeInterval := 0; @@ -161,7 +164,8 @@ is Sock.sackBlockCount := 0; Sock.receiveQueue := null; pragma Annotate (GNATprove, False_Positive, - "memory leak might occur", "Memory should already be free"); + "memory leak might occur", + "Memory should already be free"); end if; end if; @@ -221,21 +225,21 @@ is Error : out Error_T) is begin - -- Connection oriented socket? + -- Connection oriented socket? if Sock.S_Type = SOCKET_TYPE_STREAM then Os_Acquire_Mutex (Net_Mutex); Tcp_Process_Segment (Sock); - -- Establish TCP connection + -- Establish TCP connection Tcp_Connect (Sock, Remote_Ip_Addr, Remote_Port, Error); Os_Release_Mutex (Net_Mutex); - -- Connectionless socket? + -- Connectionless socket? elsif Sock.S_Type = SOCKET_TYPE_DGRAM then Sock.S_Remote_Ip_Addr := Remote_Ip_Addr; Sock.S_Remote_Port := Remote_Port; Error := NO_ERROR; - -- Raw Socket? + -- Raw Socket? elsif Sock.S_Type = SOCKET_TYPE_RAW_IP then Sock.S_Remote_Ip_Addr := Remote_Ip_Addr; Error := NO_ERROR; @@ -262,11 +266,12 @@ is Os_Acquire_Mutex (Net_Mutex); if Sock.S_Type = SOCKET_TYPE_STREAM then - -- INTERFERENCES + -- INTERFERENCES Tcp_Process_Segment (Sock); Tcp_Send (Sock, Data, Written, Flags, Error); elsif Sock.S_Type = SOCKET_TYPE_DGRAM then - Udp_Send_Datagram (Sock, Dest_Ip_Addr, Dest_Port, Data, Written, Flags, Error); + Udp_Send_Datagram + (Sock, Dest_Ip_Addr, Dest_Port, Data, Written, Flags, Error); else Error := ERROR_INVALID_SOCKET; end if; @@ -289,11 +294,11 @@ is Os_Acquire_Mutex (Net_Mutex); if Sock.S_Type = SOCKET_TYPE_STREAM then - -- INTERFERENCES + -- INTERFERENCES Tcp_Process_Segment (Sock); Tcp_Send (Sock, Data, Written, Flags, Error); elsif Sock.S_Type = SOCKET_TYPE_DGRAM then - -- @TODO : See how to improve this part without using .all + -- @TODO : See how to improve this part without using .all Udp_Send_Datagram (Sock => Sock, Dest_Ip_Addr => IpAddr'(Length => Sock.S_Remote_Ip_Addr.Length, @@ -327,14 +332,14 @@ is Os_Acquire_Mutex (Net_Mutex); if Sock.S_Type = SOCKET_TYPE_STREAM then - -- INTERFERENCES + -- INTERFERENCES Tcp_Process_Segment (Sock); Tcp_Receive (Sock, Data, Received, Flags, Error); - -- Save the source IP address + -- Save the source IP address Src_Ip_Addr := Sock.S_Remote_Ip_Addr; - -- Save the source port number + -- Save the source port number Src_Port := Sock.S_Remote_Port; - -- Save the destination IP address + -- Save the destination IP address Dest_Ip_Addr := Sock.S_localIpAddr; elsif Sock.S_Type = SOCKET_TYPE_DGRAM then Udp_Receive_Datagram @@ -399,7 +404,7 @@ is procedure Socket_Close (Sock : in out Socket) is Ignore_Error : Error_T; begin - -- Get exclusive access + -- Get exclusive access Os_Acquire_Mutex (Net_Mutex); if Sock.S_Type = SOCKET_TYPE_STREAM then @@ -409,37 +414,38 @@ is | SOCKET_TYPE_RAW_IP | SOCKET_TYPE_RAW_ETH then - -- @TODO Have a look at this section to see if the code is - -- valid, in particular in what is done with pointers. + -- @TODO Have a look at this section to see if the code is + -- valid, in particular in what is done with pointers. declare - -- Point to the first item in the receive queue + -- Point to the first item in the receive queue Queue_Item : Socket_Queue_Item_Acc := Sock.receiveQueue; begin - -- Purge the receive queue + -- Purge the receive queue while Queue_Item /= null loop declare - -- Keep track of the next item in the queue - Next_Queue_Item : Socket_Queue_Item_Acc := Queue_Item.Next; + -- Keep track of the next item in the queue + Next_Queue_Item : constant Socket_Queue_Item_Acc + := Queue_Item.Next; begin Queue_Item.Next := null; - -- Free previously allocated memory - -- netBufferFree(queueItem.Buffer); in the c code + -- Free previously allocated memory + -- netBufferFree(queueItem.Buffer); in the c code Net_Buffer_Free (Queue_Item); - -- Point to the next item + -- Point to the next item Queue_Item := Next_Queue_Item; end; end loop; Sock.receiveQueue := null; end; - -- Mark the socket as closed + -- Mark the socket as closed Sock.S_Type := SOCKET_TYPE_UNUSED; - -- Fake free the socket + -- Fake free the socket Free_Socket (Sock); end if; - -- Release exclusive access + -- Release exclusive access Os_Release_Mutex (Net_Mutex); end Socket_Close; @@ -488,7 +494,7 @@ is procedure Socket_Listen (Sock : in out Not_Null_Socket; Backlog : Natural) - -- Error : out Error_T) + -- Error : out Error_T) is begin Os_Acquire_Mutex (Net_Mutex); diff --git a/src/ada/socket_interface.ads b/src/ada/socket_interface.ads index 82fb196..6a02b12 100644 --- a/src/ada/socket_interface.ads +++ b/src/ada/socket_interface.ads @@ -58,7 +58,7 @@ is Error => (Server_Name, Flags)), Post => (if Error = NO_ERROR then - Is_Initialized_Ip(Server_Ip_Addr)); + Is_Initialized_Ip (Server_Ip_Addr)); ----------------- -- Socket_Open -- @@ -72,15 +72,15 @@ is Global => (Input => (Net_Mutex, Socket_Table), In_Out => Tcp_Dynamic_Port), - Depends => - (Sock => (S_Type, S_Protocol, Tcp_Dynamic_Port, Socket_Table), + Depends => (Sock => (S_Type, S_Protocol, Tcp_Dynamic_Port, + Socket_Table), Tcp_Dynamic_Port => (S_Type, Tcp_Dynamic_Port), null => Net_Mutex), Post => (if Sock /= null then Sock.S_Type = S_Type and then - not Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then - not Is_Initialized_Ip(Sock.S_localIpAddr)), + not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then + not Is_Initialized_Ip (Sock.S_localIpAddr)), Contract_Cases => (S_Type = SOCKET_TYPE_STREAM => (if Sock /= null then @@ -108,7 +108,7 @@ is (Sock => (Timeout, Sock), null => Net_Mutex), Post => - Model(Sock) = Model(Sock)'Old; + Model (Sock) = Model (Sock)'Old; -------------------- -- Socket_Set_Ttl -- @@ -124,7 +124,7 @@ is (Sock => (Ttl, Sock), null => Net_Mutex), Post => - Model(Sock) = Model(Sock)'Old; + Model (Sock) = Model (Sock)'Old; ------------------------------ -- Socket_Set_Multicast_Ttl -- @@ -140,7 +140,7 @@ is (Sock => (Ttl, Sock), null => Net_Mutex), Post => - Model(Sock) = Model(Sock)'Old; + Model (Sock) = Model (Sock)'Old; -------------------- -- Socket_Connect -- @@ -181,17 +181,17 @@ is Sock.S_Type = SOCKET_TYPE_DGRAM => Error = NO_ERROR and then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_Remote_Ip_Addr => Remote_Ip_Addr, S_Remote_Port => Remote_Port), Sock.S_Type = SOCKET_TYPE_RAW_IP => Error = NO_ERROR and then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_Remote_Ip_Addr => Remote_Ip_Addr), others => - Model(Sock) = Model(Sock)'Old); + Model (Sock) = Model (Sock)'Old); -------------------- -- Socket_Send_To -- @@ -215,29 +215,29 @@ is null => Net_Mutex), Pre => (if Sock.S_Type = SOCKET_TYPE_STREAM then - Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.S_Remote_Port > 0 and then (Sock.State = TCP_STATE_ESTABLISHED or else Sock.State = TCP_STATE_CLOSE_WAIT) elsif Sock.S_Type = SOCKET_TYPE_DGRAM then - Is_Initialized_Ip(Dest_Ip_Addr) and then + Is_Initialized_Ip (Dest_Ip_Addr) and then Dest_Port > 0), Post => - Basic_Model(Sock) = Basic_Model(Sock)'Old and then + Basic_Model (Sock) = Basic_Model (Sock)'Old and then (if Error = NO_ERROR then Written <= Data'Length), Contract_Cases => (Sock.S_Type = SOCKET_TYPE_STREAM => (if Error = NO_ERROR then (if Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old in TCP_STATE_SYN_RECEIVED | TCP_STATE_SYN_SENT | TCP_STATE_ESTABLISHED then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT))), others => True); @@ -260,7 +260,7 @@ is Written => (Sock, Data, Flags), null => Net_Mutex), Pre => - Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then (if Sock.S_Type = SOCKET_TYPE_STREAM then Sock.State = TCP_STATE_ESTABLISHED or else Sock.State = TCP_STATE_CLOSE_WAIT or else @@ -268,21 +268,21 @@ is Sock.State = TCP_STATE_SYN_RECEIVED or else Sock.State = TCP_STATE_CLOSED), Post => - Basic_Model(Sock) = Basic_Model(Sock)'Old and then + Basic_Model (Sock) = Basic_Model (Sock)'Old and then (if Error = NO_ERROR then Written <= Data'Length), Contract_Cases => (Sock.S_Type = SOCKET_TYPE_STREAM => (if Error = NO_ERROR then (if Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old in TCP_STATE_SYN_RECEIVED | TCP_STATE_SYN_SENT | TCP_STATE_ESTABLISHED then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT))), others => True); @@ -315,10 +315,10 @@ is Data'Last >= Data'First and then (if Sock.S_Type = SOCKET_TYPE_STREAM then Sock.State /= TCP_STATE_LISTEN and then - Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.S_Remote_Port > 0), Post => - Basic_Model(Sock) = Basic_Model(Sock)'Old, + Basic_Model (Sock) = Basic_Model (Sock)'Old, Contract_Cases => (Sock.S_Type = SOCKET_TYPE_STREAM => (if Error = NO_ERROR then @@ -326,37 +326,37 @@ is | TCP_STATE_SYN_RECEIVED | TCP_STATE_SYN_SENT then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) elsif Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old = TCP_STATE_FIN_WAIT_1 then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old in TCP_STATE_FIN_WAIT_2 | TCP_STATE_CLOSING then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_CLOSED then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old = TCP_STATE_TIME_WAIT or else Sock.State'Old = TCP_STATE_LAST_ACK then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) ) and then Received > 0 @@ -367,32 +367,32 @@ is | TCP_STATE_SYN_SENT | TCP_STATE_CLOSE_WAIT then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) elsif Sock.State'Old = TCP_STATE_CLOSING then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_TIME_WAIT then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_FIN_WAIT_2 then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_FIN_WAIT_1 then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) ) and then Received = 0 @@ -425,7 +425,7 @@ is Data'Last >= Data'First and then (if Sock.S_Type = SOCKET_TYPE_STREAM then Sock.State /= TCP_STATE_LISTEN and then - Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.S_Remote_Port > 0), Post => Basic_Model (Sock) = Basic_Model (Sock)'Old, @@ -436,37 +436,37 @@ is | TCP_STATE_SYN_RECEIVED | TCP_STATE_SYN_SENT then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) elsif Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old = TCP_STATE_FIN_WAIT_1 then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old in TCP_STATE_FIN_WAIT_2 | TCP_STATE_CLOSING then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_CLOSED then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old = TCP_STATE_TIME_WAIT or else Sock.State'Old = TCP_STATE_LAST_ACK then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) ) and then Received > 0 @@ -477,32 +477,32 @@ is | TCP_STATE_SYN_SENT | TCP_STATE_CLOSE_WAIT then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) elsif Sock.State'Old = TCP_STATE_CLOSING then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_TIME_WAIT then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_FIN_WAIT_2 then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_FIN_WAIT_1 then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) ) and then Received = 0 @@ -529,78 +529,78 @@ is null => Net_Mutex), Pre => Sock.S_Type = SOCKET_TYPE_STREAM and then - Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.State /= TCP_STATE_LISTEN, Post => (if Error = NO_ERROR then (if How = SOCKET_SD_SEND then (if Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) else (Sock.State'Old = TCP_STATE_SYN_SENT and then - Model(Sock) = Model(Sock)'Old) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old) or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED, S_Reset_Flag => True) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED))) and then (if How = SOCKET_SD_RECEIVE then - -- The connection can have been reset - Model(Sock) = (Model(Sock)'Old with delta + -- The connection can have been reset + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED, S_Reset_Flag => True) or else (if Sock.State'Old in TCP_STATE_SYN_SENT | TCP_STATE_SYN_RECEIVED | TCP_STATE_ESTABLISHED then - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) elsif Sock.State'Old = TCP_STATE_CLOSE_WAIT then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old elsif Sock.State'Old = TCP_STATE_LAST_ACK then - Model(Sock) = Model(Sock)'Old or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = Model (Sock)'Old or else + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED) elsif Sock.State'Old = TCP_STATE_CLOSED then - Model(Sock) = Model(Sock)'Old + Model (Sock) = Model (Sock)'Old else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED))) and then (if How = SOCKET_SD_BOTH then - -- The connection can have been reset - Model(Sock) = (Model(Sock)'Old with delta + -- The connection can have been reset + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED, S_Reset_Flag => True) or else - -- Special case for the function SYN_SENT + -- Special case for the function SYN_SENT (Sock.State'Old = TCP_STATE_SYN_SENT and then - (Model(Sock) = (Model(Sock)'Old with delta + (Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_ESTABLISHED) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT))) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_FIN_WAIT_2) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_TIME_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSE_WAIT) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_LAST_ACK) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSING) or else - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_CLOSED)) else Basic_Model (Sock) = Basic_Model (Sock)'Old); @@ -629,10 +629,10 @@ is with Depends => (Sock => (Size, Sock)), Pre => Sock.S_Type = SOCKET_TYPE_STREAM and then - not Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.State = TCP_STATE_CLOSED, Post => - Model(Sock) = Model(Sock)'Old; + Model (Sock) = Model (Sock)'Old; ------------------------------- -- Socket_Set_Rx_Buffer_Size -- @@ -648,7 +648,7 @@ is not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.State = TCP_STATE_CLOSED, Post => - Model(Sock) = Model(Sock)'Old; + Model (Sock) = Model (Sock)'Old; ----------------- -- Socket_Bind -- @@ -662,14 +662,14 @@ is Global => (Proof_In => IP_ADDR_ANY), Depends => (Sock => (Sock, Local_Ip_Addr, Local_Port)), Pre => - not Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then - not Is_Initialized_Ip(Sock.S_localIpAddr) and then - (Is_Initialized_Ip(Local_Ip_Addr) or else + not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then + not Is_Initialized_Ip (Sock.S_localIpAddr) and then + (Is_Initialized_Ip (Local_Ip_Addr) or else Local_Ip_Addr = IP_ADDR_ANY) and then (Sock.S_Type = SOCKET_TYPE_STREAM or else Sock.S_Type = SOCKET_TYPE_DGRAM), Post => - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_localIpAddr => Local_Ip_Addr, S_Local_Port => Local_Port); @@ -689,12 +689,12 @@ is null => Net_Mutex), Pre => Sock.S_Type = SOCKET_TYPE_STREAM and then - (Is_Initialized_Ip(Sock.S_localIpAddr) or else + (Is_Initialized_Ip (Sock.S_localIpAddr) or else Sock.S_localIpAddr = IP_ADDR_ANY) and then - not Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.State = TCP_STATE_CLOSED, Post => - Model(Sock) = (Model(Sock)'Old with delta + Model (Sock) = (Model (Sock)'Old with delta S_State => TCP_STATE_LISTEN); ------------------- @@ -719,19 +719,19 @@ is Tcp_Dynamic_Port =>+ (Sock, Socket_Table), null => Net_Mutex), Pre => Sock.S_Type = SOCKET_TYPE_STREAM and then - (Is_Initialized_Ip(Sock.S_localIpAddr) or else + (Is_Initialized_Ip (Sock.S_localIpAddr) or else Sock.S_localIpAddr = IP_ADDR_ANY) and then - not Is_Initialized_Ip(Sock.S_Remote_Ip_Addr) and then + not Is_Initialized_Ip (Sock.S_Remote_Ip_Addr) and then Sock.State = TCP_STATE_LISTEN and then Sock.S_Local_Port > 0, Post => - Model(Sock) = Model(Sock)'Old and then + Model (Sock) = Model (Sock)'Old and then (if Client_Socket /= null then Client_Port > 0 and then Is_Initialized_Ip (Client_Ip_Addr) and then Client_Socket.S_Type = SOCKET_TYPE_STREAM and then Client_Socket.S_Protocol = SOCKET_IP_PROTO_TCP and then - Is_Initialized_Ip(Client_Socket.S_localIpAddr) and then + Is_Initialized_Ip (Client_Socket.S_localIpAddr) and then Client_Socket.S_Local_Port = Sock.S_Local_Port and then Client_Socket.S_Remote_Ip_Addr = Client_Ip_Addr and then Client_Socket.S_Remote_Port = Client_Port and then diff --git a/src/ada/socket_types.ads b/src/ada/socket_types.ads index feed611..fe31227 100644 --- a/src/ada/socket_types.ads +++ b/src/ada/socket_types.ads @@ -35,7 +35,7 @@ is type Socket_Event is mod 2 ** 10 with Size => int'Size; - -- for Socket_Event'Size use unsigned'Size; + -- for Socket_Event'Size use unsigned'Size; SOCKET_EVENT_TIMEOUT : constant Socket_Event := 000; SOCKET_EVENT_CONNECTED : constant Socket_Event := 001; @@ -136,7 +136,7 @@ is S_Event_Flags : Socket_Event; S_User_Event : Os_Event_Acc; - -- TCP specific variables + -- TCP specific variables State : Tcp_State; owned_Flag : Bool; closed_Flag : Bool; @@ -182,7 +182,7 @@ is retransmitTimer : Tcp_Timer; retransmitCount : unsigned; - synQueue : Tcp_Syn_Queue_Item_Acc;-- Tcp_Syn_Queue_Item_Acc; + synQueue : Tcp_Syn_Queue_Item_Acc; -- Tcp_Syn_Queue_Item_Acc; synQueueSize : Syn_Queue_Size; wndProbeCount : unsigned; @@ -198,7 +198,7 @@ is sackBlockCount : unsigned; #if (not UDP_SUPPORT'Defined) or UDP_SUPPORT then - -- UDP specific variables + -- UDP specific variables receiveQueue : Socket_Queue_Item_Acc; #end if; end record @@ -214,9 +214,10 @@ is Socket_Struct.S_Event_Mask = SOCKET_EVENT_TX_SHUTDOWN or else Socket_Struct.S_Event_Mask = SOCKET_EVENT_RX_READY or else Socket_Struct.S_Event_Mask = SOCKET_EVENT_RX_SHUTDOWN or else - Socket_Struct.S_Event_Mask = (SOCKET_EVENT_CONNECTED or SOCKET_EVENT_CLOSED); + Socket_Struct.S_Event_Mask = (SOCKET_EVENT_CONNECTED or + SOCKET_EVENT_CLOSED); - -- @brief Flags used by I/O functions + -- @brief Flags used by I/O functions subtype Socket_Flags is unsigned; @@ -230,7 +231,7 @@ is SOCKET_FLAG_NO_DELAY : constant Socket_Flags := 16#4000#; SOCKET_FLAG_DELAY : constant Socket_Flags := 16#8000#; - -- Number of sockets that can be opened simultaneously + -- Number of sockets that can be opened simultaneously #if SOCKET_MAX_COUNT'Defined then SOCKET_MAX_COUNT : constant Positive := $SOCKET_MAX_COUNT; @@ -258,48 +259,49 @@ is ------------------------------ type Socket_Model is record - -- S_Descriptor : Sock_Descriptor; + -- S_Descriptor : Sock_Descriptor; S_Type : Socket_Type; S_Protocol : Socket_Protocol; S_localIpAddr : IpAddr; S_Local_Port : Port; S_Remote_Ip_Addr : IpAddr; S_Remote_Port : Port; - -- S_Timeout : Systime; - -- S_TTL : unsigned_char; - -- S_Multicast_TTL : unsigned_char; + -- S_Timeout : Systime; + -- S_TTL : unsigned_char; + -- S_Multicast_TTL : unsigned_char; S_State : Tcp_State; - -- S_Tx_Buffer_Size: Tx_Buffer_Size; - -- S_Rx_Buffer_Size: Rx_Buffer_Size; + -- S_Tx_Buffer_Size: Tx_Buffer_Size; + -- S_Rx_Buffer_Size: Rx_Buffer_Size; S_Reset_Flag : Bool; S_Owned_Flag : Bool; end record with Ghost; - function Model (Sock : not null access constant Socket_Struct) return Socket_Model is + function Model (Sock : not null access constant Socket_Struct) return + Socket_Model is (Socket_Model'( - -- S_Descriptor => Sock.S_Descriptor, + -- S_Descriptor => Sock.S_Descriptor, S_Type => Sock.S_Type, S_Protocol => Sock.S_Protocol, S_localIpAddr => Sock.S_localIpAddr, S_Local_Port => Sock.S_Local_Port, S_Remote_Ip_Addr => Sock.S_Remote_Ip_Addr, S_Remote_Port => Sock.S_Remote_Port, - -- S_Timeout => Sock.S_Timeout, - -- S_TTL => Sock.S_TTL, - -- S_Multicast_TTL => Sock.S_Multicast_TTL, + -- S_Timeout => Sock.S_Timeout, + -- S_TTL => Sock.S_TTL, + -- S_Multicast_TTL => Sock.S_Multicast_TTL, S_State => Sock.State, - -- S_Rx_Buffer_Size => Sock.rxBufferSize, - -- S_Tx_Buffer_Size => Sock.txBufferSize + -- S_Rx_Buffer_Size => Sock.rxBufferSize, + -- S_Tx_Buffer_Size => Sock.txBufferSize S_Reset_Flag => Sock.reset_Flag, S_Owned_Flag => Sock.owned_Flag )) with Ghost; - -- Basic Socket Model is here to model a socket after a procedure - -- call that fail et return an error. - -- It allows to model that we don't know everything about the TCP - -- state, but we still know what kind of protocol the socket is using + -- Basic Socket Model is here to model a socket after a procedure + -- call that fail et return an error. + -- It allows to model that we don't know everything about the TCP + -- state, but we still know what kind of protocol the socket is using type Basic_Socket_Model is record S_Type : Socket_Type; @@ -310,7 +312,8 @@ is S_Remote_Port : Port; end record with Ghost; - function Basic_Model(Sock : not null access constant Socket_Struct) return Basic_Socket_Model is + function Basic_Model (Sock : not null access constant Socket_Struct) return + Basic_Socket_Model is (Basic_Socket_Model'( S_Type => Sock.S_Type, S_Protocol => Sock.S_Protocol, @@ -322,28 +325,29 @@ is with Ghost; - -- The transition relation function is used to compute all the transitions - -- that can happen when a message is received. - -- This function can be used (for example) in loop invariant to compute - -- all the transition that can happen while receiving data - -- or in a loop that sends data. + -- The transition relation function is used to compute all the transitions + -- that can happen when a message is received. + -- This function can be used (for example) in loop invariant to compute + -- all the transition that can happen while receiving data + -- or in a loop that sends data. - -- This function represents only the direct transitions and the - -- transition to closed when a RST segment is received isn't - -- considered because this case must always be filtered by checking the returned - -- code of the function, and thus, may not appear in a loop invariant + -- This function represents only the direct transitions and the + -- transition to closed when a RST segment is received isn't + -- considered because this case must always be filtered by checking the + -- returned code of the function, and thus, may not appear in a loop + -- invariant function TCP_Rel (Model_Before : Socket_Model; Model_After : Socket_Model) return Boolean is - (-- Basic attributes of the socket are kept + ( -- Basic attributes of the socket are kept Model_Before.S_Type = Model_After.S_Type and then Model_Before.S_Protocol = Model_After.S_Protocol and then Model_Before.S_localIpAddr = Model_After.S_localIpAddr and then Model_Before.S_Local_Port = Model_After.S_Local_Port and then Model_Before.S_Remote_Ip_Addr = Model_After.S_Remote_Ip_Addr and then Model_Before.S_Remote_Port = Model_After.S_Remote_Port and then - -- Only the TCP State is changed + -- Only the TCP State is changed (Model_Before.S_State = Model_After.S_State or else (if Model_Before.S_State = TCP_STATE_SYN_SENT then Model_After.S_State = TCP_STATE_SYN_RECEIVED or else @@ -367,19 +371,19 @@ is )) with Ghost; - -- Transitive closure of the function TCP_Rel + -- Transitive closure of the function TCP_Rel function TCP_Rel_Iter (Model_Before : Socket_Model; Model_After : Socket_Model) return Boolean is - (-- Basic attributes of the socket are kept + ( -- Basic attributes of the socket are kept Model_After.S_Type = Model_Before.S_Type and then Model_After.S_Protocol = Model_Before.S_Protocol and then Model_After.S_localIpAddr = Model_Before.S_localIpAddr and then Model_After.S_Local_Port = Model_Before.S_Local_Port and then Model_After.S_Remote_Ip_Addr = Model_Before.S_Remote_Ip_Addr and then Model_After.S_Remote_Port = Model_Before.S_Remote_Port and then - -- Only the TCP State is changed + -- Only the TCP State is changed ( Model_After.S_State = Model_Before.S_State or else (if Model_Before.S_State = TCP_STATE_SYN_SENT then diff --git a/src/ada/tcp_fsm_binding.ads b/src/ada/tcp_fsm_binding.ads index 82b5fb8..ec2af4c 100644 --- a/src/ada/tcp_fsm_binding.ads +++ b/src/ada/tcp_fsm_binding.ads @@ -36,7 +36,7 @@ is -- This function is used to model the transitions that can happen -- when a segment is received from the network. -- This function model zero, one or more transitions that can happen when - -- a message is received. (reprent →* = ∪_{n∈ℕ} →^n, n∈ℕ) + -- a message is received. procedure Tcp_Process_Segment (Sock : in out Not_Null_Socket) with Global => null,