diff options
| author | Yannick Moy <moy@adacore.com> | 2024-07-17 10:43:06 +0200 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-08-02 09:08:11 +0200 |
| commit | ce7f7b92505e59ae517b05493694be2102cadf5a (patch) | |
| tree | 83c227cc8bf4fbdae69f62664227e4d0e1bacecd /gcc/c | |
| parent | d8a27bb9a7d932b3a3f8b1ffc9e156f698d08aee (diff) | |
| download | gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.zip gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.tar.gz gcc-ce7f7b92505e59ae517b05493694be2102cadf5a.tar.bz2 | |
ada: Fix handling of SPARK_Mode on standalone child subprogram
SPARK_Mode aspect was not properly propagated to the body of
a standalone child subprogram from the generated spec for that subprogram,
leading GNATprove to not analyze this body. Now fixed.
gcc/ada/
* aspects.adb (Find_Aspect): Take into account the case of a node
of kind N_Defining_Program_Unit_Name.
* sem_ch10.adb (Analyze_Compilation_Unit): Copy the SPARK aspect
from the spec to the body. Delay semantic analysis after that
point to ensure that SPARK_Mode is properly analyzed.
Diffstat (limited to 'gcc/c')
0 files changed, 0 insertions, 0 deletions