Ada version of TLS v1.3 client application implemented

wrapper/Ada/ada_binding.c

@@ -24,10 +24,10 @@
 
 #include <wolfssl/ssl.h>
 
-// These functions give access to the integer values of the enumeration
+/* These functions give access to the integer values of the enumeration
-// constants used in WolfSSL. These functions make it possible
+   constants used in WolfSSL. These functions make it possible
-// for the WolfSSL implementation to change the values of the constants
+   for the WolfSSL implementation to change the values of the constants
-// without the need to make a corresponding change in the Ada code.
+   without the need to make a corresponding change in the Ada code. */
 extern int get_wolfssl_success(void);
 extern int get_wolfssl_verify_none(void);
 extern int get_wolfssl_verify_peer(void);

wrapper/Ada/c_tls_server_main.c

@@ -144,7 +144,7 @@ static void sig_handler(const int sig)
 #endif
 
 
-// To execute the application: ./main
+/* To execute the application: ./main */
 int main(int argc, char** argv)
 {
     int ret = 0;

wrapper/Ada/client.gpr

@@ -0,0 +1,69 @@
+project Client is
+   for Languages use ("C", "Ada");
+
+   for Source_Dirs use (".",
+                        "../../",
+                        "../../src",
+                        "../../wolfcrypt/src");
+
+   for Object_Dir use "obj";
+
+   for Main use ("tls_client_main.adb");
+
+   package Naming is
+      for Spec_Suffix ("C") use ".h";
+   end Naming;
+
+   package Compiler is
+      for Switches ("C") use
+         ("-DWOLFSSL_USER_SETTINGS",  --  Use the user_settings.h file.
+          "-Wno-pragmas",
+          "-Wall",
+          "-Wextra",
+          "-Wunknown-pragmas",
+          "--param=ssp-buffer-size=1",
+          "-Waddress",
+          "-Warray-bounds",
+          "-Wbad-function-cast",
+          "-Wchar-subscripts",
+          "-Wcomment",
+          "-Wfloat-equal",
+          "-Wformat-security",
+          "-Wformat=2",
+          "-Wmaybe-uninitialized",
+          "-Wmissing-field-initializers",
+          "-Wmissing-noreturn",
+          "-Wmissing-prototypes",
+          "-Wnested-externs",
+          "-Wnormalized=id",
+          "-Woverride-init",
+          "-Wpointer-arith",
+          "-Wpointer-sign",
+          "-Wshadow",
+          "-Wsign-compare",
+          "-Wstrict-overflow=1",
+          "-Wstrict-prototypes",
+          "-Wswitch-enum",
+          "-Wundef",
+          "-Wunused",
+          "-Wunused-result",
+          "-Wunused-variable",
+          "-Wwrite-strings",
+          "-fwrapv");
+
+      for Switches ("Ada") use ("-g");
+   end Compiler;
+
+   package Linker is
+      for Switches ("C") use
+         ("-lm");  --  To include the math library (used by WolfSSL).
+
+      for Switches ("Ada") use
+         ("-lm");  --  To include the math library (used by WolfSSL).
+   end Linker;
+
+   package Binder is
+      for Switches ("Ada") use ("-Es");  --  To include stack traces.
+   end Binder;
+
+end Client;

wrapper/Ada/default.gpr

@@ -22,7 +22,7 @@ project Default is
 
    package Compiler is
       for Switches ("C") use
-         ("-DWOLFSSL_USER_SETTINGS",
+         ("-DWOLFSSL_USER_SETTINGS", --  Use the user_settings.h file.
           "-Wno-pragmas",
           "-Wall",
           "-Wextra",
@@ -56,6 +56,8 @@ project Default is
           "-Wunused-variable",
           "-Wwrite-strings",
           "-fwrapv");
+
+      for Switches ("Ada") use ("-g");
    end Compiler;
 
    package Linker is
@@ -66,4 +68,8 @@ project Default is
          ("-lm");  --  To include the math library (used by WolfSSL).
    end Linker;
 
+   package Binder is
+      for Switches ("Ada") use ("-Es");  --  To include stack traces.
+   end Binder;
+
 end Default;

wrapper/Ada/tls_client.adb

@@ -1,8 +1,30 @@
+-- tls_client.adb
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 --  Ada Standard Library packages.
 with Ada.Characters.Handling;
 with Ada.Command_Line;
 with Ada.Strings.Bounded;
 with Ada.Text_IO.Bounded_IO;
+with Interfaces.C;
 
 --  GNAT Library packages.
 with GNAT.Sockets;
@@ -18,16 +40,35 @@ package body Tls_Client is
 
    use all type WolfSSL.Subprogram_Result;
 
+   subtype Byte_Type is WolfSSL.Byte_Type;
+
    package Messages is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 200);
    use all type Messages.Bounded_String;
 
+   package Integer_IO is new Ada.Text_IO.Integer_IO (Integer);
+
    package Messages_IO is new Ada.Text_IO.Bounded_IO (Messages);
 
+   procedure Put (Text : String) is
+   begin
+      Ada.Text_IO.Put (Text);
+   end Put;
+
+   procedure Put (Number : Integer) is
+   begin
+      Integer_IO.Put (Item => Number, Width => 0, Base => 10);
+   end Put;
+
    procedure Put_Line (Text : String) is
    begin
       Ada.Text_IO.Put_Line (Text);
    end Put_Line;
 
+   procedure New_Line is
+   begin
+      Ada.Text_IO.New_Line;
+   end New_Line;
+
    procedure Put_Line (Text : Messages.Bounded_String) is
    begin
       Messages_IO.Put_Line (Text);
@@ -65,17 +106,164 @@ package body Tls_Client is
 
    Any_Inet_Addr : Inet_Addr_Type renames GNAT.Sockets.Any_Inet_Addr;
 
-   CERT_FILE : constant String := "../certs/server-cert.pem";
+   CERT_FILE : constant String := "../certs/client-cert.pem";
-   KEY_FILE  : constant String := "../certs/server-key.pem";
+   KEY_FILE  : constant String := "../certs/client-key.pem";
-   CA_FILE   : constant String := "../certs/client-cert.pem";
+   CA_FILE   : constant String := "../certs/ca-cert.pem";
 
    subtype Byte_Array is WolfSSL.Byte_Array;
 
+   function Argument_Count return Natural is
+   begin
+      return Ada.Command_Line.Argument_Count;
+   end Argument_Count;
+
+   function Argument (Number : Positive) return String is
+   begin
+      return Ada.Command_Line.Argument (Number);
+   end Argument;
+
    procedure Run is
       A : Sock_Addr_Type;
       C : Socket_Type;  --  Client socket.
+      D : Byte_Array (1 .. 200);
+      P : constant Port_Type := 11111;
+
+      Ssl : WolfSSL.WolfSSL_Type;
+      Ctx : WolfSSL.Context_Type;
+
+      Bytes_Written : Integer;
+
+      Count : WolfSSL.Byte_Index;
+
+      Text : String (1 .. 200);
+      Last : Integer;
+
+      Input : WolfSSL.Read_Result;
+
+      Result : WolfSSL.Subprogram_Result;
    begin
-      null; -- work in progress.
+      if Argument_Count /= 1 then
+         Put_Line ("usage: tcl_client <IPv4 address>");
+         return;
+      end if;
+      GNAT.Sockets.Create_Socket (Socket => C);
+
+      A := (Family => Family_Inet,
+            Addr   => GNAT.Sockets.Inet_Addr (Argument (1)),
+            Port   => P);
+
+      GNAT.Sockets.Connect_Socket (Socket => C,
+                                   Server => A);
+
+      --  Create and initialize WOLFSSL_CTX.
+      WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Client_Method,
+                              Context => Ctx);
+      if not WolfSSL.Is_Valid (Ctx) then
+         Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      --  Load client certificate into WOLFSSL_CTX.
+      Result := WolfSSL.Use_Certificate_File (Context => Ctx,
+                                              File    => CERT_FILE,
+                                              Format  => WolfSSL.Format_Pem);
+      if Result = Failure then
+         Put ("ERROR: failed to load ");
+         Put (CERT_FILE);
+         Put (", please check the file.");
+         New_Line;
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      --  Load client key into WOLFSSL_CTX.
+      Result := WolfSSL.Use_Private_Key_File (Context => Ctx,
+                                              File    => KEY_FILE,
+                                              Format  => WolfSSL.Format_Pem);
+      if Result = Failure then
+         Put ("ERROR: failed to load ");
+         Put (KEY_FILE);
+         Put (", please check the file.");
+         New_Line;
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      --  Load CA certificate into WOLFSSL_CTX.
+      Result := WolfSSL.Load_Verify_Locations (Context => Ctx,
+                                               File    => CA_FILE,
+                                               Path    => "");
+      if Result = Failure then
+         Put ("ERROR: failed to load ");
+         Put (CA_FILE);
+         Put (", please check the file.");
+         New_Line;
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      --  Create a WOLFSSL object.
+      WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl);
+      if not WolfSSL.Is_Valid (Ssl) then
+         Put_Line ("ERROR: failed to create WOLFSSL object.");
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      --  Attach wolfSSL to the socket.
+      Result := WolfSSL.Attach (Ssl    => Ssl,
+                                Socket => GNAT.Sockets.To_C (C));
+      if Result = Failure then
+         Put_Line ("ERROR: Failed to set the file descriptor.");
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      Result := WolfSSL.Connect (Ssl);
+      if Result = Failure then
+         Put_Line ("ERROR: failed to connect to wolfSSL.");
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+
+      Put ("Message for server: ");
+      Ada.Text_IO.Get_Line (Text, Last);
+
+      Interfaces.C.To_C (Item       => Text (1 .. Last),
+                         Target     => D,
+                         Count      => Count,
+                         Append_Nul => False);
+      Bytes_Written := WolfSSL.Write (Ssl  => Ssl,
+                                      Data => D (1 .. Count));
+      if Bytes_Written < Last then
+         Put ("ERROR: failed to write entire message");
+         New_Line;
+         Put (Bytes_Written);
+         Put (" bytes of ");
+         Put (Last);
+         Put ("bytes were sent");
+         New_Line;
+         return;
+      end if;
+
+      Input := WolfSSL.Read (Ssl);
+      if Input.Result /= Success then
+         Put_Line ("Read error.");
+         Set (Exit_Status_Failure);
+         return;
+      end if;
+      Interfaces.C.To_Ada (Item     => Input.Buffer,
+                           Target   => Text,
+                           Count    => Last,
+                           Trim_Nul => False);
+      Put ("Server: ");
+      Put (Text (1 .. Last));
+      New_Line;
+
+      GNAT.Sockets.Close_Socket (C);
+      WolfSSL.Free (Ssl);
+      WolfSSL.Free (Context => Ctx);
    end Run;
 
 end Tls_Client;

