From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id DFEA93857C5A; Tue, 20 Jun 2023 07:47:07 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org DFEA93857C5A DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687247227; bh=3MBxKpJ/p9aNGcyyY2a1R0uV3728dnf3glH8obhqcSc=; h=From:To:Subject:Date:From; b=cUADGczWcodFa8ZSJ8wXp+Io/X6v0LwBQcEUjpoLkk/O8+hRcxU/1R5oLGOUFvV9F ydbgdGrzqx/nQrE/rsUpi4QmKuj6C3CyhkqklnVHt+6puxxfHIRxo9I5jto38fVX8h 9bUTRlcrLqaiabMWKOq9lZ6A8xqhItFjJEe+21gI= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-1976] ada: Add the ability to add error codes to error messages X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: b367a66cfb620b88338111eebd549cc2fad1c16b X-Git-Newrev: f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8 Message-Id: <20230620074707.DFEA93857C5A@sourceware.org> Date: Tue, 20 Jun 2023 07:47:07 +0000 (GMT) List-Id: https://gcc.gnu.org/g:f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8 commit r14-1976-gf1c15fe3f054d453f94e1412ec5bcb2c1e7205e8 Author: Yannick Moy 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