Frontend typically expands record aggregates to an N_Aggregate node with
Expressions field set to No_List; for example, in Step_8 of the
Sem_Aggr.Resolve_Record_Aggregate routine. In the GNATprove backend we
never traverse this field, but we have an assertion to confirm that the
Expressions field is indeed set to No_List.
However, record aggregates created in the Capture_Discriminants block of
the Sem_Aggr.Resolve_Record_Aggregate routine have their Expressions
field set to an empty list. This list is created by a call to New_List
but is never populated with any elements. Such an empty list is both
unnecessary and causes GNATprove to crash on its seemingly reasonable
assertion when processing this code:
procedure Test is
type Discriminated_Record (Discriminant : Boolean := False) is record
case Discriminant is
when True =>
Component : Integer;
when False =>
null;
end case;
end record;
type Enclosing_Record is record
DR : Discriminated_Record;
end record;
ER : Enclosing_Record := (others => <>);
-- The initialization expression is expanded into:
-- "(DR => (Discriminants => False))"
-- and the inner aggregate had Expressions set to an empty list.
begin
null;
end Test;
Also, this empty list seems to violate the description of N_Aggregate in
sinfo.ads, which says:
-- Expressions (List1) (set to No_List if none or null record case)
and then
-- In particular, for a record aggregate, the expressions
-- field will be set if there are positional associations.
Aggregates created in Resolve_Record_Aggregate have no positional
associations, so according to the above comments, their Expressions
field should be set to No_List.
This patch doesn't seem to affect the compiler, as apparently it
doesn't care whether the Expressions field is No_List or an empty list.
Tested on x86_64-pc-linux-gnu, committed on trunk
2020-06-05 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* sem_aggr.adb (Resolve_Record_Aggregate): Create the
N_Aggregate node with its Expressions field set to No_List and
not to an empty list.--- gcc/ada/sem_aggr.adb
+++ gcc/ada/sem_aggr.adb
@@ -147,9 +147,10 @@ package body Sem_Aggr is
--
-- Once this new Component_Association_List is built and all the semantic
-- checks performed, the original aggregate subtree is replaced with the
- -- new named record aggregate just built. Note that subtree substitution is
- -- performed with Rewrite so as to be able to retrieve the original
- -- aggregate.
+ -- new named record aggregate just built. This new record aggregate has no
+ -- positional associations, so its Expressions field is set to No_List.
+ -- Note that subtree substitution is performed with Rewrite so as to be
+ -- able to retrieve the original aggregate.
--
-- The aggregate subtree manipulation performed by Resolve_Record_Aggregate
-- yields the aggregate format expected by Gigi. Typically, this kind of
@@ -3990,7 +3991,7 @@ package body Sem_Aggr is
begin
if Is_Record_Type (T) and then Has_Discriminants (T) then
- New_Aggr := Make_Aggregate (Loc, New_List, New_List);
+ New_Aggr := Make_Aggregate (Loc, No_List, New_List);
Set_Etype (New_Aggr, T);
Add_Association
@@ -5043,7 +5044,7 @@ package body Sem_Aggr is
Expr : Node_Id;
begin
- Expr := Make_Aggregate (Loc, New_List, New_List);
+ Expr := Make_Aggregate (Loc, No_List, New_List);
Set_Etype (Expr, Ctyp);
-- If the enclosing type has discriminants, they have
