[Ada] Fix handling of generic actuals with default expression in SPARK
authorPiotr Trojanek <trojanek@adacore.com>
Wed, 14 Nov 2018 11:40:30 +0000 (11:40 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Wed, 14 Nov 2018 11:40:30 +0000 (11:40 +0000)
commitcff7b62c05a411a7dfb3af5e8feb63090c00df4a
tree81e4bda4269aa6dcd79bf70c63cb741687040ded
parent923ecd0e4b472073e2794ad2cb272880c3c9e937
[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
gcc/ada/ChangeLog
gcc/ada/sem_ch12.adb
gcc/ada/sinfo.ads
gcc/testsuite/ChangeLog
gcc/testsuite/gnat.dg/generic_actuals.adb [new file with mode: 0644]