From: Yannick Moy <m...@adacore.com>
The value of SPARK_Mode associated with a renaming-as-body might
not be the correct one, when the private part of the package containing
the declaration has SPARK_Mode Off while the public part has SPARK_Mode
On. This may lead to analysis of code by GNATprove that should not be
analyzed.
gcc/ada/
* freeze.adb (Build_Renamed_Body): Propagate SPARK_Pragma to body
build from renaming, so that locally relevant value is taken into
account.
* sem_ch6.adb (Analyze_Expression_Function): Propagate
SPARK_Pragma to body built from expression function, so that
locally relevant value is taken into account.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/freeze.adb | 7 +++++++
gcc/ada/sem_ch6.adb | 9 +++++++++
2 files changed, 16 insertions(+)
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index c8d20d020c7..a947018052c 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -586,6 +586,13 @@ package body Freeze is
Next (Param_Spec);
end loop;
+ -- Copy SPARK pragma from renaming declaration
+
+ Set_SPARK_Pragma
+ (Defining_Unit_Name (Spec), SPARK_Pragma (New_S));
+ Set_SPARK_Pragma_Inherited
+ (Defining_Unit_Name (Spec), SPARK_Pragma_Inherited (New_S));
+
-- In GNATprove, prefer to generate an expression function whenever
-- possible, to benefit from the more precise analysis in that case
-- (as if an implicit postcondition had been generated).
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 0988fad97e8..d3912ffc9d5 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -333,6 +333,15 @@ package body Sem_Ch6 is
New_Spec := Copy_Subprogram_Spec (Spec);
Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
+ -- Copy SPARK pragma from expression function
+
+ Set_SPARK_Pragma
+ (Defining_Unit_Name (New_Spec),
+ SPARK_Pragma (Defining_Unit_Name (Spec)));
+ Set_SPARK_Pragma_Inherited
+ (Defining_Unit_Name (New_Spec),
+ SPARK_Pragma_Inherited (Defining_Unit_Name (Spec)));
+
-- If there are previous overloadable entities with the same name,
-- check whether any of them is completed by the expression function.
-- In a generic context a formal subprogram has no completion.
--
2.45.2
