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 /libcpp | |
| 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.
Diffstat (limited to 'libcpp')
0 files changed, 0 insertions, 0 deletions