
with System;

package body Gneiss.Message with
   SPARK_Mode
is
   use type System.Address;

   function Initialized (Session : Client_Session) return Boolean is
      (Session.Connection /= System.Null_Address
       and then Session.Event /= System.Null_Address
       and then Session.Index.Valid);

   function Initialized (Session : Server_Session) return Boolean is
      (Session.Component /= System.Null_Address
       and then Session.Index.Valid);

   function Initialized (Session : Dispatcher_Session) return Boolean is
      (Session.Root /= System.Null_Address
       and then Session.Dispatch /= System.Null_Address
       and then Session.Env /= System.Null_Address
       and then Session.Index.Valid);

   function Index (Session : Client_Session) return Session_Index_Option is
      (Session.Index);

   function Index (Session : Server_Session) return Session_Index_Option is
      (Session.Index);

   function Index (Session : Dispatcher_Session) return Session_Index_Option is
      (Session.Index);

   function Registered (Session : Dispatcher_Session) return Boolean is (False);

end Gneiss.Message;
