diff options
| author | Yannick Moy <moy@adacore.com> | 2023-06-27 11:49:09 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-07-06 13:36:09 +0200 |
| commit | d1715f6e7613969d44ab6ab0585eb99200fd62cc (patch) | |
| tree | 61c0342b2dd6f4d404e9f17d757af7733768e5a5 /gcc | |
| parent | fd4f48b37718748b39344129e70223a5d290c6eb (diff) | |
| download | gcc-d1715f6e7613969d44ab6ab0585eb99200fd62cc.zip gcc-d1715f6e7613969d44ab6ab0585eb99200fd62cc.tar.gz gcc-d1715f6e7613969d44ab6ab0585eb99200fd62cc.tar.bz2 | |
ada: Improve error message on violation of SPARK_Mode rules
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/errout.ads | 1 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 4 |
2 files changed, 4 insertions, 1 deletions
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index 80dd7df..2065d73 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 c581068..6de87fb 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; |