[Ada] Support aspect Relaxed_Initialization and attribute Initialized

2020-06-15  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* aspects.ads (Aspect_Id): Add Aspect_Relaxed_Initialization.
	(Implementation_Defined_Aspect): Add new aspect.
	(Aspect_Argument): Add new aspect with Optional_Expression
	argument.
	(Is_Representation_Aspect): Add new aspect as a
	non-representation one.
	(Aspect_Names): Add name for the new aspect.
	(Aspect_Delay): Add new aspect as a non-delayed one.
	* sem_ch3.adb: Minor reformatting.
	* einfo.ads, einfo.adb (Is_Relaxed_Initialization_State): New
	query; reuses existing code for querying abstract state options.
	* exp_attr.adb (Expand_N_Attribute_Reference): For now ignore
	attribute 'Initialized.
	* sem_attr.adb (Analyze_Attribute_Old_Result): Allow attribute
	'Result to be used in the aspect Relaxed_Initialization
	expression.
	(Analyze_Attribute): Analyze attribute 'Initialized; based on
	existing code for attribute 'Valid_Scalars.
	(Eval_Attribute): Do not expect attribute 'Initialized, just
	like attribute 'Valid_Scalars is not expected.
	* sem_ch13.adb (Analyze_Aspect_Relaxed_Initialization): New
	routine.
	(Analyze_Aspect_Specifications): Analyze new aspect in a
	dedicated routine.
	(Check_Aspect_At_Freeze_Point): Do not expect new aspect.
	* sem_prag.adb (Analyze_Abstract_State): Support option
	Relaxed_Initialization on abstract states.
	* sem_util.ads, sem_util.adb (Has_Relaxed_Initialization): New
	query for the GNATprove backend.
	* snames.ads-tmpl (Snames): Add Name_Ids for the new aspect and
	attribute; add an Attribute_Id for the new attribute.

11 files changed, 402 insertions, 11 deletions

diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 82bf5ca..383a528 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -138,6 +138,7 @@ package Aspects is
       Aspect_Refined_Post,                  -- GNAT
       Aspect_Refined_State,                 -- GNAT
       Aspect_Relative_Deadline,
+      Aspect_Relaxed_Initialization,        -- GNAT
       Aspect_Scalar_Storage_Order,          -- GNAT
       Aspect_Secondary_Stack_Size,          -- GNAT
       Aspect_Simple_Storage_Pool,           -- GNAT
@@ -261,6 +262,7 @@ package Aspects is
       Aspect_Persistent_BSS             => True,
       Aspect_Predicate                  => True,
       Aspect_Pure_Function              => True,
+      Aspect_Relaxed_Initialization     => True,
       Aspect_Remote_Access_Type         => True,
       Aspect_Scalar_Storage_Order       => True,
       Aspect_Secondary_Stack_Size       => True,
@@ -400,6 +402,7 @@ package Aspects is
       Aspect_Refined_Post               => Expression,
       Aspect_Refined_State              => Expression,
       Aspect_Relative_Deadline          => Expression,
+      Aspect_Relaxed_Initialization     => Optional_Expression,
       Aspect_Scalar_Storage_Order       => Expression,
       Aspect_Secondary_Stack_Size       => Expression,
       Aspect_Simple_Storage_Pool        => Name,
@@ -493,6 +496,7 @@ package Aspects is
       Aspect_Refined_Post                 => False,
       Aspect_Refined_State                => False,
       Aspect_Relative_Deadline            => False,
+      Aspect_Relaxed_Initialization       => False,
       Aspect_Scalar_Storage_Order         => True,
       Aspect_Secondary_Stack_Size         => True,
       Aspect_Simple_Storage_Pool          => True,
@@ -651,6 +655,7 @@ package Aspects is
       Aspect_Refined_Post                 => Name_Refined_Post,
       Aspect_Refined_State                => Name_Refined_State,
       Aspect_Relative_Deadline            => Name_Relative_Deadline,
+      Aspect_Relaxed_Initialization       => Name_Relaxed_Initialization,
       Aspect_Remote_Access_Type           => Name_Remote_Access_Type,
       Aspect_Remote_Call_Interface        => Name_Remote_Call_Interface,
       Aspect_Remote_Types                 => Name_Remote_Types,
