diff options
| author | Yannick Moy <moy@adacore.com> | 2024-07-22 11:31:03 +0200 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-08-06 10:54:30 +0200 |
| commit | 439af1ef21d0d96b1f48d86e8c978e9af81490bc (patch) | |
| tree | 0873601f69171ed27e90bc43494e1ffa01e9f3f3 | |
| parent | 070f973cd3b99ed57cd40582fa90eb08dc5f84c4 (diff) | |
| download | gcc-439af1ef21d0d96b1f48d86e8c978e9af81490bc.zip gcc-439af1ef21d0d96b1f48d86e8c978e9af81490bc.tar.gz gcc-439af1ef21d0d96b1f48d86e8c978e9af81490bc.tar.bz2 | |
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.
| -rw-r--r-- | gcc/ada/freeze.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 9 |
2 files changed, 16 insertions, 0 deletions
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index c8d20d0..a947018 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 0988fad..d3912ff 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. |