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

Address gnatprove issues in tls client

Browse Source
This commit is contained in:
Daly Brown
2024-04-08 19:40:06 -04:00
parent 97e731f27b
commit 707e60aa79
2 changed files with 11 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
wrapper/Ada/tls_client.adb
View File

@ -47,12 +47,18 @@ package body Tls_Client with SPARK_Mode is
Ada.Text_IO.Put (Text); Ada.Text_IO.Put (Text);
end Put; end Put;
procedure Put (Number : Natural) is procedure Put (Number : Natural)
with
Annotate => (GNATprove, Might_Not_Return)
is
begin begin
Natural_IO.Put (Item => Number, Width => 0, Base => 10); Natural_IO.Put (Item => Number, Width => 0, Base => 10);
end Put; end Put;
procedure Put (Number : Byte_Index) is procedure Put (Number : Byte_Index)
with
Annotate => (GNATprove, Might_Not_Return)
is
begin begin
Natural_IO.Put (Item => Natural (Number), Width => 0, Base => 10); Natural_IO.Put (Item => Natural (Number), Width => 0, Base => 10);
end Put; end Put;
@ -137,7 +143,7 @@ package body Tls_Client with SPARK_Mode is
Output : WolfSSL.Write_Result; Output : WolfSSL.Write_Result;
Result : WolfSSL.Subprogram_Result; Result : WolfSSL.Subprogram_Result;
DTLS : Boolean := False; DTLS : Boolean;
begin begin
Result := WolfSSL.Initialize; Result := WolfSSL.Initialize;
if Result /= Success then if Result /= Success then

3
wrapper/Ada/tls_client.ads
View File

@ -32,6 +32,7 @@ package Tls_Client with SPARK_Mode is
Pre => (not Client.Exists and not Pre => (not Client.Exists and not
WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)), WolfSSL.Is_Valid (Ssl) and not WolfSSL.Is_Valid (Ctx)),
Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and Post => (not Client.Exists and not WolfSSL.Is_Valid (Ssl) and
not WolfSSL.Is_Valid (Ctx)); not WolfSSL.Is_Valid (Ctx)),
Annotate => (GNATprove, Might_Not_Return);
end Tls_Client; end Tls_Client;