From patchwork Wed Aug 21 08:31:43 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: 1150699 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-507428-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="SaxDQJtP"; 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 46D1Bz45tRz9sBp for ; Wed, 21 Aug 2019 18:33:15 +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=Cl6NKc3zwWvsdMlb4KJL6Csa6hvUn+jjTBqBv9roO3HQwy+ahc VQT/Nw4YWzgbcz292O5X8ms8PyUI8MdM8bXcolIL3H+rpu0f0UhQBwOvoVzsUgvN Y5vLwZ27mSIZZFjqDb73o3/1hDtUe2EIQmcXpIr8YATQFqYaH9QsEgDNs= 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=t81TsPprXuCjK4T3CjbRaCpxMYo=; b=SaxDQJtPzhD7qKGmQQBP Ntaeikt/cOFebz8lm46vBJkr3KG62e8+nVFOHj/4YloikfZE1Oi1/j1K6cp4n4jc 2q5I+WrU+Z13XYnPQA+JpXtwoZeovFbGcwzl9XWzyTD/lAR2hdFNAxEkmfsZOV/K 17RyJvL8C2ybma4cVsy9MKU= Received: (qmail 96228 invoked by alias); 21 Aug 2019 08:31:51 -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 96175 invoked by uid 89); 21 Aug 2019 08:31:51 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.8 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy= X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 21 Aug 2019 08:31:49 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i0M1y-00012g-UQ for gcc-patches@gcc.gnu.org; Wed, 21 Aug 2019 04:31:48 -0400 Received: from rock.gnat.com ([205.232.38.15]:46181) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1i0M1y-000122-7Z for gcc-patches@gcc.gnu.org; Wed, 21 Aug 2019 04:31:46 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 596F21163FF; Wed, 21 Aug 2019 04:31:43 -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 M21g91y0ydQk; Wed, 21 Aug 2019 04:31:43 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 4868C1163EA; Wed, 21 Aug 2019 04:31:43 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 473EF646; Wed, 21 Aug 2019 04:31:43 -0400 (EDT) Date: Wed, 21 Aug 2019 04:31:43 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] More precise propagation of Size attribute in generic instances Message-ID: <20190821083143.GA71911@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 205.232.38.15 X-IsSubscribed: yes GNATprove analyzer for SPARK code depends on the frontend to accurately propagate the known value of Size attribute. This was not done for formal type parameters in generic instantiations. Now fixed. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-21 Yannick Moy gcc/ada/ * sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size field for formal type parameters in generic instantiations. --- gcc/ada/sem_ch3.adb +++ gcc/ada/sem_ch3.adb @@ -5555,6 +5555,14 @@ package body Sem_Ch3 is => Set_Ekind (Id, E_Record_Subtype); + -- Subtype declarations introduced for formal type parameters + -- in generic instantiations should inherit the Size value of + -- the type they rename. + + if Present (Generic_Parent_Type (N)) then + Set_RM_Size (Id, RM_Size (T)); + end if; + if Ekind (T) = E_Record_Subtype and then Present (Cloned_Subtype (T)) then