diff mbox series

[COMMITTED,2/9] ada: Fix propagation of SPARK_Mode for renaming-as-body

Message ID 20240806090241.576862-2-poulhies@adacore.com
State Committed
Commit 439af1ef21d0d96b1f48d86e8c978e9af81490bc
Headers
Series [COMMITTED,1/9] ada: Reject use-clause conflicts in the run-time library |

Commit Message

Marc Poulhiès Aug. 6, 2024, 9:02 a.m. UTC 
  From: Yannick Moy <moy@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 mbox series

Patch

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.