From patchwork Tue Aug 20 09:51:29 2019 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: 1150002 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-507357-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="PZtsCIz3"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 46CR3n2P2Nz9s4Y for ; Tue, 20 Aug 2019 19:55:01 +1000 (AEST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=oZRNdiP5VRi3/k6OOFimLW5nbhjkzwsIhXtEoVTIVjWOcICALn npTzaPaYu0cxbga2oorOYjxaMidSpc4liNosHNL5nXnWR5ejYA6CnBnXQ7+tQ/w0 3WJQud6DkyXBlxnfwiMts+DNEjqYumJnaK0MjAVmT95hcTRF/weelE/hk= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=ZiuhlTmGwgX8lMGEAAteOf+SczQ=; b=PZtsCIz3io+ZfQYWPfrE 1Ordl5LVV4WFB/eKfDRk/6G8Nyoa9eFd6YLII5qTQiEAmnvbiCxSgcOhuFUkh6U9 ZpMabCMmPiJKrar87Gxb7+q2Pk+JyWe54P29SBuNN8Zpyq7qLaskg4nwmDxXU7FR ATI2Tb2Q/TXDf0ZPyJuIMXk= Received: (qmail 123482 invoked by alias); 20 Aug 2019 09:51:42 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 122320 invoked by uid 89); 20 Aug 2019 09:51:32 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.1 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.1 spammy= X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Tue, 20 Aug 2019 09:51:30 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id C4E25560C4; Tue, 20 Aug 2019 05:51:29 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id JyL2BZXdXSsh; Tue, 20 Aug 2019 05:51:29 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id B38B8560BB; Tue, 20 Aug 2019 05:51:29 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id B2A7D63E; Tue, 20 Aug 2019 05:51:29 -0400 (EDT) Date: Tue, 20 Aug 2019 05:51:29 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Adapt GNATprove expansion for slices with access prefix Message-ID: <20190820095129.GA75602@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes The special expansion done in GNATprove mode should be adapted to slices where the prefix has access type, like indexed expressions. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-20 Yannick Moy gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Slice_Or_Indexed_Component): Renaming of function to apply to slices as well. (Expand_SPARK): Expand prefix of slices of access type. --- gcc/ada/exp_spark.adb +++ gcc/ada/exp_spark.adb @@ -59,9 +59,6 @@ package body Exp_SPARK is procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id); -- Build the DIC procedure of a type when needed, if not already done - procedure Expand_SPARK_N_Indexed_Component (N : Node_Id); - -- Insert explicit dereference if required - procedure Expand_SPARK_N_Loop_Statement (N : Node_Id); -- Perform loop statement-specific expansion @@ -77,6 +74,9 @@ package body Exp_SPARK is procedure Expand_SPARK_N_Selected_Component (N : Node_Id); -- Insert explicit dereference if required + procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id); + -- Insert explicit dereference if required + ------------------ -- Expand_SPARK -- ------------------ @@ -138,8 +138,10 @@ package body Exp_SPARK is Expand_SPARK_N_Freeze_Type (Entity (N)); end if; - when N_Indexed_Component => - Expand_SPARK_N_Indexed_Component (N); + when N_Indexed_Component + | N_Slice + => + Expand_SPARK_N_Slice_Or_Indexed_Component (N); when N_Selected_Component => Expand_SPARK_N_Selected_Component (N); @@ -326,21 +328,6 @@ package body Exp_SPARK is end if; end Expand_SPARK_N_Loop_Statement; - -------------------------------------- - -- Expand_SPARK_N_Indexed_Component -- - -------------------------------------- - - procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is - Pref : constant Node_Id := Prefix (N); - Typ : constant Entity_Id := Etype (Pref); - - begin - if Is_Access_Type (Typ) then - Insert_Explicit_Dereference (Pref); - Analyze_And_Resolve (Pref, Designated_Type (Typ)); - end if; - end Expand_SPARK_N_Indexed_Component; - --------------------------------------- -- Expand_SPARK_N_Object_Declaration -- --------------------------------------- @@ -552,4 +539,19 @@ package body Exp_SPARK is end if; end Expand_SPARK_N_Selected_Component; + ----------------------------------------------- + -- Expand_SPARK_N_Slice_Or_Indexed_Component -- + ----------------------------------------------- + + procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id) is + Pref : constant Node_Id := Prefix (N); + Typ : constant Entity_Id := Etype (Pref); + + begin + if Is_Access_Type (Typ) then + Insert_Explicit_Dereference (Pref); + Analyze_And_Resolve (Pref, Designated_Type (Typ)); + end if; + end Expand_SPARK_N_Slice_Or_Indexed_Component; + end Exp_SPARK;