+ -- If the aggregate has box-initialized components, its type must be
+ -- frozen so that initialization procedures can properly be called
+ -- in the resolution that follows. The replacement of boxes with
+ -- initialization calls is properly an expansion activity but it must
+ -- be done during revolution.
+
+ if Expander_Active
+ and then Present (Component_Associations (N))
+ then
+ declare
+ Comp : Node_Id;
+
+ begin
+ Comp := First (Component_Associations (N));
+ while Present (Comp) loop
+ if Box_Present (Comp) then
+ Insert_Actions (N, Freeze_Entity (Typ, N));
+ exit;
+ end if;
+
+ Next (Comp);
+ end loop;
+ end;
+ end if;
+
+ -- An unqualified aggregate is restricted in SPARK to:
+
+ -- An aggregate item inside an aggregate for a multi-dimensional array
+
+ -- An expression being assigned to an unconstrained array, but only if
+ -- the aggregate specifies a value for OTHERS only.
+
+ if Nkind (Parent (N)) = N_Qualified_Expression then
+ if Is_Array_Type (Typ) then
+ Check_Qualified_Aggregate (Number_Dimensions (Typ), N);
+ else
+ Check_Qualified_Aggregate (1, N);
+ end if;
+ else
+ if Is_Array_Type (Typ)
+ and then Nkind (Parent (N)) = N_Assignment_Statement
+ and then not Is_Constrained (Etype (Name (Parent (N))))
+ then
+ if not Is_Others_Aggregate (N) then
+ Check_SPARK_Restriction
+ ("array aggregate should have only OTHERS", N);
+ end if;
+
+ elsif Is_Top_Level_Aggregate (N) then
+ Check_SPARK_Restriction ("aggregate should be qualified", N);
+
+ -- The legality of this unqualified aggregate is checked by calling
+ -- Check_Qualified_Aggregate from one of its enclosing aggregate,
+ -- unless one of these already causes an error to be issued.
+
+ else
+ null;
+ end if;
+ end if;
+