ada: Add the ability to add error codes to error messages

Add a new character sequence [] for error codes in error messages
handled by Error_Msg procedures, to use for SPARK-related errors.
Display of additional information on the error or warning based on
the error code is delegated to GNATprove.

gcc/ada/

	* err_vars.ads (Error_Msg_Code): New variable for error codes.
	* errout.adb (Error_Msg_Internal): Display continuation message
	when an error code was present.
	(Set_Msg_Text): Handle character sequence [] for error codes.
	* errout.ads: Document new insertion sequence [].
	(Error_Msg_Code): New renaming.
	* erroutc.adb (Prescan_Message): Detect presence of error code.
	(Set_Msg_Insertion_Code): Handle new insertion sequence [].
	* erroutc.ads (Has_Error_Code): New variable for prescan.
	(Set_Msg_Insertion_Code): Handle new insertion sequence [].
	* contracts.adb (Check_Type_Or_Object_External_Properties):
	Replace reference to SPARK RM section by an error code.
	* sem_elab.adb (SPARK_Processor): Same.
	* sem_prag.adb (Check_Missing_Part_Of): Same.
	* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Same.

1 files changed, 24 insertions, 0 deletions

diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index f152839..80dd7df 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -404,6 +404,10 @@ package Errout is
    --      This is like [ except that the insertion messages say may/might,
    --      instead of will/would.
 
+   --    Insertion sequence [] (Left and right brackets: error code)
+   --      The insertion sequence [] should be replaced by an error code, whose
+   --      value is given by Error_Msg_Code.
+
    --    Insertion sequence "(style)" (style message)
    --      This appears only at the start of the message (and not any of its
    --      continuations, if any), and indicates that the message is a style
@@ -454,6 +458,11 @@ package Errout is
    Error_Msg_Uint_2 : Uint renames Err_Vars.Error_Msg_Uint_2;
    --  Uint values for ^ insertion characters in message
 
+   Error_Msg_Code_Digits : constant := Err_Vars.Error_Msg_Code_Digits;
+   Error_Msg_Code : Nat renames Err_Vars.Error_Msg_Code;
+   --  Nat value for [] insertion sequence in message, where a value of zero
+   --  indicates the absence of an error code.
+
    Error_Msg_Sloc : Source_Ptr renames Err_Vars.Error_Msg_Sloc;
    --  Source location for # insertion character in message
 
@@ -600,6 +609,21 @@ package Errout is
    --  Returns the flag location of the error message with the given id E
 
    ------------------------
+   -- GNAT Explain Codes --
+   ------------------------
+
+   --  Explain codes are used in GNATprove to provide more information on
+   --  selected error/warning messages. The subset of those codes used in
+   --  the GNAT frontend are defined here.
+
+   GEC_None                             : constant := 0000;
+   GEC_Volatile_At_Library_Level        : constant := 0001;
+   GEC_Type_Early_Call_Region           : constant := 0003;
+   GEC_Volatile_Non_Interfering_Context : constant := 0004;
+   GEC_Required_Part_Of                 : constant := 0009;
+   GEC_Ownership_Moved_Object           : constant := 0010;
+
+   ------------------------
    -- List Pragmas Table --
    ------------------------