diff options
| author | Yannick Moy <moy@adacore.com> | 2023-11-21 16:48:20 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-12-19 15:27:47 +0100 |
| commit | da5dca1d36d5a70b3068825f74612000973a819e (patch) | |
| tree | e4bce548453d541be3ea8c308ec95e5f6002b841 /gcc/btfout.cc | |
| parent | 27fd2dc518b696d260336a60fbb0c8baa1ef80a6 (diff) | |
| download | gcc-da5dca1d36d5a70b3068825f74612000973a819e.zip gcc-da5dca1d36d5a70b3068825f74612000973a819e.tar.gz gcc-da5dca1d36d5a70b3068825f74612000973a819e.tar.bz2 | |
ada: Cleanup SPARK legality checking
Move one SPARK legality check from GNAT to GNATprove, and cleanup
other uses of SPARK_Mode for legality checking.
gcc/ada/
* sem_ch4.adb (Analyze_Selected_Component): Check correct mode
variable for GNATprove.
* sem_prag.adb (Refined_State): Call SPARK_Msg_NE which checks
value of SPARK_Mode before issuing a message.
* sem_res.adb (Resolve_Entity_Name): Remove legality check for
SPARK RM 6.1.9(1), moved to GNATprove.
Diffstat (limited to 'gcc/btfout.cc')
0 files changed, 0 insertions, 0 deletions