feedc0de/wolfssl
1
0
Fork 0
forked from wolfSSL/wolfssl
Code Pull Requests Activity

Ada: fix issues in tls_server.adb detected by gnatprove

Browse Source 
Checked with:
```
gnatprove -Pdefault.gpr --level=4 -j12
```
This commit is contained in:
mgrojo
2025-03-28 19:33:42 +01:00
parent bf5009b544
commit 98eda78857
1 changed files with 5 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
wrapper/Ada/tls_server.adb
View File

@ -139,10 +139,6 @@ package body Tls_Server with SPARK_Mode is
return 0; return 0;
end if; end if;
put_line (Interfaces.C.Strings.Value
(Item => Identity,
Length => Identity_String'Length) );
Interfaces.C.Strings.Update Interfaces.C.Strings.Update
(Item => Key, (Item => Key,
Offset => 0, Offset => 0,
@ -261,13 +257,15 @@ package body Tls_Server with SPARK_Mode is
if not PSK then if not PSK then
-- Require mutual authentication. -- Require mutual authentication.
WolfSSL.Set_Verify WolfSSL.Set_Verify
(Context => Ctx, (Context => Ctx,
Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert); Mode => WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert);
-- Check verify is set correctly (GitHub #7461) -- Check verify is set correctly (GitHub #7461)
if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then if WolfSSL.Get_Verify(Context => Ctx) /= (WolfSSL.Verify_Peer or WolfSSL.Verify_Fail_If_No_Peer_Cert) then
Put ("Error: Verify does not match requested"); Put_Line ("Error: Verify does not match requested");
New_Line; SPARK_Sockets.Close_Socket (L);
WolfSSL.Free (Context => Ctx);
Set (Exit_Status_Failure);
return; return;
end if; end if;