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.
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 --
-- 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
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;