[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
This commit is contained in:
Ed Schonberg
2019-10-10 15:23:56 +00:00
committed by Pierre-Marie de Rodat
parent f200341cf8
commit a096f12eae
2 changed files with 13 additions and 5 deletions

View File

@@ -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.
* 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.

View File

@@ -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;