From patchwork Tue Dec 19 14:30:08 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: 82487 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id BFA36386183A for ; Tue, 19 Dec 2023 14:30:36 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32d.google.com (mail-wm1-x32d.google.com [IPv6:2a00:1450:4864:20::32d]) by sourceware.org (Postfix) with ESMTPS id 137633858417 for ; Tue, 19 Dec 2023 14:30:12 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 137633858417 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 137633858417 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::32d ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1702996214; cv=none; b=D9S++tYkCOAlNpVT7pA/fB0uFXDAPzYKBJWTe+qboY52UM9oqih7u1ZXw7q+PVOLCXmCgYp46qICeGQigJkLBpfFonqNbuLfd9S+jprJn9y3azNSbxS968Actt/4YDs8KIt+HAQyfAXkmahXDywsh53ybx2dO5OpotRVcEusMp4= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1702996214; c=relaxed/simple; bh=U9f9qy22Qg4krpI0wMZOMsbPUtI5SbYCv4pv7BGlWUE=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Cu0Abk7qjE0KVgkKdGoBfFbtmMxu5Ok+oGKt+pfdSsCFGNnsxdfkoRKvR6EAE7O045PA16UdOREucU2ZxZ6MH7f+XTZvjxu+2a+0yiPCnpDImoekdcP17fmjb8mgpnqrdfJZJGRDjXFBnJU93/ZGdZgHmJJGHp9jjXzO+ZV78K0= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wm1-x32d.google.com with SMTP id 5b1f17b1804b1-40c3fe6c08fso53173435e9.1 for ; Tue, 19 Dec 2023 06:30:12 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1702996209; x=1703601009; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=UKVbj0ce0baf8ESU7iHHhoWzTqixrLouwcYTGN+k908=; b=gpQfOAmNR0t2NIxHYN5V5BPRpwedcHP+scPq3ZNVyCH3KI0LJwyrNv8IhpekB1vBqY nOVKPFgxqrY0ywmgMxBeLel1QfG4kU/7pu6dy6TkBN1QS1ygAdODS3Ay/8LDkBhO6GLK C0o0VWvC67ZYJL0QfCKXEX1a76u33FOVGCifCb2Kh6gSvguH2BSgyj1Y5Bin4KAsUuli BVyQJPVGDJF6p75Yg+FfX1lqXkBJIKaMRop9MrxiG5RHwELJXmKXmnOR06uk14jtuyJe 29AhiOmX4uMH/K17wv5kPsje5ntcZ9+ooWmky/HxXZMEHzkQ2LQ40isgFoTxQO6Pj7Kg HUwQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1702996209; x=1703601009; 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=UKVbj0ce0baf8ESU7iHHhoWzTqixrLouwcYTGN+k908=; b=OfOD8eYre2XYejGeiJvLY8wSuyTXBu17fCJXznlKPzda9WE957eXl3ochyZdu3bTGZ cK5NnzlbsDjiYTM2eJnuAm0f3xf6nZ1CI/2VVEe3ymV60tIBEyEc46ZfaEB8rZ5QAUlG 18xBBqgHmKqMafN42Pfs5Ddx8ltNTXe1Kmxa0qT4BDGd9XE5N/WCucH5F4S5VvG93mpz 7PiHVir4TgQLeK/qWhmPJq1+ErbHBNXFlT4jDdY/0d8gqKTxBhPBGVmmhB4j5s68YPTQ xSwgeo75FnWmxfXWHu/2NpQz3pcfPVGqrHLF/bQSQaznzpbB1VWY5sDuH90DSCTYrzlF TeZA== X-Gm-Message-State: AOJu0YxdDjxf04LDGx+sClEZVb8c9yKld82ju3BcCFOtaCJ6s4RFZm06 X8QTHiUdlR8L3vBMSX9dsRyyXvcdnG8NbPkzrUE= X-Google-Smtp-Source: AGHT+IFGBRxFlT896UYOekTYXJyLXs7lkAHEX1ba2tj5niXlAsl3xtIVd0vtKPjpwZNY2HG1ohHB+g== X-Received: by 2002:a05:600c:492f:b0:40c:2dd8:bb35 with SMTP id f47-20020a05600c492f00b0040c2dd8bb35mr6865960wmp.77.1702996209492; Tue, 19 Dec 2023 06:30:09 -0800 (PST) Received: from poulhies-Precision-5550.lan ([2001:861:3382:1a90:fe1e:443:c34f:edaa]) by smtp.gmail.com with ESMTPSA id c5-20020a05600c0a4500b0040c411da99csm3071727wmq.48.2023.12.19.06.30.08 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 Dec 2023 06:30:09 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Cleanup SPARK legality checking Date: Tue, 19 Dec 2023 15:30:08 +0100 Message-ID: <20231219143008.454633-1-poulhies@adacore.com> X-Mailer: git-send-email 2.43.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.0 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.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org From: Yannick Moy Move one SPARK legality check from GNAT to GNATprove, and cleanup other uses of SPARK_Mode for legality checking. gcc/ada/ * sem_ch4.adb (Analyze_Selected_Component): Check correct mode variable for GNATprove. * sem_prag.adb (Refined_State): Call SPARK_Msg_NE which checks value of SPARK_Mode before issuing a message. * sem_res.adb (Resolve_Entity_Name): Remove legality check for SPARK RM 6.1.9(1), moved to GNATprove. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_ch4.adb | 10 ++--- gcc/ada/sem_prag.adb | 12 +++--- gcc/ada/sem_res.adb | 100 ------------------------------------------- 3 files changed, 10 insertions(+), 112 deletions(-) diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index d506944bc8d..64aa9a84e60 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -6025,17 +6025,17 @@ package body Sem_Ch4 is -- Emit appropriate message. The node will be replaced -- by an appropriate raise statement. - -- Note that in SPARK mode, as with all calls to apply a - -- compile time constraint error, this will be made into - -- an error to simplify the processing of the formal - -- verification backend. + -- Note that in GNATprove mode, as with all calls to + -- apply a compile time constraint error, this will be + -- made into an error to simplify the processing of the + -- formal verification backend. Apply_Compile_Time_Constraint_Error (N, "component not present in }??", CE_Discriminant_Check_Failed, Ent => Prefix_Type, Emit_Message => - SPARK_Mode = On or not In_Instance_Not_Visible); + GNATprove_Mode or not In_Instance_Not_Visible); return; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9d66fb71a06..db20f20b9f1 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23375,15 +23375,13 @@ package body Sem_Prag is Analyze_If_Present (Pragma_SPARK_Mode); -- State refinement is allowed only when the corresponding package - -- declaration has non-null pragma Abstract_State. Refinement not - -- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)). + -- declaration has non-null pragma Abstract_State (SPARK RM + -- 7.2.2(3)). - if SPARK_Mode /= Off - and then - (No (Abstract_States (Spec_Id)) - or else Has_Null_Abstract_State (Spec_Id)) + if No (Abstract_States (Spec_Id)) + or else Has_Null_Abstract_State (Spec_Id) then - Error_Msg_NE + SPARK_Msg_NE ("useless refinement, package & does not define abstract " & "states", N, Spec_Id); return; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index c684075219b..d81a5af9032 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7787,14 +7787,6 @@ package body Sem_Res is -- Determine whether Expr is part of an N_Attribute_Reference -- expression. - function In_Attribute_Old (Expr : Node_Id) return Boolean; - -- Determine whether Expr is in attribute Old - - function Within_Exceptional_Cases_Consequence - (Expr : Node_Id) - return Boolean; - -- Determine whether Expr is part of an Exceptional_Cases consequence - ---------------------------------------- -- Is_Assignment_Or_Object_Expression -- ---------------------------------------- @@ -7836,31 +7828,6 @@ package body Sem_Res is end if; end Is_Assignment_Or_Object_Expression; - ---------------------- - -- In_Attribute_Old -- - ---------------------- - - function In_Attribute_Old (Expr : Node_Id) return Boolean is - N : Node_Id := Expr; - begin - while Present (N) loop - if Nkind (N) = N_Attribute_Reference - and then Attribute_Name (N) = Name_Old - then - return True; - - -- Prevent the search from going too far - - elsif Is_Body_Or_Package_Declaration (N) then - return False; - end if; - - N := Parent (N); - end loop; - - return False; - end In_Attribute_Old; - ----------------------------- -- Is_Attribute_Expression -- ----------------------------- @@ -7884,39 +7851,6 @@ package body Sem_Res is return False; end Is_Attribute_Expression; - ------------------------------------------ - -- Within_Exceptional_Cases_Consequence -- - ------------------------------------------ - - function Within_Exceptional_Cases_Consequence - (Expr : Node_Id) - return Boolean - is - Context : Node_Id := Parent (Expr); - begin - while Present (Context) loop - if Nkind (Context) = N_Pragma then - - -- In Exceptional_Cases references to formal parameters are - -- only allowed within consequences, so it is enough to - -- recognize the pragma itself. - - if Get_Pragma_Id (Context) = Pragma_Exceptional_Cases then - return True; - end if; - - -- Prevent the search from going too far - - elsif Is_Body_Or_Package_Declaration (Context) then - return False; - end if; - - Context := Parent (Context); - end loop; - - return False; - end Within_Exceptional_Cases_Consequence; - -- Local variables E : constant Entity_Id := Entity (N); @@ -8048,40 +7982,6 @@ package body Sem_Res is if SPARK_Mode = On then - -- Parameters of modes OUT or IN OUT of the subprogram shall not - -- occur in the consequences of an exceptional contract unless - -- they are either passed by reference or occur in the prefix - -- of a reference to the 'Old attribute. For convenience, we also - -- allow them as prefixes of attributes that do not actually read - -- data from the object. - - if Ekind (E) in E_Out_Parameter | E_In_Out_Parameter - and then Scope (E) = Current_Scope_No_Loops - and then Within_Exceptional_Cases_Consequence (N) - and then not In_Attribute_Old (N) - and then not (Nkind (Parent (N)) = N_Attribute_Reference - and then - Attribute_Name (Parent (N)) in Name_Constrained - | Name_First - | Name_Last - | Name_Length - | Name_Range) - and then not Is_By_Reference_Type (Etype (E)) - and then not Is_Aliased (E) - then - if Ekind (E) = E_Out_Parameter then - Error_Msg_N - ("formal parameter of mode `OUT` cannot appear " & - "in consequence of Exceptional_Cases", N); - else - Error_Msg_N - ("formal parameter of mode `IN OUT` cannot appear " & - "in consequence of Exceptional_Cases", N); - end if; - Error_Msg_N - ("\only parameters passed by reference are allowed", N); - end if; - -- Check for possible elaboration issues with respect to reads of -- variables. The act of renaming the variable is not considered a -- read as it simply establishes an alias.