From patchwork Wed Nov 14 11:43:07 2018 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: 997625 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-489996-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="knYNKK8x"; 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 42w2gw2Bfyz9s3q for ; Wed, 14 Nov 2018 22:43:40 +1100 (AEDT) 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=WBLWNYvCaWW/qFTJe4r2kytLc4mnvOYT3Mmep4bXAQYwPMBLSE rKeFOwcb8huw+ovKNYgqoHF55gM970J/pTV+pZDFWUQ+GDvB7XCTQfDAKRQE1urR sTvm6vpaJyYGJZBfiIQ/1UKa/ah0H68vgrnDc1qgO30LqkYX2YLRVPQkw= 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=CelRpGFmAmGQOH13fXn2XoeGPYY=; b=knYNKK8xPMd4JIXlgOdX EvYykSX4BKacWgQQKdaT/t/khVuLv6j/QLozAfjfVQ7vOq9IKbOkqHpAQfDPlPr6 1x0UC6T+xdINie++Cisvu7xssJdzK2PPLCV6Q5p8U5Ycv/OsZAF1RUowyBlwI9o0 8fCwTSjEIUFqiBdkOPWreR4= Received: (qmail 38329 invoked by alias); 14 Nov 2018 11:43:11 -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 38228 invoked by uid 89); 14 Nov 2018 11:43:10 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=Expression, appearing, queries, contract 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; Wed, 14 Nov 2018 11:43:09 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id AA38556158; Wed, 14 Nov 2018 06:43:07 -0500 (EST) 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 OrBwlwoQA-m9; Wed, 14 Nov 2018 06:43:07 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 971E1560C3; Wed, 14 Nov 2018 06:43:07 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id 9340C353A; Wed, 14 Nov 2018 06:43:07 -0500 (EST) Date: Wed, 14 Nov 2018 06:43:07 -0500 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [Ada] Fix handling of generic actuals with default expression in SPARK Message-ID: <20181114114307.GA73861@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes Both in the GNAT frontend and in the GNATprove backend we have several checks related to generic actuals of mode IN that rely on the Corresponding_Generic_Association flag. However, this flag was only set for actuals with explicit expressions from the generic instance and unset for actuals with implicit expressions from the generic unit. For example, the code from the added testcase was wrongly rejected with a message that Y (which is an actual with a default expression) cannot appear in the Initializes contract. Now this code is accepted. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-11-14 Piotr Trojanek gcc/ada/ * sem_ch12.adb (Instantiate_Object): Set Corresponding_Generic_Association on generic actuals with default expression. * sinfo.ads (Corresponding_Generic_Association): Update comment. gcc/testsuite/ * gnat.dg/generic_actuals.adb: New testcase. --- gcc/ada/sem_ch12.adb +++ gcc/ada/sem_ch12.adb @@ -11097,6 +11097,9 @@ package body Sem_Ch12 is Expression => New_Copy_Tree (Default_Expression (Formal))); + Set_Corresponding_Generic_Association + (Decl_Node, Expression (Decl_Node)); + Append (Decl_Node, List); Set_Analyzed (Expression (Decl_Node), False); --- gcc/ada/sinfo.ads +++ gcc/ada/sinfo.ads @@ -1106,9 +1106,11 @@ package Sinfo is -- Corresponding_Generic_Association (Node5-Sem) -- This field is defined for object declarations and object renaming -- declarations. It is set for the declarations within an instance that - -- map generic formals to their actuals. If set, the field points to - -- a generic_association which is the original parent of the expression - -- or name appearing in the declaration. This simplifies ASIS queries. + -- map generic formals to their actuals. If set, the field points either + -- to a copy of a default expression for an actual of mode IN or to a + -- generic_association which is the original parent of the expression or + -- name appearing in the declaration. This simplifies ASIS and GNATprove + -- queries. -- Corresponding_Integer_Value (Uint4-Sem) -- This field is set in real literals of fixed-point types (it is not --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/generic_actuals.adb @@ -0,0 +1,18 @@ +-- { dg-do compile } +-- { dg-options "-gnatd.F" } + +procedure Generic_Actuals with SPARK_Mode is + generic + X : Integer; + Y : Integer := 0; + package Q with Initializes => (XX => X, YY => Y) is + -- Both X and Y actuals can appear in the Initializes contract, + -- i.e. the default expression of Y should not matter. + XX : Integer := X; + YY : Integer := Y; + end Q; + + package Inst is new Q (X => 0); +begin + null; +end Generic_Actuals;