@@ -912,6 +917,7 @@ package Aspects is
       Aspect_Refined_Global               => Never_Delay,
       Aspect_Refined_Post                 => Never_Delay,
       Aspect_Refined_State                => Never_Delay,
+      Aspect_Relaxed_Initialization       => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 2456fc1..eb6ae17 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -8249,6 +8249,21 @@ package body Einfo is
           and then Is_Protected_Type (Corresponding_Concurrent_Type (Id));
    end Is_Protected_Record_Type;
 
+   -------------------------------------
+   -- Is_Relaxed_Initialization_State --
+   -------------------------------------
+
+   function Is_Relaxed_Initialization_State (Id : E) return B is
+   begin
+      --  To qualify, the abstract state must appear with simple option
+      --  "Relaxed_Initialization" (??? add reference to SPARK RM once the
+      --  Relaxed_Initialization aspect is described there).
+
+      return
+        Ekind (Id) = E_Abstract_State
+          and then Has_Option (Id, Name_Relaxed_Initialization);
+   end Is_Relaxed_Initialization_State;
+
    --------------------------------
    -- Is_Standard_Character_Type --
    --------------------------------
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index a1cfd7d..346a15e 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3184,6 +3184,10 @@ package Einfo is
 --       Applies to all entities, true for record types and subtypes,
 --       includes class-wide types and subtypes (which are also records).
 
+--    Is_Relaxed_Initialization_State (synthesized)
+--       Applies to all entities, true for abstract states that are subject to
+--       option Relaxed_Initialization.
+
 --    Is_Remote_Call_Interface (Flag62)
 --       Defined in all entities. Set in E_Package and E_Generic_Package
 --       entities to which a pragma Remote_Call_Interface is applied, and
@@ -5832,6 +5836,7 @@ package Einfo is
    --    Has_Null_Visible_Refinement         (synth)
    --    Is_External_State                   (synth)
    --    Is_Null_State                       (synth)
+   --    Is_Relaxed_Initialization_State     (synth)
    --    Is_Synchronized_State               (synth)
    --    Partial_Refinement_Constituents     (synth)
 
@@ -7669,6 +7674,7 @@ package Einfo is
    function Is_Protected_Component              (Id : E) return B;
    function Is_Protected_Interface              (Id : E) return B;
    function Is_Protected_Record_Type            (Id : E) return B;
+   function Is_Relaxed_Initialization_State     (Id : E) return B;
    function Is_Standard_Character_Type          (Id : E) return B;
    function Is_Standard_String_Type             (Id : E) return B;
    function Is_String_Type                      (Id : E) return B;
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 182ce15..08bea2b5 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -3737,6 +3737,25 @@ package body Exp_Attr is
       when Attribute_Img =>
          Exp_Imgv.Expand_Image_Attribute (N);
 
+      -----------------
+      -- Initialized --
+      -----------------
+
+      --  For execution, we could either implement an approximation of this
+      --  aspect, or use Valid_Scalars as a first approximation. For now we do
+      --  the latter.
+
+      when Attribute_Initialized =>
+         Rewrite
+           (N,
+            Make_Attribute_Reference
+              (Sloc           => Loc,
+               Prefix         => Pref,
+               Attribute_Name => Name_Valid_Scalars,
+               Expressions    => Exprs));
+
+         Analyze_And_Resolve (N);
+
       -----------
       -- Input --
       -----------
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 801c445..2bb24a2 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1324,6 +1324,15 @@ package body Sem_Attr is
             then
                null;
 
