From patchwork Tue Jul 12 12:25:26 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1655381 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=fYkYZaAN; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4Lj0Qz3JK2z9sB4 for ; Tue, 12 Jul 2022 22:28:27 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 4E68D3944DCD for ; Tue, 12 Jul 2022 12:28:25 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 4E68D3944DCD DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1657628905; bh=rp/QXaEo0gGFKEHZjaX9Z2A0jqB4NOsztY90hbNp8Ik=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=fYkYZaANiC204EUKi1aURJoU5TxTFL6Rzchmt48aqtYFFMJIkB5s92dZO4Z+ZYoK2 TFkcDNnHS+5GCTdQ2wM3doyy4R+Oo5lfwVZ2/TT7NYrCmiR89IryRyUnv3Csy1PH5J eIag0HklJlTArrt4DjHMRRecDxtZgBkVIuhyozIg= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-ej1-x631.google.com (mail-ej1-x631.google.com [IPv6:2a00:1450:4864:20::631]) by sourceware.org (Postfix) with ESMTPS id 6EB173836F90 for ; Tue, 12 Jul 2022 12:25:29 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 6EB173836F90 Received: by mail-ej1-x631.google.com with SMTP id h23so13965523ejj.12 for ; Tue, 12 Jul 2022 05:25:29 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=rp/QXaEo0gGFKEHZjaX9Z2A0jqB4NOsztY90hbNp8Ik=; b=ExOLla1LN9Q4AwIxv8ReNv5FGQtbb4QzH1P/fww4qXa4n3e9kc8rQJiEW+TgXZxUPI ErFLEK1V0BXi43RHn2zdDffbWIik+tjkG0+EJtif+ZqI4cHDsgdbCP7oyyGTekmkpcCw CRG5Los+Wpu3VgBG8w+/ePjeazNnhW7uiRc1nhDrg+R9EVymxGVUPAgDIdJGlUesjZl4 D97HHxTsrjN6ZlKTYEfWKMII5YAr2KgcBg26SRgzPaBEZ+1VzImYay4kiboi7IhqCzwd 8cbpY2USKgYdaKZLNq6ThUrz+fDEzPPJ8B5Ie9oKEVZ7+a6YQCuc3Q1tL7en7b0t6KMF oa5w== X-Gm-Message-State: AJIora/xPzVrQC2P+f4ucFgBE5IeV/oNASXY8iJACrSnyX8d+G8AGsGC tJO7GYAbkB3NFhYVFDONUMlD6RlcwCfa1g== X-Google-Smtp-Source: AGRyM1sEMeJIjXve+I8g+OHmonoU6zRHomOT0CSpqdXLOH/hUXk3B+TSdRlB8BnPfBPNUQcGvOrH2A== X-Received: by 2002:a17:907:1c12:b0:72b:4a03:2290 with SMTP id nc18-20020a1709071c1200b0072b4a032290mr13520300ejc.163.1657628728182; Tue, 12 Jul 2022 05:25:28 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id f15-20020a17090631cf00b0072af3deb944sm3727047ejf.223.2022.07.12.05.25.27 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 12 Jul 2022 05:25:27 -0700 (PDT) Date: Tue, 12 Jul 2022 12:25:26 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Ignore switches for controlling frontend warnings in GNATprove mode Message-ID: <20220712122526.GA3404840@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.8 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" In the special mode for GNATprove, ignore switches controlling frontend warnings, like already done for the control of style checks warnings. Also remove special handling of warning mode in Errout to make up for the previous division of control between -gnatw (GNAT) and --warnings (GNATprove). Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * errout.adb (Record_Compilation_Errors): Remove global variable. (Compilation_Errors): Simplify. (Initialize): Inline Reset_Warnings. (Reset_Warnings): Remove. * errout.ads (Reset_Warnings): Remove. (Compilation_Errors): Update comment. * gnat1drv.adb (Adjust_Global_Switches): Ignore all frontend warnings in GNATprove mode, except regarding elaboration and suspicious contracts. diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -64,13 +64,6 @@ package body Errout is Finalize_Called : Boolean := False; -- Set True if the Finalize routine has been called - Record_Compilation_Errors : Boolean := False; - -- Record that a compilation error was witnessed during a given phase of - -- analysis for gnat2why. This is needed as Warning_Mode is modified twice - -- in gnat2why, hence Erroutc.Compilation_Errors can only return a suitable - -- value for each phase of analysis separately. This is updated at each - -- call to Compilation_Errors. - Warn_On_Instance : Boolean; -- Flag set true for warning message to be posted on instance @@ -252,17 +245,8 @@ package body Errout is begin if not Finalize_Called then raise Program_Error; - - -- Record that a compilation error was witnessed during a given phase of - -- analysis for gnat2why. This is needed as Warning_Mode is modified - -- twice in gnat2why, hence Erroutc.Compilation_Errors can only return a - -- suitable value for each phase of analysis separately. - else - Record_Compilation_Errors := - Record_Compilation_Errors or else Erroutc.Compilation_Errors; - - return Record_Compilation_Errors; + return Erroutc.Compilation_Errors; end if; end Compilation_Errors; @@ -1914,7 +1898,10 @@ package body Errout is -- Reset counts for warnings - Reset_Warnings; + Warnings_Treated_As_Errors := 0; + Warnings_Detected := 0; + Warning_Info_Messages := 0; + Warnings_As_Errors_Count := 0; -- Initialize warnings tables @@ -3414,18 +3401,6 @@ package body Errout is end loop; end Remove_Warning_Messages; - -------------------- - -- Reset_Warnings -- - -------------------- - - procedure Reset_Warnings is - begin - Warnings_Treated_As_Errors := 0; - Warnings_Detected := 0; - Warning_Info_Messages := 0; - Warnings_As_Errors_Count := 0; - end Reset_Warnings; - ---------------------- -- Adjust_Name_Case -- ---------------------- diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads --- a/gcc/ada/errout.ads +++ b/gcc/ada/errout.ads @@ -858,11 +858,6 @@ package Errout is -- Remove warnings on all elements of a list (Calls Remove_Warning_Messages -- on each element of the list, see above). - procedure Reset_Warnings; - -- Reset the counts related to warnings. This is used both to initialize - -- these counts and to reset them after each phase of analysis for a given - -- value of Opt.Warning_Mode in gnat2why. - procedure Set_Ignore_Errors (To : Boolean); -- Following a call to this procedure with To=True, all error calls are -- ignored. A call with To=False restores the default treatment in which @@ -910,11 +905,10 @@ package Errout is -- matching Warnings Off pragma preceding this one. function Compilation_Errors return Boolean; - -- Returns True if errors have been detected, or warnings in -gnatwe (treat - -- warnings as errors) mode. Note that it is mandatory to call Finalize - -- before calling this routine. To account for changes to Warning_Mode in - -- gnat2why between phases, the past or current presence of an error is - -- recorded in a global variable at each call. + -- Returns True if errors have been detected, or warnings when they are + -- treated as errors, which corresponds to switch -gnatwe in the compiler, + -- and other switches in other tools. Note that it is mandatory to call + -- Finalize before calling this routine. procedure Error_Msg_CRT (Feature : String; N : Node_Id); -- Posts a non-fatal message on node N saying that the feature identified diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -557,10 +557,14 @@ procedure Gnat1drv is Validity_Checks_On := False; Check_Validity_Of_Parameters := False; - -- Turn off style check options since we are not interested in any - -- front-end warnings when we are getting SPARK output. + -- Turn off style checks and compiler warnings in GNATprove except: + -- - elaboration warnings, which turn into errors on SPARK code + -- - suspicious contracts, which are useful for SPARK code Reset_Style_Check_Options; + Restore_Warnings (W => (Elab_Warnings => True, + Warn_On_Suspicious_Contract => True, + others => False)); -- Suppress the generation of name tables for enumerations, which are -- not needed for formal verification, and fall outside the SPARK