diff options
| author | Yannick Moy <moy@adacore.com> | 2023-11-21 12:06:52 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-12-19 15:27:48 +0100 |
| commit | 1acce1417b42aee9152fc42bb0247ced2acc3a4f (patch) | |
| tree | 27698eafa56a0bddb76fd43662661afc20fd6449 /gcc/ada/gen_il-fields.ads | |
| parent | da5dca1d36d5a70b3068825f74612000973a819e (diff) | |
| download | gcc-1acce1417b42aee9152fc42bb0247ced2acc3a4f.zip gcc-1acce1417b42aee9152fc42bb0247ced2acc3a4f.tar.gz gcc-1acce1417b42aee9152fc42bb0247ced2acc3a4f.tar.bz2 | |
ada: Do not issue SPARK legality error if SPARK_Mode ignored
When pragma Ignore_Pragma(SPARK_Mode) is used, do not issue error
messages related to SPARK legality checking. This facilitates the
instrumentation of code by GNATcoverage.
gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst: Fix doc for
pragma Ignore_Pragma, in the case where it follows another
configuration pragma that it names, which causes the preceding
pragma to be ignored after parsing.
* errout.adb (Should_Ignore_Pragma_SPARK_Mode): New query.
(SPARK_Msg_N): Do nothing if SPARK_Mode is ignored.
(SPARK_Msg_NE): Same.
* gnat-style.texi: Regenerate.
* gnat_rm.texi: Regenerate.
* gnat_ugn.texi: Regenerate.
Diffstat (limited to 'gcc/ada/gen_il-fields.ads')
0 files changed, 0 insertions, 0 deletions