diff mbox series

[COMMITTED,26/26] ada: Fix handling of SPARK_Mode on standalone child subprogram

Message ID 20240802071210.413366-26-poulhies@adacore.com
State New
Headers show
Series [COMMITTED,01/26] ada: Fix detection of suspicious loop patterns | expand

Commit Message

Marc Poulhiès Aug. 2, 2024, 7:11 a.m. UTC 
From: Yannick Moy <moy@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/aspects.adb  |  8 +++++++-
 gcc/ada/sem_ch10.adb | 12 +++++++++++-
 2 files changed, 18 insertions(+), 2 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b7262c56f3f..4c8ab7b4a33 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 73e5388affd..e56fe30adae 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));