https://gcc.gnu.org/g:ce7f7b92505e59ae517b05493694be2102cadf5a
commit r15-2687-gce7f7b92505e59ae517b05493694be2102cadf5a
Author: Yannick Moy <m...@adacore.com>
Date: Wed Jul 17 10:43:06 2024 +0200
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:
---
gcc/ada/aspects.adb | 8 +++++++-
gcc/ada/sem_ch10.adb | 12 +++++++++++-
2 files changed, 18 insertions(+), 2 deletions(-)
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b7262c56f3f1..4c8ab7b4a332 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);
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 73e5388affdc..e56fe30adaea 100644
--- 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));
