From patchwork Mon May 16 08:42:57 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: 54001 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 5CBDC3858C56 for ; Mon, 16 May 2022 08:45:33 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 5CBDC3858C56 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1652690733; bh=hq4zakcr8XWed7dLKLlY4oCSTDzaEPZghG0y4eeJ5Mg=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=Js+PyzGbQCooPf1Tx7RdB8lBpQd/DNU1kIuNo237q8Xgs847+CWUGZ1dxneIGFR9D NWvSOT9nnqIVSeIXXvn6IZsc1jFTl/jntimQr0caTENkETOSgIetllkrptgTYj0y58 dqIk68tsk8dUKNFBL+BoCuagZ0wDlaYw17YY/MFg= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) by sourceware.org (Postfix) with ESMTPS id E441A3857C4E for ; Mon, 16 May 2022 08:42:59 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org E441A3857C4E Received: by mail-wr1-x433.google.com with SMTP id d21so3555050wra.10 for ; Mon, 16 May 2022 01:42:59 -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=hq4zakcr8XWed7dLKLlY4oCSTDzaEPZghG0y4eeJ5Mg=; b=Ib0RaQ7hpSSeNjtTWBeDdVMThJsrJoVjQ++/LVZJ4AmO+IkQVMQqVAxO6a+2mh/FnM MKoNPeTkEdqX4+T7G1utvGKfcHEIJtzSgLtvgq7WRjyA/+b2iwRZQGjNaIddOe34Er80 0vcgyUglfFb0zhHNoM5mnVYJogiu/zDNo1N4XgNtpryJ7sI1nUPYcKqiD0r7lN02+3yn 6y8kdEwMEmLEh9WFchlPxbQrGeSknKt843wD8NFgpgX7J3mC8Tx1uxMfHfxjy9ieJiLC ruft4tFA4bbIlYR59Kjpm9NxP4/NIg45EQ1XvC1vl82yKWT4td95u2Yu6FYy21h48Ulh Rudg== X-Gm-Message-State: AOAM53266DhK7TjpgrmXKBQz08mqqsB4JDYQd0O8pb+OLF+15dXdXFrH VHbfi7kR8xfJbNp1fKQytYKnnHpDPL2QhQ== X-Google-Smtp-Source: ABdhPJw5dhvfCDM6/K7e1+7oyJeHHHUB68CO/e6GDDcRN0w+1lpoGP6amoO+vYP3sCLpmQJXk6zepQ== X-Received: by 2002:a5d:64ec:0:b0:20c:62d4:3917 with SMTP id g12-20020a5d64ec000000b0020c62d43917mr12744031wri.480.1652690578163; Mon, 16 May 2022 01:42:58 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id y11-20020adfc7cb000000b0020cf41017b4sm8204519wrg.19.2022.05.16.01.42.57 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 16 May 2022 01:42:57 -0700 (PDT) Date: Mon, 16 May 2022 08:42:57 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Pick volatile refinement property of a subtype from its base type Message-ID: <20220516084257.GA3843363@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-13.2 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Piotr Trojanek Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" Volatile refinement properties (e.g. Async_Writers), which refine the Volatile aspect in SPARK, are inherited by subtypes from their base types. In particular, this patch fixes handling of those properties for subtypes of private types. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.adb (Type_Or_Variable_Has_Enabled_Property): Given a subtype recurse into its base type. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12683,7 +12683,8 @@ package body Sem_Util is then return False; - -- For a private type, may need to look at the full view + -- For a private type (including subtype of a private types), look at + -- the full view. elsif Is_Private_Type (Item_Id) and then Present (Full_View (Item_Id)) then @@ -12696,6 +12697,13 @@ package body Sem_Util is return Type_Or_Variable_Has_Enabled_Property (First_Subtype (Etype (Base_Type (Item_Id)))); + -- For a subtype, the property will be inherited from its base type. + + elsif Is_Type (Item_Id) + and then not Is_Base_Type (Item_Id) + then + return Type_Or_Variable_Has_Enabled_Property (Etype (Item_Id)); + -- If not specified explicitly for an object and its type -- is effectively volatile, then take result from the type.