From patchwork Tue Jun 20 07:52:10 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 110313 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:994d:0:b0:3d9:f83d:47d9 with SMTP id k13csp3497954vqr; Tue, 20 Jun 2023 00:59:01 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ4f957ZdPGAupaEwKK0/IRLojgBwERBfEIlh81i96gShHbPxxnDDgt3wDW39L1eE2F3e7KY X-Received: by 2002:a17:906:7312:b0:96a:3119:ac0 with SMTP id di18-20020a170906731200b0096a31190ac0mr8543075ejc.69.1687247941344; Tue, 20 Jun 2023 00:59:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1687247941; cv=none; d=google.com; s=arc-20160816; b=MAMv7QeEnS2v9hKxoDD9D4Byuqr2m2MjtoRwjmfJdrnOskGX1gewwnqUnxaFdPg16I 4v9ffLDgayfkNodoR1BmQio83f5MITV9oXq/LOCMW5UN0YEY2CQReM7S7Vl3p5v8LQBL tk4aL2xYtORiyVpRpD0CGGcsDnJ6WxKWBlXwpOgGjW2cpEjRKr+x7K7ET105h/r+Rp3L MA164Fhqt8uZdTc8oH6pcNtTt++yHwuAnb9Hbm6u4yTlm8I6sXp4zEB5z5jOBQaqkLt5 KWfPoaRBe6y4WuWRXZvoR2DbDBcqM2zqCRcNlp8TJpAjW7Qk5AomNLplOD08a8ytROtV ZAkg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=F2EwOhAFqprzv0yo6KjDu01o67zIcUcRoD4F9/QkNUE=; b=BbClrrcO0xHDuMUGxXo2FmN63FrmYv+Nh5UWUyWPmrPE4IQWud3fqzgO6PDwwx6BLG vXudTjJDRykukcWRAMjTRmqDrlpDleG0HOj9R64ZIv/DWcVcXaJCZAXp9YtPwRXF9OHl OxXq1dMYRCYIvD6rvGYQXIVa9du+k+x44B90S0/X4CODTpbjcT3cbHekRfg4P/z5D23x EYDrIQsJqV4N2U9EVnrznUUzha77Tel6UqVBm+JZBKzuTG1kJOMkyvQBTlo5l0ccdj02 f2ozp2r+NTliNq7DYGxeERigJwPUS9gXDT3cF1lTejVpH7AJrIC9KBgLZeU1jmH86qJW gEjw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b="h/PVZbJq"; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id t14-20020a1709066bce00b0097462d656f8si933143ejs.581.2023.06.20.00.59.00 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Jun 2023 00:59:01 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b="h/PVZbJq"; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id CDAE0388B69C for ; Tue, 20 Jun 2023 07:53:04 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org CDAE0388B69C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687247584; bh=F2EwOhAFqprzv0yo6KjDu01o67zIcUcRoD4F9/QkNUE=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=h/PVZbJqhY1ErywldVCtqlADsGdpTZERxviwq9fJWRIWlteKRNZ7lEiVG5Dj9iD4v 0wvRTDBUOTp4CuOb8C3DmpVF0nHxlgsmq1koK4GgVQQCur9GlGLz97FIF7/V7BXt6f VYi4I/366sLrzZaAYFLpZLUd4C7nvdF+jfBN9LWE= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x435.google.com (mail-wr1-x435.google.com [IPv6:2a00:1450:4864:20::435]) by sourceware.org (Postfix) with ESMTPS id 0EDCC38A817E for ; Tue, 20 Jun 2023 07:52:13 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 0EDCC38A817E Received: by mail-wr1-x435.google.com with SMTP id ffacd0b85a97d-31121494630so5061403f8f.3 for ; Tue, 20 Jun 2023 00:52:13 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1687247532; x=1689839532; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=F2EwOhAFqprzv0yo6KjDu01o67zIcUcRoD4F9/QkNUE=; b=CJc+q1IagweKreN4oCgmIjXUyITiFQWoicd/m8Y1/5vKj+u30YttQILPDERu/gkU8j 6c2l/PPfwrue3VLkHVqzPhI8LN5zNsZ2L1pG+9l5DHGqPJ7mHzhyIFAwHPP0iNfTiwP2 RI1beEKkBl30mBktz27QFGUcKfhH4dNBA13lzjywy3TLRr+o8aRLZ4cjT9ER+zcnUbhU L0TcfmHXeM2dVv87jVcAhpGxwZypeymWEAO2vh6iCXQX1vmW5noTLM940eV313faUNsD 4lAIhavq7eAhhUq1hglkIjEiwHNochfsrlQf/RA9CzDXrviQ4/8huOjXI8cGKpdy5pdi HLMQ== X-Gm-Message-State: AC+VfDwdHmjtYeWI6lsl/owxKfs/BoBr2QqhA1YdDEORDqT40IsP70dp OhUVj2ssIcxDCBykHIAJoxgk4aK3hI7XHCiU1LbHeA== X-Received: by 2002:adf:f203:0:b0:2f9:4fe9:74bb with SMTP id p3-20020adff203000000b002f94fe974bbmr10473920wro.40.1687247531821; Tue, 20 Jun 2023 00:52:11 -0700 (PDT) Received: from poulhies-Precision-5550.lan ([2001:861:3382:1a90:4c16:36ea:1b76:c001]) by smtp.gmail.com with ESMTPSA id e14-20020adfe38e000000b0030fcf3d75c4sm1360184wrm.45.2023.06.20.00.52.10 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Jun 2023 00:52:11 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Add the ability to add error codes to error messages Date: Tue, 20 Jun 2023 09:52:10 +0200 Message-Id: <20230620075210.1253631-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.3 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1769207697305036266?= X-GMAIL-MSGID: =?utf-8?q?1769207697305036266?= From: Yannick Moy 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. Tested on x86_64-pc-linux-gnu, committed on master. --- 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