* Completed support for SPARK2014 features, as supported by

          SPARK GPL 2015

src/backends/ocarina-backends-po_hi_ada-activity.adb

@@ -614,7 +614,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
          N :=
            Make_Package_Instantiation
              (Defining_Identifier => Map_Task_Identifier (E),
-              Generic_Package     => RU (RU_PolyORB_HI_Periodic_Task),
+              Generic_Package     =>
+                RU (RU_PolyORB_HI_Periodic_Task, Elaborated => True),
               Parameter_List      => Parameter_List);
          return N;
       end Periodic_Task_Instantiation;
@@ -674,7 +675,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
          N :=
            Make_Package_Instantiation
              (Defining_Identifier => Map_Task_Identifier (E),
-              Generic_Package     => RU (RU_PolyORB_HI_Sporadic_Task),
+              Generic_Package     =>
+                RU (RU_PolyORB_HI_Sporadic_Task, Elaborated => True),
               Parameter_List      => Parameter_List);
          return N;
       end Sporadic_Task_Instantiation;
@@ -733,7 +735,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
          N :=
            Make_Package_Instantiation
              (Defining_Identifier => Map_Task_Identifier (E),
-              Generic_Package     => RU (RU_PolyORB_HI_Aperiodic_Task),
+              Generic_Package     =>
+                RU (RU_PolyORB_HI_Aperiodic_Task, Elaborated => True),
               Parameter_List      => Parameter_List);
          return N;
       end Aperiodic_Task_Instantiation;
@@ -755,7 +758,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
          N :=
            Make_Package_Instantiation
              (Defining_Identifier => Map_Task_Identifier (E),
-              Generic_Package     => RU (RU_PolyORB_HI_Background_Task),
+              Generic_Package     =>
+                RU (RU_PolyORB_HI_Background_Task, Elaborated => True),
               Parameter_List      => Parameter_List);
          return N;
       end Background_Task_Instantiation;
@@ -798,10 +802,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
                Fatal => True);
          end if;
 
-         N := Make_Withed_Package (RU (RU_Ada_Interrupts_Names));
-         Append_Node_To_List (N, ADN.Withed_Packages (Current_Package));
-         N := Make_Used_Package (RU (RU_Ada_Interrupts_Names));
-         Append_Node_To_List (N, ADN.Visible_Part (Current_Package));
+         Add_With_Package (RU (RU_Ada_Interrupts_Names));
+         Add_With_Package (RU (RU_Ada_Interrupts_Names));
 
          N :=
            Make_Parameter_Association
@@ -1097,6 +1099,21 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
                   --  Link the variable and the object
 
                   Bind_AADL_To_Object (Identifier (S), N);
+
+                  if Get_Concurrency_Protocol (Corresponding_Instance (S))
+                    = Priority_Ceiling
+                  then
+                     --  XXX For now, we disable SPARK_Mode due to the
+                     --  inability of SPARK GPL2015 to support
+                     --  variable that denotes protected objects.
+
+                     N := Make_Pragma_Statement
+                       (Pragma_SPARK_Mode, Make_List_Id (RE (RE_Off)));
+
+                     Append_Node_To_List
+                       (N, ADN.Package_Headers (Current_Package));
+                  end if;
+
                else
                   --  Visit the component instance corresponding to the
                   --  subcomponent S.
@@ -3795,6 +3812,19 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
                    (ADN.Marshall_Node (Backend_Node (Identifier (E)))));
             Append_Node_To_List (N, Inst_Profile);
 
+            --  The 'Send' generic formal
+
+            N :=
+              Make_Parameter_Association
+                (Make_Defining_Identifier (SN (S_Send)),
+                 Extract_Designator
+                   (ADN.Send_Node
+                      (Backend_Node (Identifier
+                                       (Corresponding_Instance
+                                          (Get_Container_Process
+                                             (Parent_Subcomponent (E))))))));
+            Append_Node_To_List (N, Inst_Profile);
+
             --  The 'Next_Deadline' genertic formal
 
             N :=
@@ -3805,26 +3835,12 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
                     Make_Defining_Identifier (SN (S_Next_Deadline))));
             Append_Node_To_List (N, Inst_Profile);
 
-            --  We do not want a pragma Elaborate_All to be
-            --  implicitely generated for
-            --  PolyORB_HI.Thread_Interrogators because we know there
-            --  is no elaboration problem betweeb Activity and
-            --  Thread_Interrogators and also to avoid cyclic
-            --  elaboration dependency to be introduced.
-
-            N :=
-              Make_Pragma_Statement
-                (Pragma_Suppress,
-                 Make_List_Id
-                   (Make_Defining_Identifier (PN (P_Elaboration_Check)),
-                    RU (RU_PolyORB_HI_Thread_Interrogators)));
-            Append_Node_To_List (N, ADN.Statements (Current_Package));
-
             N :=
               Make_Package_Instantiation
                 (Defining_Identifier =>
                    Make_Defining_Identifier (Map_Interrogators_Name (E)),
-                 Generic_Package => RU (RU_PolyORB_HI_Thread_Interrogators),
+                 Generic_Package =>
+                   RU (RU_PolyORB_HI_Thread_Interrogators, Elaborated => True),
                  Parameter_List  => Inst_Profile);
 
             Append_Node_To_List (N, ADN.Statements (Current_Package));
@@ -4312,6 +4328,24 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
          if not AINU.Is_Empty (Subcomponents (E)) then
             S := First_Node (Subcomponents (E));
             while Present (S) loop
+               --  If the process has a data subcomponent, then map a
+               --  shared variable.
+
+               if AINU.Is_Data (Corresponding_Instance (S))
+                 and then Get_Concurrency_Protocol (Corresponding_Instance (S))
+                 = Priority_Ceiling
+               then
+                  --  XXX For now, we disable SPARK_Mode due to the
+                  --  inability of SPARK GPL2015 to support
+                  --  variable that denotes protected objects.
+
+                  N := Make_Pragma_Statement
+                    (Pragma_SPARK_Mode, Make_List_Id (RE (RE_Off)));
+
+                  Append_Node_To_List
+                    (N, ADN.Package_Headers (Current_Package));
+               end if;
+
                --  Visit the component instance corresponding to the
                --  subcomponent S.
 

src/backends/ocarina-backends-po_hi_ada-marshallers.adb

@@ -884,16 +884,13 @@ package body Ocarina.Backends.PO_HI_Ada.Marshallers is
       -------------------------------
 
       function Marshallers_Instantiation (E : Node_Id) return Node_Id is
-         N : Node_Id;
       begin
-         N :=
-           Make_Package_Instantiation
-             (Defining_Identifier =>
-                Make_Defining_Identifier (Map_Marshallers_Name (E)),
-              Generic_Package => RU (RU_PolyORB_HI_Marshallers_G),
-              Parameter_List  => Make_List_Id (Get_Marshalled_Type (E)));
-
-         return N;
+         return Make_Package_Instantiation
+           (Defining_Identifier =>
+              Make_Defining_Identifier (Map_Marshallers_Name (E)),
+            Generic_Package =>
+              RU (RU_PolyORB_HI_Marshallers_G, Elaborated => True),
+            Parameter_List  => Make_List_Id (Get_Marshalled_Type (E)));
       end Marshallers_Instantiation;
 
       -----------