+            --  Attribute 'Result is allowed to appear in aspect
+            --  Relaxed_Initialization (??? add reference to SPARK RM once this
+            --  attribute is described there).
+
+            elsif Prag_Nam = Name_Relaxed_Initialization
+              and then Aname = Name_Result
+            then
+               null;
+
             elsif Nam_In (Prag_Nam, Name_Post,
                                     Name_Post_Class,
                                     Name_Postcondition,
@@ -4146,6 +4155,26 @@ package body Sem_Attr is
       when Attribute_Img =>
          Analyze_Image_Attribute (Standard_String);
 
+      -----------------
+      -- Initialized --
+      -----------------
+
+      when Attribute_Initialized =>
+         Check_E0;
+
+         if Comes_From_Source (N) then
+
+            --  A similar attribute Valid_Scalars can be prefixed with
+            --  references to both functions and objects, but this attribute
+            --  can be only prefixed with references to objects.
+
+            if not Is_Object_Reference (P) then
+               Error_Attr_P ("prefix of % attribute must be object");
+            end if;
+         end if;
+
+         Set_Etype (N, Standard_Boolean);
+
       -----------
       -- Input --
       -----------
@@ -10231,6 +10260,7 @@ package body Sem_Attr is
          | Attribute_First_Bit
          | Attribute_Img
          | Attribute_Input
+         | Attribute_Initialized
          | Attribute_Last_Bit
          | Attribute_Library_Level
          | Attribute_Maximum_Alignment
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 0f23cbb..503fd15 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1708,6 +1708,9 @@ package body Sem_Ch13 is
             procedure Analyze_Aspect_Implicit_Dereference;
             --  Perform analysis of the Implicit_Dereference aspects
 
+            procedure Analyze_Aspect_Relaxed_Initialization;
+            --  Perform analysis of aspect Relaxed_Initialization
+
             procedure Make_Aitem_Pragma
               (Pragma_Argument_Associations : List_Id;
                Pragma_Name                  : Name_Id);
@@ -2040,6 +2043,179 @@ package body Sem_Ch13 is
 
             end Analyze_Aspect_Implicit_Dereference;
 
+            -------------------------------------------
+            -- Analyze_Aspect_Relaxed_Initialization --
+            -------------------------------------------
+
+            procedure Analyze_Aspect_Relaxed_Initialization is
+               procedure Analyze_Relaxed_Parameter
+                 (Subp_Id : Entity_Id;
+                  Param   : Node_Id;
+                  Seen    : in out Elist_Id);
+               --  Analyze parameter that appears in the expression of the
+               --  aspect Relaxed_Initialization.
+
+               -------------------------------
+               -- Analyze_Relaxed_Parameter --
+               -------------------------------
+
+               procedure Analyze_Relaxed_Parameter
+                 (Subp_Id : Entity_Id;
+                  Param   : Node_Id;
+                  Seen    : in out Elist_Id)
+               is
+               begin
+                  --  The relaxed parameter is a formal parameter
+
+                  if Nkind_In (Param, N_Identifier, N_Expanded_Name) then
+                     Analyze (Param);
+
+                     declare
+                        Item : constant Entity_Id := Entity (Param);
+                     begin
+                        --  It must be a formal of the analyzed subprogram
+
+                        if Scope (Item) = Subp_Id then
+
+                           pragma Assert (Is_Formal (Item));
+
+                           --  Detect duplicated items
+
+                           if Contains (Seen, Item) then
+                              Error_Msg_N ("duplicate aspect % item", Param);
+                           else
+                              Append_New_Elmt (Item, Seen);
+                           end if;
+                        else
+                           Error_Msg_N ("illegal aspect % item", Param);
+                        end if;
+                     end;
+
+                  --  The relaxed parameter is the function's Result attribute
+
+                  elsif Is_Attribute_Result (Param) then
+                     Analyze (Param);
+
+                     declare
+                        Pref : constant Node_Id := Prefix (Param);
+                     begin
+                        if Present (Pref)
+                          and then
+                            Nkind_In (Pref, N_Identifier, N_Expanded_Name)
+                          and then
+                            Entity (Pref) = Subp_Id
+                        then
+                           --  Detect duplicated items
+
+                           if Contains (Seen, Subp_Id) then
+                              Error_Msg_N ("duplicate aspect % item", Param);
+                           else
+                              Append_New_Elmt (Entity (Pref), Seen);
+                           end if;
+
+                        else
+                           Error_Msg_N ("illegal aspect % item", Param);
+                        end if;
+                     end;
+                  else
+                     Error_Msg_N ("illegal aspect % item", Param);
+                  end if;
+               end Analyze_Relaxed_Parameter;
+
+               --  Local variables
+
+               Seen : Elist_Id := No_Elist;
+               --  Items that appear in the relaxed initialization aspect
+               --  expression of a subprogram; for detecting duplicates.
+
+            --  Start of processing for Analyze_Aspect_Relaxed_Initialization
+
+            begin
+               --  Set name of the aspect for error messages
+               Error_Msg_Name_1 := Nam;
+
+               --  Annotation of a type; no aspect expression is allowed
+               --  ??? Once the exact rule for this aspect is ready, we will
+               --  likely reject concurrent types, etc., so let's keep the code
+               --  for types and variable separate.
+
+               if Is_First_Subtype (E) then
+                  if Present (Expr) then
+                     Error_Msg_N ("illegal aspect % expression", Expr);
+                  end if;
+
+               --  Annotation of a variable; no aspect expression is allowed
+
+               elsif Ekind (E) = E_Variable then
+                  if Present (Expr) then
+                     Error_Msg_N ("illegal aspect % expression", Expr);
+                  end if;
+
+               --  Annotation of a subprogram; aspect expression is required
+
+               elsif Is_Subprogram (E) then
+                  if Present (Expr) then
+
+                     --  Subprogram and its formal parameters must be visible
+                     --  when analyzing the aspect expression.
+
+                     pragma Assert (not In_Open_Scopes (E));
+
+                     Push_Scope (E);
+
+                     if Is_Generic_Subprogram (E) then
+                        Install_Generic_Formals (E);
+                     else
+                        Install_Formals (E);
+                     end if;
+
+                     --  Aspect expression is either an aggregate with list of
+                     --  parameters (and possibly the Result attribute for a
+                     --  function).
+
+                     if Nkind (Expr) = N_Aggregate then
+
+                        --  Component associations are not allowed in the
+                        --  aspect expression aggregate.
+
+                        if Present (Component_Associations (Expr)) then
+                           Error_Msg_N ("illegal aspect % expression", Expr);
+                        else
+                           declare
+                              Param : Node_Id := First (Expressions (Expr));
+
+                           begin
+                              while Present (Param) loop
+                                 Analyze_Relaxed_Parameter (E, Param, Seen);
+                                 Next (Param);
+                              end loop;
+                           end;
+                        end if;
+
+                        --  Mark the aggregate expression itself as analyzed;
+                        --  its subexpressions were marked when they themselves
+                        --  were analyzed.
+
+                        Set_Analyzed (Expr);
+
+                     --  Otherwise, it is a single name of a subprogram
+                     --  parameter (or possibly the Result attribute for
+                     --  a function).
+
+                     else
+                        Analyze_Relaxed_Parameter (E, Expr, Seen);
+                     end if;
+
+                     End_Scope;
+                  else
+                     Error_Msg_N ("missing expression for aspect %", N);
+                  end if;
+
+               else
+                  Error_Msg_N ("inappropriate entity for aspect %", E);
+               end if;
+            end Analyze_Aspect_Relaxed_Initialization;
+
             -----------------------
             -- Make_Aitem_Pragma --
             -----------------------
@@ -3332,6 +3508,12 @@ package body Sem_Ch13 is
                      end;
                   end if;
 
+               --  Relaxed_Initialization
+
+               when Aspect_Relaxed_Initialization =>
+                  Analyze_Aspect_Relaxed_Initialization;
+                  goto Continue;
+
                --  Secondary_Stack_Size
 
                --  Aspect Secondary_Stack_Size needs to be converted into a
@@ -9942,6 +10124,7 @@ package body Sem_Ch13 is
             | Aspect_Refined_Global
             | Aspect_Refined_Post
             | Aspect_Refined_State
+            | Aspect_Relaxed_Initialization
             | Aspect_SPARK_Mode
             | Aspect_Test_Case
             | Aspect_Unimplemented
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 2e9a3d0..2431b26 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2814,7 +2814,7 @@ package body Sem_Ch3 is
       if Present (L) then
          Context := Parent (L);
 
-         --  Certain contract annocations have forward visibility semantics and
+         --  Certain contract annotations have forward visibility semantics and
          --  must be analyzed after all declarative items have been processed.
          --  This timing ensures that entities referenced by such contracts are
          --  visible.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a7356c7..2b63617 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -11798,7 +11798,7 @@ package body Sem_Prag is
          --    SIMPLE_OPTION
          --  | NAME_VALUE_OPTION
 
-         --  SIMPLE_OPTION ::= Ghost | Synchronous
+         --  SIMPLE_OPTION ::= Ghost | Relaxed_Initialization | Synchronous
 
          --  NAME_VALUE_OPTION ::=
          --    Part_Of => ABSTRACT_STATE
@@ -11868,15 +11868,16 @@ package body Sem_Prag is
             is
                --  Flags used to verify the consistency of options
 
-               AR_Seen          : Boolean := False;
-               AW_Seen          : Boolean := False;
-               ER_Seen          : Boolean := False;
-               EW_Seen          : Boolean := False;
-               External_Seen    : Boolean := False;
-               Ghost_Seen       : Boolean := False;
-               Others_Seen      : Boolean := False;
-               Part_Of_Seen     : Boolean := False;
-               Synchronous_Seen : Boolean := False;
+               AR_Seen                     : Boolean := False;
+               AW_Seen                     : Boolean := False;
+               ER_Seen                     : Boolean := False;
+               EW_Seen                     : Boolean := False;
+               External_Seen               : Boolean := False;
+               Ghost_Seen                  : Boolean := False;
+               Others_Seen                 : Boolean := False;
+               Part_Of_Seen                : Boolean := False;
+               Relaxed_Initialization_Seen : Boolean := False;
+               Synchronous_Seen            : Boolean := False;
 
                --  Flags used to store the static value of all external states'
                --  expressions.
@@ -12357,6 +12358,12 @@ package body Sem_Prag is
                            Check_Duplicate_Option (Opt, Synchronous_Seen);
                            Check_Ghost_Synchronous;
 
+                        --  Relaxed_Initialization
+
+                        elsif Chars (Opt) = Name_Relaxed_Initialization then
+                           Check_Duplicate_Option
+                             (Opt, Relaxed_Initialization_Seen);
+
                         --  Option Part_Of without an encapsulating state is
                         --  illegal (SPARK RM 7.1.4(8)).
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index a1bf0ae..9f97f7d 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12424,6 +12424,123 @@ package body Sem_Util is
       end if;
    end Has_Private_Component;
 
+   --------------------------------
+   -- Has_Relaxed_Initialization --
+   --------------------------------
+
+   function Has_Relaxed_Initialization (E : Entity_Id) return Boolean is
+
+      function Denotes_Relaxed_Parameter
+        (Expr  : Node_Id;
+         Param : Entity_Id)
+         return Boolean;
+      --  Returns True iff expression Expr denotes a formal parameter or
+      --  function Param (through its attribute Result).
+
+      -------------------------------
+      -- Denotes_Relaxed_Parameter --
+      -------------------------------
+
+      function Denotes_Relaxed_Parameter
+        (Expr  : Node_Id;
+         Param : Entity_Id)
+         return Boolean
+      is
+      begin
+         if Nkind_In (Expr, N_Identifier, N_Expanded_Name) then
+            return Entity (Expr) = Param;
+         else
+            pragma Assert (Is_Attribute_Result (Expr));
+            return Entity (Prefix (Expr)) = Param;
+         end if;
+      end Denotes_Relaxed_Parameter;
+
+   --  Start of processing for Has_Relaxed_Initialization
+
+   begin
+      --  When analyzing, we checked all syntax legality rules for the aspect
+      --  Relaxed_Initialization, but didn't store the property anywhere (e.g.
+      --  as an Einfo flag). To query the property we look directly at the AST,
+      --  but now without any syntactic checks.
+
+      case Ekind (E) is
+         --  Abstract states have option Relaxed_Initialization
+
+         when E_Abstract_State =>
+            return Is_Relaxed_Initialization_State (E);
+
+         --  Variables have this aspect attached directly
+
+         when E_Variable =>
+            return Has_Aspect (E, Aspect_Relaxed_Initialization);
+
+         --  Types have this aspect attached directly (though we only allow it
+         --  to be specified for the first subtype).
+
+         when Type_Kind =>
+            pragma Assert (Is_First_Subtype (E));
+            return Has_Aspect (E, Aspect_Relaxed_Initialization);
+
+         --  Formal parameters and functions have the Relaxed_Initialization
+         --  aspect attached to the subprogram entity and must be listed in
+         --  the aspect expression.
+
+         when Formal_Kind
+            | E_Function
+         =>
+            declare
+               Subp_Id     : Entity_Id;
+               Aspect_Expr : Node_Id;
+               Param_Expr  : Node_Id;
+
+            begin
+               if Is_Formal (E) then
+                  Subp_Id := Scope (E);
+               else
+                  Subp_Id := E;
+               end if;
+
+               if Has_Aspect (Subp_Id, Aspect_Relaxed_Initialization) then
+                  Aspect_Expr :=
+                    Find_Value_Of_Aspect (E, Aspect_Relaxed_Initialization);
+
+                  --  Aspect expression is either an aggregate, e.g.:
+                  --
+                  --    function F (X : Integer) return Integer
+                  --      with Relaxed_Initialization => (X, F'Result);
+
+                  if Nkind (Aspect_Expr) = N_Aggregate then
+
+                     Param_Expr := First (Expressions (Aspect_Expr));
+
+                     while Present (Param_Expr) loop
+                        if Denotes_Relaxed_Parameter (Param_Expr, E) then
+                           return True;
+                        end if;
+
+                        Next (Param_Expr);
+                     end loop;
+
+                     return False;
+
+                  --  or it is a single identifier, e.g.:
+                  --
+                  --    function F (X : Integer) return Integer
+                  --      with Relaxed_Initialization => X;
+
+                  else
+                     return Denotes_Relaxed_Parameter (Aspect_Expr, E);
+                  end if;
+               else
+                  return False;
+               end if;
+            end;
+
+         when others =>
+            raise Program_Error;
+      end case;
+   end Has_Relaxed_Initialization;
+
    ----------------------
    -- Has_Signed_Zeros --
    ----------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index a6d9139..5aac8b8 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1380,6 +1380,11 @@ package Sem_Util is
    --  Check if a type has a (sub)component of a private type that has not
    --  yet received a full declaration.
 
+   function Has_Relaxed_Initialization (E : Entity_Id) return Boolean;
+   --  Returns True iff entity E, which can be either a type, a variable, an
+   --  abstract state or a function, is subject to the Relaxed_Initialization
+   --  aspect.
+
    function Has_Signed_Zeros (E : Entity_Id) return Boolean;
    --  Determines if the floating-point type E supports signed zeros.
    --  Returns False if E is not a floating-point type.
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 8711788..8d6ba41 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -148,6 +148,7 @@ package Snames is
    Name_Dimension_System               : constant Name_Id := N + $;
    Name_Disable_Controlled             : constant Name_Id := N + $;
    Name_Dynamic_Predicate              : constant Name_Id := N + $;
+   Name_Relaxed_Initialization         : constant Name_Id := N + $;
    Name_Static_Predicate               : constant Name_Id := N + $;
    Name_Synchronization                : constant Name_Id := N + $;
    Name_Unimplemented                  : constant Name_Id := N + $;
@@ -953,6 +954,7 @@ package Snames is
    Name_Has_Tagged_Values              : constant Name_Id := N + $; -- GNAT
    Name_Identity                       : constant Name_Id := N + $;
    Name_Implicit_Dereference           : constant Name_Id := N + $; -- GNAT
+   Name_Initialized                    : constant Name_Id := N + $; -- GNAT
    Name_Integer_Value                  : constant Name_Id := N + $; -- GNAT
    Name_Invalid_Value                  : constant Name_Id := N + $; -- GNAT
    Name_Iterator_Element               : constant Name_Id := N + $; -- GNAT
@@ -1636,6 +1638,7 @@ package Snames is
       Attribute_Has_Tagged_Values,
       Attribute_Identity,
       Attribute_Implicit_Dereference,
+      Attribute_Initialized,
       Attribute_Integer_Value,
       Attribute_Invalid_Value,
       Attribute_Iterator_Element,