public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r14-1976] ada: Add the ability to add error codes to error messages
@ 2023-06-20 7:47 Marc Poulhi?s
0 siblings, 0 replies; only message in thread
From: Marc Poulhi?s @ 2023-06-20 7:47 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8
commit r14-1976-gf1c15fe3f054d453f94e1412ec5bcb2c1e7205e8
Author: Yannick Moy <moy@adacore.com>
Date: Wed May 10 16:10:54 2023 +0200
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.
Diff:
---
gcc/ada/contracts.adb | 5 +++--
gcc/ada/err_vars.ads | 5 +++++
gcc/ada/errout.adb | 48 ++++++++++++++++++++++++++++++++++++------------
gcc/ada/errout.ads | 24 ++++++++++++++++++++++++
gcc/ada/erroutc.adb | 46 ++++++++++++++++++++++++++++++++++++++++++++++
gcc/ada/erroutc.ads | 10 ++++++++++
gcc/ada/sem_elab.adb | 3 ++-
gcc/ada/sem_prag.adb | 5 +++--
gcc/ada/sem_res.adb | 9 +++++----
9 files changed, 134 insertions(+), 21 deletions(-)
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-06-20 7:47 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-06-20 7:47 [gcc r14-1976] ada: Add the ability to add error codes to error messages Marc Poulhi?s
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).