wrapper/Ada/tls_client.ads

@@ -1,3 +1,24 @@
+-- tls_client.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 package Tls_Client is
 
    procedure Run;

wrapper/Ada/tls_client_main.adb

@@ -1,3 +1,24 @@
+-- tls_client_main.adb
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 with Tls_Client; pragma Elaborate_All (Tls_Client);
 
 --  Application entry point for the Ada translation of the

wrapper/Ada/tls_server.adb

@@ -1,3 +1,24 @@
+-- tls_server.adb
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 --  Ada Standard Library packages.
 with Ada.Characters.Handling;
 with Ada.Command_Line;
@@ -81,9 +102,9 @@ package body Tls_Server is
 
       Ch : Character;
 
-      Ssl : WolfSSL.Optional_WolfSSL;
+      Ssl : WolfSSL.WolfSSL_Type;
 
-      Ctx : WolfSSL.Optional_Context;
+      Ctx : WolfSSL.Context_Type;
       Result : WolfSSL.Subprogram_Result;
       M : Messages.Bounded_String;
       Shall_Continue : Boolean := True;
@@ -107,7 +128,7 @@ package body Tls_Server is
       --  Create and initialize WOLFSSL_CTX.
       WolfSSL.Create_Context (Method  => WolfSSL.TLSv1_3_Server_Method,
                               Context => Ctx);
