From: Ed Schonberg Date: Thu, 10 Oct 2019 15:23:56 +0000 (+0000) Subject: [Ada] Missing Predicated_Parent link on array Itype X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a096f12eae91f891ef17687a9c48fee3de0b2fdd;p=gcc.git [Ada] Missing Predicated_Parent link on array Itype 2019-10-10 Ed Schonberg 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1045a89632f..97e2dcfbd17 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,6 @@ -2019-10-10 Eric Botcazou +2019-10-10 Ed Schonberg - * 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 87fe050bb4c..3db998d5eda 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;