diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_aggr.adb | 9 |
2 files changed, 13 insertions, 5 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1045a89..97e2dcf 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,6 @@ -2019-10-10 Eric Botcazou <ebotcazou@adacore.com> +2019-10-10 Ed Schonberg <schonberg@adacore.com> - * sem_ch3.adb (Analyze_Number_Declaration): Set - Debug_Info_Needed in the case where the expression is an integer - literal.
\ No newline at end of file + * 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.
\ No newline at end of file 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; |