[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  <trojanek@adacore.com>

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8a42f4faea4cca53d239863cf0e229353f030a3d..04caf7a5a5eb6bbe96ce4b3cea74488c41847661 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-11-14  Piotr Trojanek  <trojanek@adacore.com>
+
+       * 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  <kirtchev@adacore.com>
 
        * 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 5e04895b57976294f8aad3d5eff707dd433482ab..f75c353b386e4658154ff9cc9bf8463935893c19 100644 (file)
--- 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 fcf99a8132b3254c7b51b0cc16244a8fe5ab9af8..801bd21fca7724d14f2e617173c125b3edb7885d 100644 (file)
--- 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 767da5380f71ddea834bc5d40b009f8566eeebe4..5536abd8401afb8bb4e10cb043c78f951913f7ca 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,7 @@
+2018-11-14  Piotr Trojanek  <trojanek@adacore.com>
+
+       * gnat.dg/generic_actuals.adb: New testcase.
+
 2018-11-14  Richard Biener  <rguenther@suse.de>
 
        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 (file)
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;