Address gnatprove warnings and errors

This commit is contained in:
Daly Brown
2024-04-05 12:09:11 -04:00
parent 42f7be20c8
commit 97e731f27b

View File

@ -105,7 +105,7 @@ package body Tls_Server with SPARK_Mode is
Ch : Character; Ch : Character;
Result : WolfSSL.Subprogram_Result; Result : WolfSSL.Subprogram_Result;
DTLS : Boolean := False; DTLS : Boolean;
Shall_Continue : Boolean := True; Shall_Continue : Boolean := True;
Input : WolfSSL.Read_Result; Input : WolfSSL.Read_Result;
@ -271,7 +271,11 @@ package body Tls_Server with SPARK_Mode is
if not WolfSSL.Is_Valid (Ssl) then if not WolfSSL.Is_Valid (Ssl) then
Put_Line ("ERROR: failed to create WOLFSSL object."); Put_Line ("ERROR: failed to create WOLFSSL object.");
SPARK_Sockets.Close_Socket (L); SPARK_Sockets.Close_Socket (L);
SPARK_Sockets.Close_Socket (C);
if not DTLS then
SPARK_Sockets.Close_Socket (C);
end if;
WolfSSL.Free (Context => Ctx); WolfSSL.Free (Context => Ctx);
Set (Exit_Status_Failure); Set (Exit_Status_Failure);
return; return;
@ -285,7 +289,11 @@ package body Tls_Server with SPARK_Mode is
Put_Line ("ERROR: Failed to set the file descriptor."); Put_Line ("ERROR: Failed to set the file descriptor.");
WolfSSL.Free (Ssl); WolfSSL.Free (Ssl);
SPARK_Sockets.Close_Socket (L); SPARK_Sockets.Close_Socket (L);
SPARK_Sockets.Close_Socket (C);
if not DTLS then
SPARK_Sockets.Close_Socket (C);
end if;
WolfSSL.Free (Context => Ctx); WolfSSL.Free (Context => Ctx);
Set (Exit_Status_Failure); Set (Exit_Status_Failure);
return; return;
@ -297,7 +305,11 @@ package body Tls_Server with SPARK_Mode is
Put_Line ("Accept error."); Put_Line ("Accept error.");
WolfSSL.Free (Ssl); WolfSSL.Free (Ssl);
SPARK_Sockets.Close_Socket (L); SPARK_Sockets.Close_Socket (L);
SPARK_Sockets.Close_Socket (C);
if not DTLS then
SPARK_Sockets.Close_Socket (C);
end if;
WolfSSL.Free (Context => Ctx); WolfSSL.Free (Context => Ctx);
Set (Exit_Status_Failure); Set (Exit_Status_Failure);
return; return;
@ -310,7 +322,11 @@ package body Tls_Server with SPARK_Mode is
Put_Line ("Read error."); Put_Line ("Read error.");
WolfSSL.Free (Ssl); WolfSSL.Free (Ssl);
SPARK_Sockets.Close_Socket (L); SPARK_Sockets.Close_Socket (L);
SPARK_Sockets.Close_Socket (C);
if not DTLS then
SPARK_Sockets.Close_Socket (C);
end if;
WolfSSL.Free (Context => Ctx); WolfSSL.Free (Context => Ctx);
Set (Exit_Status_Failure); Set (Exit_Status_Failure);
return; return;