diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 26bc4b39735..77578dacc18 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1040,11 +1040,12 @@ package body Contracts is
             --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
 
             if not Is_Library_Level_Entity (Type_Or_Obj_Id) then
+               Error_Msg_Code := GEC_Volatile_At_Library_Level;
                Error_Msg_N
                  ("effectively volatile "
                     & Decl_Kind
-                    & " & must be declared at library level "
-                    & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id);
+                    & " & must be declared at library level '[[]']",
+                    Type_Or_Obj_Id);
 
             --  An object of a discriminated type cannot be effectively
             --  volatile except for protected objects (SPARK RM 7.1.3(5)).
diff --git a/gcc/ada/err_vars.ads b/gcc/ada/err_vars.ads
index e73e9fb295a..e84efb65575 100644
--- a/gcc/ada/err_vars.ads
+++ b/gcc/ada/err_vars.ads
@@ -100,6 +100,11 @@ package Err_Vars is
    Error_Msg_Uint_2 : Uint := No_Uint;
    --  Uint values for ^ insertion characters in message
 
+   Error_Msg_Code_Digits : constant := 4;
+   Error_Msg_Code : Nat range 0 .. 10 ** Error_Msg_Code_Digits - 1;
+   --  Nat value for [] insertion sequence in message, where a value of zero
+   --  indicates the absence of an error code.
+
    --  WARNING: There is a matching C declaration of these variables in fe.h
 
    Error_Msg_Sloc : Source_Ptr;
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 6e378a60731..adc260843ec 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)
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index f152839678d..80dd7dfaead 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
 
@@ -599,6 +608,21 @@ package Errout is
      renames Erroutc.Get_Location;
    --  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 --
    ------------------------
diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index e5caeba6802..5a8556ba900 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -959,6 +959,7 @@ package body Erroutc is
       end if;
 
       Has_Double_Exclam  := False;
+      Has_Error_Code     := False;
       Has_Insertion_Line := False;
 
       --  Loop through message looking for relevant insertion sequences
@@ -1012,6 +1013,15 @@ package body Erroutc is
             Is_Serious_Error := False;
             J := J + 1;
 
+         --  Error code ([] insertion)
+
+         elsif Msg (J) = '['
+           and then J < Msg'Last
+           and then Msg (J + 1) = ']'
+         then
+            Has_Error_Code := True;
+            J := J + 2;
+
          else
             J := J + 1;
          end if;
@@ -1156,6 +1166,42 @@ package body Erroutc is
       end if;
    end Set_Msg_Char;
 
+   ----------------------------
+   -- Set_Msg_Insertion_Code --
+   ----------------------------
+
+   procedure Set_Msg_Insertion_Code is
+      H : constant array (Nat range 0 .. 9) of Character := "0123456789";
+      P10 : constant array (Natural range 0 .. 3) of Nat :=
+        (10 ** 0,
+         10 ** 1,
+         10 ** 2,
+         10 ** 3);
+
+      Code_Len : constant Natural :=
+        (case Error_Msg_Code is
+           when    0         => 0,
+           when    1 ..    9 => 1,
+           when   10 ..   99 => 2,
+           when  100 ..  999 => 3,
+           when 1000 .. 9999 => 4);
+      Code_Rest  : Nat := Error_Msg_Code;
+      Code_Digit : Nat;
+
+   begin
+      Set_Msg_Char ('E');
+
+      for J in 1 .. Error_Msg_Code_Digits - Code_Len loop
+         Set_Msg_Char ('0');
+      end loop;
+
+      for J in 1 .. Code_Len loop
+         Code_Digit := Code_Rest / P10 (Code_Len - J);
+         Set_Msg_Char (H (Code_Digit));
+         Code_Rest := Code_Rest - Code_Digit * P10 (Code_Len - J);
+      end loop;
+   end Set_Msg_Insertion_Code;
+
    ---------------------------------
    -- Set_Msg_Insertion_File_Name --
    ---------------------------------
diff --git a/gcc/ada/erroutc.ads b/gcc/ada/erroutc.ads
index c32b19ffe88..6602907a3c7 100644
--- a/gcc/ada/erroutc.ads
+++ b/gcc/ada/erroutc.ads
@@ -51,6 +51,10 @@ package Erroutc is
    --  Set true to indicate that the current message contains the insertion
    --  sequence !! (force warnings even in non-main unit source files).
 
+   Has_Error_Code : Boolean := False;
+   --  Set true to indicate that the current message contains the insertion
+   --  sequence [] (insert error code).
+
    Has_Insertion_Line : Boolean := False;
    --  Set True to indicate that the current message contains the insertion
    --  character # (insert line number reference).
@@ -547,6 +551,9 @@ package Erroutc is
    --    Has_Double_Exclam is set True if the message contains the sequence !!
    --    and is otherwise set False.
    --
+   --    Has_Error_Code is set True if the message contains the sequence []
+   --    and is otherwise set False.
+   --
    --    Has_Insertion_Line is set True if the message contains the character #
    --    and is otherwise set False.
    --
@@ -581,6 +588,9 @@ package Erroutc is
    --  check for special insertion characters (they are just treated as text
    --  characters if they occur).
 
+   procedure Set_Msg_Insertion_Code;
+   --  Handle error code insertion ([] insertion character)
+
    procedure Set_Msg_Insertion_File_Name;
    --  Handle file name insertion (left brace insertion character)
 
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index dc81e47da9e..46bad04a889 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -15316,9 +15316,10 @@ package body Sem_Elab is
 
             if Earlier_In_Extended_Unit (FNode, Region) then
                Error_Msg_Node_2 := Prim;
+               Error_Msg_Code := GEC_Type_Early_Call_Region;
                Error_Msg_NE
                  ("first freezing point of type & must appear within early "
-                  & "call region of primitive body & (SPARK RM 7.7(8))",
+                  & "call region of primitive body '[[]']",
                   Typ_Decl, Typ);
 
                Error_Msg_Sloc := Sloc (Region);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index bcae43ff59d..c5810685dc3 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -30974,9 +30974,10 @@ package body Sem_Prag is
          --  All other cases require Part_Of
 
          else
+            Error_Msg_Code := GEC_Required_Part_Of;
             Error_Msg_N
-              ("indicator Part_Of is required in this context "
-               & "(SPARK RM 7.2.6(2))", Item_Id);
+              ("indicator Part_Of is required in this context '[[]']",
+               Item_Id);
             Error_Msg_Name_1 := Chars (Pack_Id);
             Error_Msg_N
               ("\& is declared in the private part of package %", Item_Id);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ef3b877f5db..f4dfc041cd6 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3914,9 +3914,10 @@ package body Sem_Res is
                                                   Obj_Ref       => N,
                                                   Check_Actuals => True)
                   then
+                     Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
                      Error_Msg_N
-                       ("volatile object cannot appear in this context"
-                        & " (SPARK RM 7.1.3(10))", N);
+                       ("volatile object cannot appear in this context '[[]']",
+                        N);
                   end if;
 
                   return Skip;
@@ -8103,9 +8104,9 @@ package body Sem_Res is
               and then
                 not Is_OK_Volatile_Context (Par, N, Check_Actuals => False)
             then
+               Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
                SPARK_Msg_N
-                 ("volatile object cannot appear in this context "
-                  & "(SPARK RM 7.1.3(10))", N);
+                 ("volatile object cannot appear in this context '[[]']", N);
             end if;
 
             --  Parameters of modes OUT or IN OUT of the subprogram shall not
