[Ada] Do not create an empty list of nodes that confuses GNATprove

Message ID 20200605122338.GA56735@adacore.com
State New
Headers show
Series
  • [Ada] Do not create an empty list of nodes that confuses GNATprove
Related show

Commit Message

Pierre-Marie de Rodat June 5, 2020, 12:23 p.m.
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  <trojanek@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.

Patch

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