diff options
| author | Ed Schonberg <schonberg@adacore.com> | 2019-10-10 15:23:56 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-10-10 15:23:56 +0000 |
| commit | a096f12eae91f891ef17687a9c48fee3de0b2fdd (patch) | |
| tree | fa07887467d2770a26ea553883896361a1770ad6 /gcc/ada/sem_aggr.adb | |
| parent | f200341cf868478ffea9626d97ab280d1cad08e7 (diff) | |
| download | gcc-a096f12eae91f891ef17687a9c48fee3de0b2fdd.zip gcc-a096f12eae91f891ef17687a9c48fee3de0b2fdd.tar.gz gcc-a096f12eae91f891ef17687a9c48fee3de0b2fdd.tar.bz2 | |
[Ada] Missing Predicated_Parent link on array Itype
2019-10-10 Ed Schonberg <schonberg@adacore.com>
gcc/ada/
* sem_aggr.adb (Resolve_Array_Aggregate): Set properly the
Predicated_Parent link of an itype created for an aggregate, so
that the predicate_function of the parent can support proofs on
the object that it initializes.
From-SVN: r276823
Diffstat (limited to 'gcc/ada/sem_aggr.adb')
| -rw-r--r-- | gcc/ada/sem_aggr.adb | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 87fe050..3db998d 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -614,10 +614,17 @@ package body Sem_Aggr is if Has_Predicates (Typ) then Set_Has_Predicates (Itype); + -- If the base type has a predicate, capture the predicated parent + -- or the existing predicate function for SPARK use. + if Present (Predicate_Function (Typ)) then Set_Predicate_Function (Itype, Predicate_Function (Typ)); - else + + elsif Is_Itype (Typ) then Set_Predicated_Parent (Itype, Predicated_Parent (Typ)); + + else + Set_Predicated_Parent (Itype, Typ); end if; end if; |