From cff7b62c05a411a7dfb3af5e8feb63090c00df4a Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 14 Nov 2018 11:40:30 +0000 Subject: [PATCH] [Ada] Fix handling of generic actuals with default expression in SPARK 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. 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. From-SVN: r266112 --- gcc/ada/ChangeLog | 7 +++++++ gcc/ada/sem_ch12.adb | 3 +++ gcc/ada/sinfo.ads | 8 +++++--- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/generic_actuals.adb | 18 ++++++++++++++++++ 5 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/generic_actuals.adb diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8a42f4f..04caf7a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-11-14 Piotr Trojanek + + * sem_ch12.adb (Instantiate_Object): Set + Corresponding_Generic_Association on generic actuals with + default expression. + * sinfo.ads (Corresponding_Generic_Association): Update comment. + 2018-11-14 Hristian Kirtchev * exp_ch4.adb (Expand_Concatenate): Use the proper routine to diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 5e04895..f75c353 100644 --- a/gcc/ada/sem_ch12.adb +++ b/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); diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index fcf99a8..801bd21 100644 --- a/gcc/ada/sinfo.ads +++ b/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 diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 767da53..5536abd 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-11-14 Piotr Trojanek + + * gnat.dg/generic_actuals.adb: New testcase. + 2018-11-14 Richard Biener PR tree-optimization/87974 diff --git a/gcc/testsuite/gnat.dg/generic_actuals.adb b/gcc/testsuite/gnat.dg/generic_actuals.adb new file mode 100644 index 0000000..aa06395 --- /dev/null +++ b/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; -- 2.7.4