From patchwork Mon May 29 08:29:46 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: 100171 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:994d:0:b0:3d9:f83d:47d9 with SMTP id k13csp1367045vqr; Mon, 29 May 2023 01:46:56 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ6AC345hnrrR1Oc4Io7X38DlfUrEzgI44v8L5Cv3fAJq7koXfzXL1A7fjgc/Q6QviomwQ5I X-Received: by 2002:a17:907:3185:b0:973:c999:d639 with SMTP id xe5-20020a170907318500b00973c999d639mr11088768ejb.8.1685350016227; Mon, 29 May 2023 01:46:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1685350016; cv=none; d=google.com; s=arc-20160816; b=z62bHbOlMS2/Z7T2oLHiZsompgbhIm/DQcT3K1cyZPZFooJO2TDjRaZXMADjZa1oTy wel5lyZ5HZiz0uN+QB7dAgDkFpb4MYycWid+wP1evjy0I8kiRWffb7ujSwEa5Cgpsjhp 86vtHJe6mmG6BccdtzyVBnRScFY0+kn2xIO+dc+d9Hx1JXO4mjRCaaX6wcVuk6edgqgh mGk6uRv6LhKIysuWERI97e9IkI4dx4lzEqKTgjrCtVA1btnO8TL2RrSJO4trdz0ibqcp +5Ky53sdU0fBnf0N071PYGrSvM1M4B0USO554HD5cYh85AItM/I354RJhw/FbB3RJZD3 l4Ow== 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=t6Id9VU4Pqz2Q0s4POPEKs2e9mTDpTVsgbvF3k3kzYY=; b=i3YKHVbPfUzBXIVbFRLpfB9PdcUTA4T3byv+7YohUXHjfxsHYRaVarKwnzj+oL+Rdv bLeY6ljyy3RmDCL9ugXV0DWww7b9ousTLzRw3Ar8i+9vd/Pj6vnOcU0r9S+A3YNO1Yu2 1bUWGcEQMH8tFcaDZxqZsv2HBlFsHbMjyvxCbcgxWrH/b85cNds3lMypt3JM7EXjOQpL DEriknd5o2SULxnwpnX5XT+CcZVomNd3ixzrKWrYnaracHcu5VAeWgiqaYYZPxDAJj3S 0rxjRfvpYEvyTJemSCTd6DqH15W80FN7ja0vUtfC0v1tZXtU6JA3mavrHJyMc4lAAFzz 3oKQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=trn8zaj0; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 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 (ip-8-43-85-97.sourceware.org. [8.43.85.97]) by mx.google.com with ESMTPS id o15-20020a170906768f00b0096f0678dde4si419424ejm.312.2023.05.29.01.46.56 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 May 2023 01:46:56 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=trn8zaj0; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 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 A6007396DC38 for ; Mon, 29 May 2023 08:38:58 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org A6007396DC38 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1685349538; bh=t6Id9VU4Pqz2Q0s4POPEKs2e9mTDpTVsgbvF3k3kzYY=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=trn8zaj0/+vuGh213WWwpbJila0q1Zpn+nM6Cgo1BOEVihNqN9aLG+DArsx2rxT9S YnegQxwOYBbg76VXaUsRoddJjRJnP2D7DK+dKODZppbBJuiBgFXiuQjluZjhOta2Or ECq0vtxlvTKApfsCI9DFjhGn/UdgCI4VZzCKmG9g= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x32e.google.com (mail-wm1-x32e.google.com [IPv6:2a00:1450:4864:20::32e]) by sourceware.org (Postfix) with ESMTPS id 02779384603C for ; Mon, 29 May 2023 08:29:48 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 02779384603C Received: by mail-wm1-x32e.google.com with SMTP id 5b1f17b1804b1-3f6e13940daso31854685e9.0 for ; Mon, 29 May 2023 01:29:47 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1685348987; x=1687940987; 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=t6Id9VU4Pqz2Q0s4POPEKs2e9mTDpTVsgbvF3k3kzYY=; b=SzU5skSy0jllOoO0SS1+uRb/7URKW0RDsXhO91VdSPwFmm48mhSo7CkCIZnQLHip4r JpGJK5k/x51bzRGTw9Tv5iZNfQT205zqDP4IIGVVoFJXI3mqAkiX0wWVnBBbixPHxZ2y +Uqul1pmsXXARNCyUCr89a2Pr5Xl8QOu8t2WGJGKf1M0f6EKCzoOpfK74MBOHc2u9ZnP NyTgIG9p5mfXVqb7nH34Bks1DTBzvYH003iIRG9BOxYTVCATLpEXi7LqYXO586xcLymh L1G20UI/OUr8X8EhpN1KPrW4QCw7haZY+P2VumJfUFIHLOFJDnvx5wIV+Ku55mZvSWg6 SAgA== X-Gm-Message-State: AC+VfDzenc7bkf30F7pr7/WI4uKGo2HJJQEgYV1DQ2l9XRktAQhONDB/ 3Mc9kifQ9WcV3KTRzFeqcwJF+lzCBpF98G2r8NBCsA== X-Received: by 2002:a1c:6a03:0:b0:3f5:6e5:1689 with SMTP id f3-20020a1c6a03000000b003f506e51689mr9386524wmc.17.1685348987630; Mon, 29 May 2023 01:29:47 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id u15-20020a05600c210f00b003f42d8dd7d1sm17159248wml.7.2023.05.29.01.29.46 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 May 2023 01:29:47 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Attach pre/post on access-to-subprogram to internal subprogram type Date: Mon, 29 May 2023 10:29:46 +0200 Message-Id: <20230529082946.2410945-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, 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?1767217578666229066?= X-GMAIL-MSGID: =?utf-8?q?1767217578666229066?= From: Piotr Trojanek Aspects Pre/Post that annotate access-to-subprogram type were attached to the source entity (whose kind is either E_Access_Subprogram_Type or E_Access_Protected_Subprogram_Type). However, it is more convenient to attach them to the internal entity (whose kind is E_Subprogram_Type), so that both Pre/Post aspects and First_Formal/Next_Formal chain are attached to the same entity, just like for ordinary subprograms. The drawback of having the Post aspect attached to an internal entity is that name in prefixes of attribute Result no longer match the name of entity where this Post aspect is attached. However, currently there is no code that relies on this matching and, in general, there are fewer routines that deal with attribute Result so they are easier to adapt than the code that queries the Pre/Post aspects. gcc/ada/ * contracts.adb (Add_Pre_Post_Condition): Attach pre/post aspects to E_Subprogram_Type entity. (Analyze_Entry_Or_Subprogram_Contract): Adapt to use full type declaration for a contract attached to E_Subprogram_Type entity. * sem_prag.adb (Analyze_Pre_Post_Condition): Add pre/post aspects to the designed type. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/contracts.adb | 12 ++++++++---- gcc/ada/sem_prag.adb | 6 +++++- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 15b65ee4c06..7625abf9554 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -334,7 +334,7 @@ package body Contracts is if Is_OK_Classification then Add_Classification; - elsif Ekind (Id) in Access_Subprogram_Kind + elsif Ekind (Id) = E_Subprogram_Type and then Prag_Nam in Name_Precondition | Name_Postcondition then @@ -665,7 +665,10 @@ package body Contracts is Freeze_Id : Entity_Id := Empty) is Items : constant Node_Id := Contract (Subp_Id); - Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Subp_Decl : constant Node_Id := + (if Ekind (Subp_Id) = E_Subprogram_Type + then Associated_Node_For_Itype (Subp_Id) + else Unit_Declaration_Node (Subp_Id)); Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; @@ -1593,8 +1596,9 @@ package body Contracts is -- Analyze Pre/Post on access-to-subprogram type - if Is_Access_Subprogram_Type (Type_Id) then - Analyze_Entry_Or_Subprogram_Contract (Type_Id); + if Ekind (Type_Id) in Access_Subprogram_Kind then + Analyze_Entry_Or_Subprogram_Contract + (Directly_Designated_Type (Type_Id)); end if; end Analyze_Type_Contract; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0d62b04cc37..0de410a2392 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -5265,7 +5265,11 @@ package body Sem_Prag is -- Chain the pragma on the contract for further processing by -- Analyze_Pre_Post_Condition_In_Decl_Part. - Add_Contract_Item (N, Subp_Id); + if Ekind (Subp_Id) in Access_Subprogram_Kind then + Add_Contract_Item (N, Directly_Designated_Type (Subp_Id)); + else + Add_Contract_Item (N, Subp_Id); + end if; -- Fully analyze the pragma when it appears inside an entry or -- subprogram body because it cannot benefit from forward references.