Fix initialization of SPDM responder

Ref. eng/recordflux/RecordFlux!1663

examples/apps/spdm_responder/src/lib/responder.adb

@@ -1,4 +1,5 @@
 with RFLX.SPDM_Responder.Session.FSM;
+with RFLX.SPDM_Responder.Session_Environment;
 with RFLX.RFLX_Types;
 with RFLX.RFLX_Types.Operators;
 
@@ -9,8 +10,11 @@ is
    use RFLX.RFLX_Types;
    use RFLX.RFLX_Types.Operators;
 
+   package SR renames RFLX.SPDM_Responder.Session.FSM;
+   package Session_Environment renames RFLX.SPDM_Responder.Session_Environment;
+
    Buffer : Bytes (Index'First .. Index'First + 1279) := (others => 0);
-   Context : RFLX.SPDM_Responder.Session.FSM.Context;
+   Context : SR.Context;
 
    function Uninitialized return Boolean is (RFLX.SPDM_Responder.Session.FSM.Uninitialized (Context));
 
@@ -29,13 +33,11 @@ is
 
    procedure Responder_Main
    is
-      package SR renames RFLX.SPDM_Responder.Session.FSM;
    begin
       loop
-         --  Eng/RecordFlux/RecordFlux#1032
-         --  Context.Plat_Initialize;
          pragma Loop_Invariant (SR.Uninitialized (Context));
 
+         Session_Environment.Plat_Initialize (Context.E);
          SR.Initialize (Context);
 
          while SR.Active (Context) loop
@@ -70,5 +72,6 @@ is
          SR.Finalize (Context);
       end loop;
    end Responder_Main;
-
+begin
+   Session_Environment.Plat_Initialize (Context.E);
 end Responder;

examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session.adb

@@ -18,28 +18,6 @@ with RFLX.SPDM_Responder.Session_Environment;
 package body RFLX.SPDM_Responder.Session with
    SPARK_Mode
 is
-
-   --  Ensure initialization of State.Instance.
-   --
-   --  This procedure is both implemented and called by the platform code. It is
-   --  called before the start of the state machine and ensures that
-   --  RFLX.SPDM_Responder.Session_Environment.State.Instance is initialized. It
-   --  is not necessary for the state machine to function. If the platform code
-   --  has other means of initializing the
-   --  RFLX.SPDM_Responder.Session_Environment.State this procedure can be
-   --  removed.
-   --
-   --  @param State RFLX.SPDM_Responder.Session_Environment.State.
-   procedure Plat_Initialize (State : in out RFLX.SPDM_Responder.Session_Environment.State)
-   is
-      procedure C_Interface (Instance : out System.Address) with
-         Import,
-         Convention => C,
-         External_Name => "spdm_platform_initialize";
-   begin
-      C_Interface (State.Instance);
-   end Plat_Initialize;
-
    --  Return CT exponent (DSP0274_1.1.0 [178]).
    --
    --  @param State RFLX.SPDM_Responder.Session_Environment.State.

examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.adb

@@ -0,0 +1,16 @@
+package body RFLX.SPDM_Responder.Session_Environment with
+   SPARK_Mode
+is
+
+   procedure Plat_Initialize (State : out Session_Environment.State) with
+      SPARK_Mode => Off
+   is
+      procedure C_Interface (Instance : out System.Address) with
+         Import,
+         Convention => C,
+         External_Name => "spdm_platform_initialize";
+   begin
+      C_Interface (State.Instance);
+   end Plat_Initialize;
+
+end RFLX.SPDM_Responder.Session_Environment;

examples/apps/spdm_responder/src/lib/rflx-spdm_responder-session_environment.ads

@@ -12,7 +12,18 @@ is
    --  implementer.
    type State is
       record
-         Instance : System.Address := System.Null_Address;
+         Instance : System.Address;
       end record;
 
+   --  Initialize State.
+   --
+   --  This procedure is implemented by the platform code. It must be called
+   --  before the start of the state machine to ensure that State.Instance is
+   --  initialized. If all components of State are initialized by default, this
+   --  procedure can be removed.
+   --
+   --  @param State Session_Environment.State.
+   procedure Plat_Initialize (State : out Session_Environment.State) with
+      Always_Terminates;
+
 end RFLX.SPDM_Responder.Session_Environment;