ada: Fix propagation of SPARK_Mode for renaming-as-body

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.

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index c8d20d020c70ac73d48734280523041d25448b96..a947018052c98b455adf1e1fcb7eaf8e8ba97c6f 100644 (file)
--- 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 0988fad97e8a6f16e3cc6ebbdeb30225ae3fbcaf..d3912ffc9d5dc38e029b9c0f6706885a3fb88b2d 100644 (file)
--- 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.