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