-      if not Ctx.Exists then
+      if not WolfSSL.Is_Valid (Ctx) then
          Put_Line ("ERROR: failed to create WOLFSSL_CTX.");
          Set (Exit_Status_Failure);
          return;
@@ -115,11 +136,11 @@ package body Tls_Server is
 
       --  Require mutual authentication.
       WolfSSL.Set_Verify
-         (Context => Ctx.Instance,
+         (Context => Ctx,
           Mode    => WolfSSL.Verify_Peer & WolfSSL.Verify_Fail_If_No_Peer_Cert);
 
       --  Load server certificates into WOLFSSL_CTX.
-      Result := WolfSSL.Use_Certificate_File (Context => Ctx.Instance,
+      Result := WolfSSL.Use_Certificate_File (Context => Ctx,
                                               File    => CERT_FILE,
                                               Format  => WolfSSL.Format_Pem);
       if Result = Failure then
@@ -132,7 +153,7 @@ package body Tls_Server is
       end if;
 
       --  Load server key into WOLFSSL_CTX.
-      Result := WolfSSL.Use_Private_Key_File (Context => Ctx.Instance,
+      Result := WolfSSL.Use_Private_Key_File (Context => Ctx,
                                               File    => KEY_FILE,
                                               Format  => WolfSSL.Format_Pem);
       if Result = Failure then
@@ -144,10 +165,8 @@ package body Tls_Server is
          return;
       end if;
 
-      Put_Line ("success to here at least");
-
       --  Load client certificate as "trusted" into WOLFSSL_CTX.
-      Result := WolfSSL.Load_Verify_Locations (Context => Ctx.Instance,
+      Result := WolfSSL.Load_Verify_Locations (Context => Ctx,
                                                File    => CA_FILE,
                                                Path    => "");
       if Result = Failure then
@@ -172,18 +191,24 @@ package body Tls_Server is
          end;
 
          --  Create a WOLFSSL object.
-         WolfSSL.Create_WolfSSL (Context => Ctx.Instance, Ssl => Ssl);
+         WolfSSL.Create_WolfSSL (Context => Ctx, Ssl => Ssl);
-         if not Ssl.Exists then
+         if not WolfSSL.Is_Valid (Ssl) then
             Put_Line ("ERROR: failed to create WOLFSSL object.");
             Set (Exit_Status_Failure);
             return;
          end if;
 
          --  Attach wolfSSL to the socket.
-         Result := WolfSSL.Attach (Ssl    => Ssl.Instance,
+         Result := WolfSSL.Attach (Ssl    => Ssl,
                                    Socket => GNAT.Sockets.To_C (C));
+         if Result = Failure then
+            Put_Line ("ERROR: Failed to set the file descriptor.");
+            Set (Exit_Status_Failure);
+            return;
+         end if;
+
          --  Establish TLS connection.
-         Result := WolfSSL.Accept_Connection (Ssl.Instance);
+         Result := WolfSSL.Accept_Connection (Ssl);
          if Result = Failure then
             Put_Line ("Accept error.");
             Set (Exit_Status_Failure);
@@ -192,7 +217,7 @@ package body Tls_Server is
 
          Put_Line ("Client connected successfully.");
 
-         Input := WolfSSL.Read (Ssl.Instance);
+         Input := WolfSSL.Read (Ssl);
 
          if Input.Result /= Success then
             Put_Line ("Read error.");
@@ -221,12 +246,12 @@ package body Tls_Server is
             end if;
          end if;
 
-         Bytes_Written := WolfSSL.Write (Ssl.Instance, Reply);
+         Bytes_Written := WolfSSL.Write (Ssl, Reply);
          if Bytes_Written /= Reply'Length then
             Put_Line ("ERROR: failed to write.");
          end if;
 
-         Result := WolfSSL.Shutdown (Ssl.Instance);
+         Result := WolfSSL.Shutdown (Ssl);
          WolfSSL.Free (Ssl);
          GNAT.Sockets.Close_Socket (C);
 

wrapper/Ada/tls_server.ads

@@ -1,3 +1,23 @@
+-- tls_server.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
 package Tls_Server is
 
    procedure Run;

wrapper/Ada/tls_server_main.adb

@@ -1,3 +1,24 @@
+-- tls_server_main.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 with Tls_Server; pragma Elaborate_All (Tls_Server);
 
 --  Application entry point for the Ada translation of the

wrapper/Ada/wolfssl.adb

@@ -1,3 +1,24 @@
+-- wolfssl.adb
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 with Interfaces.C.Strings;
 
 package body WolfSSL is
@@ -31,6 +52,11 @@ package body WolfSSL is
       end if;
    end Finalize;
 
+   function Is_Valid (Context : Context_Type) return Boolean is
+   begin
+      return Context /= null;
+   end Is_Valid;
+
    function WolfTLSv1_2_Server_Method return Method_Type with
      Convention    => C,
      External_Name => "wolfTLSv1_2_server_method",
@@ -51,28 +77,33 @@ package body WolfSSL is
       return WolfTLSv1_3_Server_Method;
    end TLSv1_3_Server_Method;
 
+   function WolfTLSv1_3_Client_Method return Method_Type with
+     Convention    => C,
+     External_Name => "wolfTLSv1_3_client_method",
+     Import        => True;
+
+   function TLSv1_3_Client_Method return Method_Type is
+   begin
+      return WolfTLSv1_3_Client_Method;
+   end TLSv1_3_Client_Method;
+
    function WolfSSL_CTX_new (Method : Method_Type)
                              return Context_Type with
      Convention => C, External_Name => "wolfSSL_CTX_new", Import => True;
 
    procedure Create_Context (Method  : Method_Type;
-                             Context : out Optional_Context) is
+                             Context : out Context_Type) is
-      C : constant Context_Type := WolfSSL_CTX_new (Method);
    begin
-      if C = null then
+      Context := WolfSSL_CTX_new (Method);
-         Context := (Exists => False);
-      else
-         Context := (Exists => True, Instance => C);
-      end if;
    end Create_Context;
 
    procedure WolfSSL_CTX_free (Context : Context_Type) with
      Convention => C, External_Name => "wolfSSL_CTX_free", Import => True;
 
-   procedure Free (Context : in out Optional_Context) is
+   procedure Free (Context : in out Context_Type) is
    begin
-      WolfSSL_CTX_free (Context.Instance);
+      WolfSSL_CTX_free (Context);
-      Context := (Exists => False);
+      Context := null;
    end Free;
 
    type Opaque_X509_Store_Context is limited null record;
@@ -145,6 +176,7 @@ package body WolfSSL is
                                   File    : String;
                                   Format  : File_Format)
                                   return Subprogram_Result is
+      Ctx : constant Context_Type := Context;
       C : size_t;
       F : char_array (1 .. File'Length + 1);
       Result : int;
@@ -153,7 +185,7 @@ package body WolfSSL is
                          Target     => F,
                          Count      => C,
                          Append_Nul => True);
-      Result := Use_Certificate_File (Context, F (1 .. C), int (Format));
+      Result := Use_Certificate_File (Ctx, F (1 .. C), int (Format));
       if Result = WOLFSSL_SUCCESS then
          return Success;
       else
@@ -197,6 +229,7 @@ package body WolfSSL is
                                   File    : String;
                                   Format  : File_Format)
                                   return Subprogram_Result is
+      Ctx : constant Context_Type := Context;
       C : size_t;
       F : char_array (1 .. File'Length + 1);
       Result : int;
@@ -205,7 +238,7 @@ package body WolfSSL is
                          Target     => F,
                          Count      => C,
                          Append_Nul => True);
-      Result := Use_Private_Key_File (Context, F (1 .. C), int (Format));
+      Result := Use_Private_Key_File (Ctx, F (1 .. C), int (Format));
       if Result = WOLFSSL_SUCCESS then
          return Success;
       else
@@ -290,6 +323,7 @@ package body WolfSSL is
                                    File    : String;
                                    Path    : String)
                                    return Subprogram_Result is
+      Ctx : constant Context_Type := Context;
       FC : size_t;  -- File Count, specifies the characters used in F.
       F : aliased char_array := (1 .. File'Length + 1 => '#');
 
@@ -300,13 +334,13 @@ package body WolfSSL is
    begin
       if File = "" then
          if Path = "" then
-            Result := Load_Verify_Locations4 (Context, null, null);
+            Result := Load_Verify_Locations4 (Ctx, null, null);
          else
             Interfaces.C.To_C (Item       => Path,
                                Target     => P,
                                Count      => PC,
                                Append_Nul => True);
-            Result := Load_Verify_Locations3 (Context, null, P);
+            Result := Load_Verify_Locations3 (Ctx, null, P);
          end if;
       else
          Interfaces.C.To_C (Item       => File,
@@ -314,7 +348,7 @@ package body WolfSSL is
                             Count      => FC,
                             Append_Nul => True);
          if Path = "" then
-            Result := Load_Verify_Locations2 (Context, F, null);
+            Result := Load_Verify_Locations2 (Ctx, F, null);
          else
             Interfaces.C.To_C (Item       => Path,
                                Target     => P,
@@ -324,7 +358,9 @@ package body WolfSSL is
                                Target     => P,
                                Count      => PC,
                                Append_Nul => True);
-            Result := Load_Verify_Locations1 (Context, F, P);
+            Result := Load_Verify_Locations1 (Context => Ctx,
+                                              File    => F,
+                                              Path    => P);
          end if;
       end if;
       if Result = WOLFSSL_SUCCESS then
@@ -334,7 +370,7 @@ package body WolfSSL is
       end if;
    end Load_Verify_Locations;
 
-   function Load_Verify_Buffer1
+   function Load_Verify_Buffer
       (Context : Context_Type;
        Input   : char_array;
        Size    : int;
@@ -357,7 +393,7 @@ package body WolfSSL is
                                 return Subprogram_Result is
       Result : int;
    begin
-      Result := Load_Verify_Buffer1 (Context => Context,
+      Result := Load_Verify_Buffer (Context => Context,
                                      Input   => Input,
                                      Size    => Input'Length,
                                      Format  => int(Format));
@@ -368,6 +404,11 @@ package body WolfSSL is
       end if;
    end Load_Verify_Buffer;
 
+   function Is_Valid (Ssl : WolfSSL_Type) return Boolean is
+   begin
+      return Ssl /= null;
+   end Is_Valid;
+
    function WolfSSL_New (Context : Context_Type)
                          return WolfSSL_Type with
      Convention    => C,
@@ -375,17 +416,115 @@ package body WolfSSL is
      Import        => True;
 
    procedure Create_WolfSSL (Context : Context_Type;
-                             Ssl     : out Optional_WolfSSL) is
+                             Ssl     : out WolfSSL_Type) is
-      Result : WolfSSL_Type := WolfSSL_New (Context);
    begin
-      if Result /= null then
+      Ssl := WolfSSL_New (Context);
-         Ssl := (Exists   => True,
-                 Instance => Result);
-      else
-         Ssl := (Exists => False);
-      end if;
    end Create_WolfSSL;
 
+   function Use_Certificate_File (Ssl     : WolfSSL_Type;
+                                  File    : char_array;
+                                  Format  : int)
+                                  return int with
+     Convention    => C,
+     External_Name => "wolfSSL_use_certificate_file",
+     Import        => True;
+
+   function Use_Certificate_File (Ssl     : WolfSSL_Type;
+                                  File    : String;
+                                  Format  : File_Format)
+                                  return Subprogram_Result is
+      C : size_t;
+      F : char_array (1 .. File'Length + 1);
+      Result : int;
+   begin
+      Interfaces.C.To_C (Item       => File,
+                         Target     => F,
+                         Count      => C,
+                         Append_Nul => True);
+      Result := Use_Certificate_File (Ssl, F (1 .. C), int (Format));
+      if Result = WOLFSSL_SUCCESS then
+         return Success;
+      else
+         return Failure;
+      end if;
+   end Use_Certificate_File;
+
+   function Use_Certificate_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : char_array;
+                                    Size    : long;
+                                    Format  : int)
+                                    return int with
+      Convention    => C,
+      External_Name => "wolfSSL_use_certificate_buffer",
+      Import        => True;
+
+   function Use_Certificate_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : char_array;
+                                    Format  : File_Format)
+                                    return Subprogram_Result is
+      Result : int;
+   begin
+      Result := Use_Certificate_Buffer (Ssl, Input,
+                                        Input'Length, int (Format));
+      if Result = WOLFSSL_SUCCESS then
+         return Success;
+      else
+         return Failure;
+      end if;
+   end Use_Certificate_Buffer;
+
+   function Use_Private_Key_File (Ssl     : WolfSSL_Type;
+                                  File    : char_array;
+                                  Format  : int)
+                                   return int with
+      Convention    => C,
+      External_Name => "wolfSSL_use_PrivateKey_file",
+      Import        => True;
+
+   function Use_Private_Key_File (Ssl     : WolfSSL_Type;
+                                  File    : String;
+                                  Format  : File_Format)
+                                  return Subprogram_Result is
+      C : size_t;
+      F : char_array (1 .. File'Length + 1);
+      Result : int;
+   begin
+      Interfaces.C.To_C (Item       => File,
+                         Target     => F,
+                         Count      => C,
+                         Append_Nul => True);
+      Result := Use_Private_Key_File (Ssl, F (1 .. C), int (Format));
+      if Result = WOLFSSL_SUCCESS then
+         return Success;
+      else
+         return Failure;
+      end if;
+   end Use_Private_Key_File;
+
+   function Use_Private_Key_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : char_array;
+                                    Size    : long;
+                                    Format  : int)
+                                    return int with
+     Convention    => C,
+     External_Name => "wolfSSL_use_PrivateKey_buffer",
+     Import        => True;
+
+   function Use_Private_Key_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : Byte_Array;
+                                    Format  : File_Format)
+                                    return Subprogram_Result is
+      Result : int;
+   begin
+      Result := Use_Private_Key_Buffer (Ssl, Input,
+                                        Input'Length, int (Format));
+      if Result = WOLFSSL_SUCCESS then
+         return Success;
+      else
+         return Failure;
+      end if;
+   end Use_Private_Key_Buffer;
+
    function WolfSSL_Set_Fd (Ssl : WolfSSL_Type; Fd : int) return int with
      Convention    => C,
      External_Name => "wolfSSL_set_fd",
@@ -581,12 +720,12 @@ package body WolfSSL is
       External_Name => "wolfSSL_free",
       Import        => True;
 
-   procedure Free (Ssl : in out Optional_WolfSSL) is
+   procedure Free (Ssl : in out WolfSSL_Type) is
    begin
-      if Ssl.Exists then
+      if Ssl /= null then
-         WolfSSL_Free (Ssl.Instance);
+         WolfSSL_Free (Ssl);
       end if;
-      Ssl := (Exists => False);
+      Ssl := null;
    end Free;
 
    Result : constant int := Initialize_WolfSSL;

wrapper/Ada/wolfssl.ads

@@ -1,10 +1,28 @@
+-- wolfssl.ads
+--
+-- Copyright (C) 2006-2023 wolfSSL Inc.
+--
+-- This file is part of wolfSSL.
+--
+-- wolfSSL is free software; you can redistribute it and/or modify
+-- it under the terms of the GNU General Public License as published by
+-- the Free Software Foundation; either version 2 of the License, or
+-- (at your option) any later version.
+--
+-- wolfSSL is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU General Public License for more details.
+--
+-- You should have received a copy of the GNU General Public License
+-- along with this program; if not, write to the Free Software
+-- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1335, USA
+--
+
 with Interfaces.C;
 
 --  This package is annotated "with SPARK_Mode" that SPARK can verify
---  the API of this package is used correctly. The body of this package
+--  the API of this package is used correctly.
---  cannot be formally verified since it calls C functions and uses
---  access-to-object types which are not part of the SPARK subset of
---  the Ada programming language.
 package WolfSSL with SPARK_Mode is
 
    procedure Finalize;
@@ -21,6 +39,7 @@ package WolfSSL with SPARK_Mode is
 
    subtype char_array is Interfaces.C.char_array;  --  Remove?
 
+   subtype Byte_Type  is Interfaces.C.char;
    subtype Byte_Index is Interfaces.C.size_t range 0 .. 16_000;
    subtype Byte_Array is Interfaces.C.char_array;
 
@@ -28,25 +47,22 @@ package WolfSSL with SPARK_Mode is
 
    type Context_Type is limited private;
 
-   type Optional_Context (Exists : Boolean := False) is record
+   function Is_Valid (Context : Context_Type) return Boolean;
-      case Exists is
-         when True  => Instance : Context_Type;
-         when False => null;
-      end case;
-   end record;
 
    type Method_Type is limited private;
 
    function TLSv1_2_Server_Method return Method_Type;
    function TLSv1_3_Server_Method return Method_Type;
+   function TLSv1_3_Client_Method return Method_Type;
 
    procedure Create_Context (Method  : Method_Type;
-                             Context : out Optional_Context);
+                             Context : out Context_Type);
    --  Create and initialize a WolfSSL context.
+   --  If successful Is_Valid (Context) = True, otherwise False.
 
-   procedure Free (Context : in out Optional_Context) with
+   procedure Free (Context : in out Context_Type) with
-      Pre  => Context.Exists,
+      Pre  => Is_Valid (Context),
-      Post => not Context.Exists;
+      Post => not Is_Valid (Context);
 
    type Mode_Type is private;
 
@@ -67,7 +83,8 @@ package WolfSSL with SPARK_Mode is
    Verify_Default : constant Mode_Type;
 
    procedure Set_Verify (Context : Context_Type;
-                         Mode    : Mode_Type);
+                         Mode    : Mode_Type) with
+      Pre => Is_Valid (Context);
 
    type File_Format is private;
 
@@ -78,58 +95,89 @@ package WolfSSL with SPARK_Mode is
    function Use_Certificate_File (Context : Context_Type;
                                   File    : String;
                                   Format  : File_Format)
-                                  return Subprogram_Result;
+                                  return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    function Use_Certificate_Buffer (Context : Context_Type;
                                     Input   : char_array;
                                     Format  : File_Format)
-                                    return Subprogram_Result;
+                                    return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    function Use_Private_Key_File (Context : Context_Type;
                                   File    : String;
                                   Format  : File_Format)
-                                  return Subprogram_Result;
+                                  return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    function Use_Private_Key_Buffer (Context : Context_Type;
                                     Input   : Byte_Array;
                                     Format  : File_Format)
-                                    return Subprogram_Result;
+                                    return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    function Load_Verify_Locations (Context : Context_Type;
                                    File    : String;
                                    Path    : String)
-                                   return Subprogram_Result;
+                                   return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    function Load_Verify_Buffer (Context : Context_Type;
                                 Input   : Byte_Array;
                                 Format  : File_Format)
-                                return Subprogram_Result;
+                                return Subprogram_Result with
+      Pre => Is_Valid (Context);
 
    type WolfSSL_Type is limited private;
 
-   type Optional_WolfSSL (Exists : Boolean := False) is record
+   function Is_Valid (Ssl : WolfSSL_Type) return Boolean;
-      case Exists is
-         when True  => Instance : WolfSSL_Type;
-         when False => null;
-      end case;
-   end record;
 
    procedure Create_WolfSSL (Context : Context_Type;
-                             Ssl     : out Optional_WolfSSL);
+                             Ssl     : out WolfSSL_Type) with
+      Pre => Is_Valid (Context);
+
+
+   function Use_Certificate_File (Ssl     : WolfSSL_Type;
+                                  File    : String;
+                                  Format  : File_Format)
+                                  return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
+
+   function Use_Certificate_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : char_array;
+                                    Format  : File_Format)
+                                    return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
+
+   function Use_Private_Key_File (Ssl     : WolfSSL_Type;
+                                  File    : String;
+                                  Format  : File_Format)
+                                  return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
+
+   function Use_Private_Key_Buffer (Ssl     : WolfSSL_Type;
+                                    Input   : Byte_Array;
+                                    Format  : File_Format)
+                                    return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
 
    --  Attach wolfSSL to the socket.
    function Attach (Ssl    : WolfSSL_Type;
                     Socket : Integer)
