ada: Fix handling of SPARK_Mode on standalone child subprogram

SPARK_Mode aspect was not properly propagated to the body of
a standalone child subprogram from the generated spec for that subprogram,
leading GNATprove to not analyze this body. Now fixed.

gcc/ada/

	* aspects.adb (Find_Aspect): Take into account the case of a node
	of kind N_Defining_Program_Unit_Name.
	* sem_ch10.adb (Analyze_Compilation_Unit): Copy the SPARK aspect
	from the spec to the body. Delay semantic analysis after that
	point to ensure that SPARK_Mode is properly analyzed.

diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b7262c56f3f19c1f3addea09c4f0fd897590da89..4c8ab7b4a332b1246367f38af461c207dbedd70c 100644 (file)
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -190,13 +190,19 @@ package body Aspects is
       --  Note that not all aspects are added to the chain of representation
       --  items. In such cases, search the list of aspect specifications. First
       --  find the declaration node where the aspects reside. This is usually
-      --  the parent or the parent of the parent.
+      --  the parent or the parent of the parent, after getting through the
+      --  additional indirection of the N_Defining_Program_Unit_Name if needed.
 
       if No (Parent (Owner)) then
          return Empty;
       end if;
 
       Decl := Parent (Owner);
+
+      if Nkind (Decl) = N_Defining_Program_Unit_Name then
+         Decl := Parent (Decl);
+      end if;
+
       if not Permits_Aspect_Specifications (Decl) then
          Decl := Parent (Decl);
 

diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 73e5388affdc08f805dfd25756c35315b83299d6..e56fe30adaeae41dd8d4ea6d595a6803583d440d 100644 (file)
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -1046,17 +1046,27 @@ package body Sem_Ch10 is
                      Set_Library_Unit (N, Lib_Unit);
                      Set_Parent_Spec (Unit (Lib_Unit), Cunit (Unum));
                      Make_Child_Decl_Unit (N);
-                     Semantics (Lib_Unit);
 
                      --  Now that a separate declaration exists, the body
                      --  of the child unit does not act as spec any longer.
 
                      Set_Acts_As_Spec (N, False);
                      Move_Aspects (From => Unit_Node, To => Unit (Lib_Unit));
+
+                     --  Ensure that the generated corresponding spec and
+                     --  original body share the same SPARK_Mode pragma or
+                     --  aspect. As a result, both have the same SPARK_Mode
+                     --  attributes, and the global SPARK_Mode value is
+                     --  correctly set for local subprograms.
+
+                     Copy_SPARK_Mode_Aspect (Unit (Lib_Unit), To => Unit_Node);
+
                      Set_Is_Child_Unit (Defining_Entity (Unit_Node));
                      Set_Debug_Info_Needed (Defining_Entity (Unit (Lib_Unit)));
                      Set_Comes_From_Source_Default (SCS);
 
+                     Semantics (Lib_Unit);
+
                      --  Restore Context_Items to the body
 
                      Set_Context_Items (N, Context_Items (Lib_Unit));