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.

1 files changed, 7 insertions, 1 deletions

diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b7262c5..4c8ab7b 100644
--- 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);