-                    return Subprogram_Result;
+                    return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
 
-   procedure Keep_Arrays (Ssl : WolfSSL_Type);
+   procedure Keep_Arrays (Ssl : WolfSSL_Type) with
+      Pre => Is_Valid (Ssl);
    --  Don't free temporary arrays at end of handshake.
 
-   procedure Free_Arrays (Ssl : WolfSSL_Type);
+   procedure Free_Arrays (Ssl : WolfSSL_Type) with
+      Pre => Is_Valid (Ssl);
    --  User doesn't need temporary arrays anymore, Free.
 
    function Accept_Connection (Ssl : WolfSSL_Type)
-                               return Subprogram_Result;
+                               return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
 
    --  This record type has discriminants with default values to be able
    --  to compile this code under the restriction no secondary stack.
@@ -141,18 +189,23 @@ package WolfSSL with SPARK_Mode is
       end case;
    end record;
 
-   function Read (Ssl : WolfSSL_Type) return Read_Result;
+   function Read (Ssl : WolfSSL_Type) return Read_Result with
+      Pre => Is_Valid (Ssl);
 
    --  The number of bytes written is returned.
-   function Write (Ssl  : WolfSSL_Type; Data : Byte_Array) return Integer;
+   function Write (Ssl  : WolfSSL_Type;
+                   Data : Byte_Array) return Integer with
+      Pre => Is_Valid (Ssl);
 
-   function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result;
+   function Shutdown (Ssl : WolfSSL_Type) return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
 
-   procedure Free (Ssl : in out Optional_WolfSSL) with
+   procedure Free (Ssl : in out WolfSSL_Type) with
-      Pre  => Ssl.Exists,
+      Pre  => Is_Valid (Ssl),
-      Post => not Ssl.Exists;
+      Post => not Is_Valid (Ssl);
 
-   function Connect (Ssl : WolfSSL_Type) return Subprogram_Result;
+   function Connect (Ssl : WolfSSL_Type) return Subprogram_Result with
+      Pre => Is_Valid (Ssl);
 
 private
    pragma SPARK_Mode (Off);