diff options
| author | Yannick Moy <moy@adacore.com> | 2024-07-17 10:43:06 +0200 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-08-02 09:08:11 +0200 |
| commit | ce7f7b92505e59ae517b05493694be2102cadf5a (patch) | |
| tree | 83c227cc8bf4fbdae69f62664227e4d0e1bacecd /gcc | |
| parent | d8a27bb9a7d932b3a3f8b1ffc9e156f698d08aee (diff) | |
| download | gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.zip gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.tar.gz gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.tar.bz2 | |
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/aspects.adb | 8 | ||||
| -rw-r--r-- | 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 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); diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 73e5388..e56fe30 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)); |