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, 36 insertions, 12 deletions

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 6e378a6..adc2608 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1447,6 +1447,22 @@ package body Errout is
             raise Unrecoverable_Error;
          end if;
       end if;
+
+      if Has_Error_Code then
+         declare
+            Msg : constant String :=
+              "launch ""gnatprove --explain=[]"" for more information";
+         begin
+            Prescan_Message (Msg);
+            Has_Error_Code := False;
+            Error_Msg_Internal
+              (Msg      => Msg,
+               Span     => Span,
+               Opan     => Opan,
+               Msg_Cont => True,
+               Node     => Node);
+         end;
+      end if;
    end Error_Msg_Internal;
 
    -----------------
@@ -4338,21 +4354,29 @@ package body Errout is
 
             when '[' =>
 
-               --  Switch the message from a warning to an error if the flag
-               --  -gnatwE is specified to treat run-time exception warnings
-               --  as errors.
+               --  "[]" (insertion of error code)
 
-               if Is_Warning_Msg
-                 and then Warning_Mode = Treat_Run_Time_Warnings_As_Errors
-               then
-                  Is_Warning_Msg   := False;
-                  Is_Runtime_Raise := True;
-               end if;
+               if P <= Text'Last and then Text (P) = ']' then
+                  P := P + 1;
+                  Set_Msg_Insertion_Code;
 
-               if Is_Warning_Msg then
-                  Set_Msg_Str ("will be raised at run time");
                else
-                  Set_Msg_Str ("would have been raised at run time");
+                  --  Switch the message from a warning to an error if the flag
+                  --  -gnatwE is specified to treat run-time exception warnings
+                  --  as errors.
+
+                  if Is_Warning_Msg
+                    and then Warning_Mode = Treat_Run_Time_Warnings_As_Errors
+                  then
+                     Is_Warning_Msg   := False;
+                     Is_Runtime_Raise := True;
+                  end if;
+
+                  if Is_Warning_Msg then
+                     Set_Msg_Str ("will be raised at run time");
+                  else
+                     Set_Msg_Str ("would have been raised at run time");
+                  end if;
                end if;
 
             --   ']' (may be/might have been raised at run time)