* [COMMITTED] ada: Improve error message on violation of SPARK_Mode rules
@ 2023-07-06 11:38 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-07-06 11:38 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
From: Yannick Moy <moy@adacore.com>
SPARK_Mode On can only be used on library-level entities.
Improve the error message here.
gcc/ada/
* errout.ads: Add explain code.
* sem_prag.adb (Check_Library_Level_Entity): Refine error message
and add explain code.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/errout.ads | 1 +
gcc/ada/sem_prag.adb | 4 +++-
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index 80dd7dfaead..2065d73614a 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -622,6 +622,7 @@ package Errout is
GEC_Volatile_Non_Interfering_Context : constant := 0004;
GEC_Required_Part_Of : constant := 0009;
GEC_Ownership_Moved_Object : constant := 0010;
+ GEC_SPARK_Mode_On_Not_Library_Level : constant := 0011;
------------------------
-- List Pragmas Table --
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c5810685dc3..6de87fbaba9 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -24144,7 +24144,8 @@ package body Sem_Prag is
-- Local variables
- Msg_1 : constant String := "incorrect placement of pragma%";
+ Msg_1 : constant String :=
+ "incorrect placement of pragma% with value ""On"" '[[]']";
Msg_2 : Name_Id;
-- Start of processing for Check_Library_Level_Entity
@@ -24161,6 +24162,7 @@ package body Sem_Prag is
and then Instantiation_Location (Sloc (N)) = No_Location
then
Error_Msg_Name_1 := Pname;
+ Error_Msg_Code := GEC_SPARK_Mode_On_Not_Library_Level;
Error_Msg_N (Fix_Error (Msg_1), N);
Name_Len := 0;
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-07-06 11:38 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-07-06 11:38 [COMMITTED] ada: Improve error message on violation of SPARK_Mode rules Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).