Fix some failing VCs reported by gnatprove

Author: mgrojo

client/src/coap_client.adb

@@ -71,8 +71,8 @@ procedure CoAP_Client is
       Global =>
          (Input  => CoAP_SPARK.Log.Active_Level,
           In_Out => (Ada.Text_IO.File_System, CoAP_SPARK.Random.Generator))
-
    is
+
       URI        : constant CoAP_SPARK.URI.URI :=
         CoAP_SPARK.URI.Create (URI_String);
       Ctx        : FSM.Context;
@@ -81,6 +81,18 @@ procedure CoAP_Client is
           (Is_Secure =>
              CoAP_SPARK.URI.Scheme (URI) = CoAP_SPARK.Secure_Scheme);
       Valid_URI : Boolean := True;
+
+      procedure Finalize is
+      begin
+         RFLX.RFLX_Types.Free (Payload);
+         if FSM.Initialized (Ctx) then
+            FSM.Finalize (Ctx);
+         end if;
+         pragma Assert (FSM.Uninitialized (Ctx));
+         Session_Environment.Finalize (Ctx.E);
+         pragma Assert (Session_Environment.Is_Finalized (Ctx.E));
+      end Finalize;
+
    begin
 
       if URI_String = "" or else URI_String (URI_String'First) = '-' then
@@ -114,14 +126,6 @@ procedure CoAP_Client is
       CoAP_SPARK.Log.Put ("Query: ");
       CoAP_SPARK.Log.Put_Line (CoAP_SPARK.URI.Query (URI));
 
-      CoAP_Secure.Initialize (Socket => Skt);
-      if not CoAP_SPARK.Channel.Is_Valid (Skt) then
-         CoAP_SPARK.Log.Put_Line
-           ("Communication problems.", CoAP_SPARK.Log.Error);
-         RFLX.RFLX_Types.Free (Payload);
-         return;
-      end if;
-
       Session_Environment.Initialize
         (Method        => Method,
          Server        => CoAP_SPARK.URI.Host (URI),
@@ -134,27 +138,30 @@ procedure CoAP_Client is
       if Ctx.E.Current_Status /= CoAP_SPARK.OK then
          CoAP_SPARK.Log.Put_Line
            (Ctx.E.Current_Status'Image, CoAP_SPARK.Log.Error);
-         RFLX.RFLX_Types.Free (Payload);
-         Session_Environment.Finalize (Ctx.E);
-         pragma Assert (Session_Environment.Is_Finalized (Ctx.E));
+         Finalize;
          return;
       end if;
       pragma Assert (FSM.Uninitialized (Ctx));
 
       FSM.Initialize (Ctx);
+
+      CoAP_Secure.Initialize (Socket => Skt);
+      if not CoAP_SPARK.Channel.Is_Ready (Skt) then
+         CoAP_SPARK.Log.Put_Line
+           ("Could not initialize socket.", CoAP_SPARK.Log.Error);
+         Finalize;
+         return;
+      end if;
+
       Channel.Connect
         (Socket => Skt,
          Server => CoAP_SPARK.URI.Host (URI),
          Port   => CoAP_SPARK.Channel.Port_Type (CoAP_SPARK.URI.Port (URI)));
 
-      if not CoAP_SPARK.Channel.Is_Valid (Skt) then
+      if not CoAP_SPARK.Channel.Is_Ready (Skt) then
          CoAP_SPARK.Log.Put_Line
            ("Connection problems.", CoAP_SPARK.Log.Error);
-         RFLX.RFLX_Types.Free (Payload);
-         FSM.Finalize (Ctx);
-         pragma Assert (FSM.Uninitialized (Ctx));
-         Session_Environment.Finalize (Ctx.E);
-         pragma Assert (Session_Environment.Is_Finalized (Ctx.E));
+         Finalize;
          return;
       end if;
 
@@ -208,11 +215,7 @@ procedure CoAP_Client is
          SPARK_Terminal.Set_Exit_Status (SPARK_Terminal.Exit_Status_Failure);
       end if;
 
-      FSM.Finalize (Ctx);
-      pragma Assert (FSM.Uninitialized (Ctx));
-
-      Session_Environment.Finalize (Ctx.E);
-      pragma Assert (Session_Environment.Is_Finalized (Ctx.E));
+      Finalize;
    end Run_Session;
 
    Method : RFLX.CoAP.Method_Code := RFLX.CoAP.Get;

src/coap_spark-channel.adb

@@ -354,27 +354,27 @@ is
    end Receive_Socket;
 
    procedure Receive_Socket
-     (Socket : Socket_Type;
+     (Socket : SPARK_Sockets.Optional_Socket;
       Item   : out Ada.Streams.Stream_Element_Array;
       Last   : out Ada.Streams.Stream_Element_Offset;
       From   : out Address_Type)
    with
      Relaxed_Initialization => Item,
-     Pre                    => Is_Valid (Socket),
+     Pre                    => Socket.Exists,
      Post                   =>
        Last in Item'First - 1 .. Item'Last
        and then Item (Item'First .. Last)'Initialized;
 
    procedure Receive_Socket
-     (Socket : Socket_Type;
+     (Socket : SPARK_Sockets.Optional_Socket;
       Item   : out Ada.Streams.Stream_Element_Array;
       Last   : out Ada.Streams.Stream_Element_Offset;
       From   : out Address_Type)
    with SPARK_Mode => Off
    is
    begin
       GNAT.Sockets.Receive_Socket
-        (Socket => Socket.Attached_Socket.Socket,
+        (Socket => Socket.Socket,
          Item   => Item,
          Last   => Last,
          From   => GNAT.Sockets.Sock_Addr_Type (From.Sock_Addr));
@@ -412,7 +412,7 @@ is
 
             if Socket.Is_Server then
                Receive_Socket
-                 (Socket => Socket,
+                 (Socket => Socket.Attached_Socket,
                   Item   => Data,
                   Last   => Last,
                   From   => Socket.Client_Address);
@@ -445,6 +445,11 @@ is
                   Socket =>
                      SPARK_Sockets.To_C (Socket.Attached_Socket.Socket));
 
+         if Socket.Result /= SPARK_Sockets.Success then
+            Finalize (Socket);
+            return;
+         end if;
+
          Socket.Result := WolfSSL.Accept_Connection (Socket.Ssl);
          if Socket.Result /= WolfSSL.Success then
             declare

src/coap_spark-client_session.adb

@@ -17,7 +17,7 @@ is
       Pre =>
          FSM.Initialized (Ctx)
          and then FSM.Has_Data (Ctx, FSM.C_Transport)
-         and then CoAP_SPARK.Channel.Is_Valid (Skt),
+         and then CoAP_SPARK.Channel.Is_Ready (Skt),
       Post =>
          FSM.Initialized (Ctx)
    is
@@ -49,7 +49,7 @@ is
       Pre =>
          FSM.Initialized (Ctx)
          and then FSM.Needs_Data (Ctx, FSM.C_Transport)
-         and then CoAP_SPARK.Channel.Is_Valid (Skt),
+         and then CoAP_SPARK.Channel.Is_Ready (Skt),
       Post =>
          FSM.Initialized (Ctx)
       is

src/coap_spark-client_session.ads

@@ -13,7 +13,7 @@ is
    with
       Pre =>
         FSM.Initialized (Ctx)
-        and then CoAP_SPARK.Channel.Is_Valid (Skt),
+        and then CoAP_SPARK.Channel.Is_Ready (Skt),
       Post => FSM.Initialized (Ctx);
 
 end CoAP_SPARK.Client_Session;