[multiple changes]

2012-11-06  Robert Dewar  <dewar@adacore.com>

	* par_sco.adb, bindgen.adb, exp_vfpt.adb, exp_vfpt.ads, exp_ch2.adb,
	errout.adb, sem_ch8.adb: Minor reformatting.

2012-11-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb: Include Loop_Entry_Attributes to the list of
	Node/List/Elist10 usage.
	(Loop_Entry_Attributes): New routine.
	(Set_Loop_Entry_Attributes): New routine.
	(Write_Field10_Name): Add an output string for Loop_Entry_Attributes.
	* einfo.ads: Define new attribute Loop_Entry_Attributes along
	with its usage in nodes.
	(Loop_Entry_Attributes): New routine and dedicated pragma Inline.
	(Set_Loop_Entry_Attributes): New routine and dedicated pragma Inline.
	* exp_attr.adb (Expand_N_Attribute_Reference): Do not expand
	Attribute_Loop_Entry here.
	* exp_ch5.adb: Add with and use clause for Elists;
	(Expand_Loop_Entry_Attributes): New routine.
	(Expand_N_Loop_Statement): Add a call to Expand_Loop_Entry_Attributes.
	* exp_prag.adb (Expand_Pragma_Loop_Assertion): Specialize the
	search to include multiple nested loops produced by the expansion
	of Ada 2012 array iterator.
	* sem_attr.adb: Add with and use clause for Elists.
	(Analyze_Attribute): Check the legality of attribute Loop_Entry.
	(Resolve_Attribute): Nothing to do for Loop_Entry.
	(S14_Attribute): New routine.
	* snames.ads-tmpl: Add a comment on entries marked with
	HiLite. Add new name Name_Loop_Entry. Add new attribute
	Attribute_Loop_Entry.

From-SVN: r193227

gcc/ada/ChangeLog

+2012-11-06  Robert Dewar  <dewar@adacore.com>
+
+	* par_sco.adb, bindgen.adb, exp_vfpt.adb, exp_vfpt.ads, exp_ch2.adb,
+	errout.adb, sem_ch8.adb: Minor reformatting.
+
+2012-11-06  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb: Include Loop_Entry_Attributes to the list of
+	Node/List/Elist10 usage.
+	(Loop_Entry_Attributes): New routine.
+	(Set_Loop_Entry_Attributes): New routine.
+	(Write_Field10_Name): Add an output string for Loop_Entry_Attributes.
+	* einfo.ads: Define new attribute Loop_Entry_Attributes along
+	with its usage in nodes.
+	(Loop_Entry_Attributes): New routine and dedicated pragma Inline.
+	(Set_Loop_Entry_Attributes): New routine and dedicated pragma Inline.
+	* exp_attr.adb (Expand_N_Attribute_Reference): Do not expand
+	Attribute_Loop_Entry here.
+	* exp_ch5.adb: Add with and use clause for Elists;
+	(Expand_Loop_Entry_Attributes): New routine.
+	(Expand_N_Loop_Statement): Add a call to Expand_Loop_Entry_Attributes.
+	* exp_prag.adb (Expand_Pragma_Loop_Assertion): Specialize the
+	search to include multiple nested loops produced by the expansion
+	of Ada 2012 array iterator.
+	* sem_attr.adb: Add with and use clause for Elists.
+	(Analyze_Attribute): Check the legality of attribute Loop_Entry.
+	(Resolve_Attribute): Nothing to do for Loop_Entry.
+	(S14_Attribute): New routine.
+	* snames.ads-tmpl: Add a comment on entries marked with
+	HiLite. Add new name Name_Loop_Entry. Add new attribute
+	Attribute_Loop_Entry.
+
 2012-11-06  Geert Bosch  <bosch@adacore.com>
 
 	* eval_fat.adb (Machine, Succ): Fix front end to support static

gcc/ada/bindgen.adb

@@ -498,8 +498,8 @@ package body Bindgen is
            and then Partition_Elaboration_Policy_Specified = 'S'
          then
             WBI ("      procedure Install_Restricted_Handlers_Sequential;");
-            WBI ("      pragma Import (C,"
-                   & "Install_Restricted_Handlers_Sequential," &
+            WBI ("      pragma Import (C," &
+                 "Install_Restricted_Handlers_Sequential," &
                  " ""__gnat_attach_all_handlers"");");
             WBI ("");
          end if;
@@ -617,15 +617,14 @@ package body Bindgen is
          WBI ("      pragma Import (C, Handler_Installed, " &
               """__gnat_handler_installed"");");
 
-         --  Import handlers attach procedure for sequential elaboration
-         --  policy.
+         --  Import handlers attach procedure for sequential elaboration policy
 
          if System_Interrupts_Used
            and then Partition_Elaboration_Policy_Specified = 'S'
          then
             WBI ("      procedure Install_Restricted_Handlers_Sequential;");
-            WBI ("      pragma Import (C,"
-                   & "Install_Restricted_Handlers_Sequential," &
+            WBI ("      pragma Import (C," &
+                 "Install_Restricted_Handlers_Sequential," &
                  " ""__gnat_attach_all_handlers"");");
             WBI ("");
          end if;

gcc/ada/einfo.adb

@@ -33,6 +33,7 @@ pragma Style_Checks (All_Checks);
 --  Turn off subprogram ordering, not used for this unit
 
 with Atree;  use Atree;
+with Errout; use Errout;
 with Namet;  use Namet;
 with Nlists; use Nlists;
 with Output; use Output;
@@ -90,6 +91,7 @@ package body Einfo is
    --    Discriminal_Link                Node10
    --    Float_Rep                       Uint10 (but returns Float_Rep_Kind)
    --    Handler_Records                 List10
+   --    Loop_Entry_Attributes           Elist10
    --    Normalized_Position_Max         Uint10
 
    --    Component_Bit_Offset            Uint11
@@ -2246,6 +2248,12 @@ package body Einfo is
       return Node16 (Id);
    end Lit_Strings;
 
+   function Loop_Entry_Attributes (Id : E) return L is
+   begin
+      pragma Assert (Ekind (Id) = E_Loop);
+      return Elist10 (Id);
+   end Loop_Entry_Attributes;
+
    function Low_Bound_Tested (Id : E) return B is
    begin
       return Flag205 (Id);
@@ -4791,6 +4799,12 @@ package body Einfo is
       Set_Node16 (Id, V);
    end Set_Lit_Strings;
 
+   procedure Set_Loop_Entry_Attributes (Id : E; V : L) is
+   begin
+      pragma Assert (Ekind (Id) = E_Loop);
+      Set_Elist10 (Id, V);
+   end Set_Loop_Entry_Attributes;
+
    procedure Set_Low_Bound_Tested (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Formal (Id));
@@ -6967,6 +6981,7 @@ package body Einfo is
             --  previous errors.
 
             elsif No (Etyp) then
+               Cascaded_Error;
                return T;
 
             elsif Is_Private_Type (T) and then Etyp = Full_View (T) then
@@ -7874,6 +7889,9 @@ package body Einfo is
               E_Procedure                                  =>
             Write_Str ("Handler_Records");
 
+         when E_Loop                                       =>
+            Write_Str ("Loop_Entry_Attributes");
+
          when E_Component                                  |
               E_Discriminant                               =>
             Write_Str ("Normalized_Position_Max");

gcc/ada/einfo.ads

@@ -2959,6 +2959,10 @@ package Einfo is
 --       the nature and use of this entity for implementing the Image and
 --       Value attributes for the enumeration type in question.
 
+--    Loop_Entry_Attributes (Elist10)
+--       Defined for loop statement scopes. The list contains all Loop_Entry
+--       attribute references related to the target loop.
+
 --    Low_Bound_Tested (Flag205)
 --       Defined in all entities. Currently this can only be set True for
 --       formal parameter entries of a standard unconstrained one-dimensional
@@ -5389,6 +5393,7 @@ package Einfo is
 
    --  E_Loop
    --    First_Exit_Statement                (Node8)
+   --    Loop_Entry_Attributes               (Elist10)
    --    Has_Exit                            (Flag47)
    --    Has_Master_Entity                   (Flag21)
    --    Has_Nested_Block_With_Handler       (Flag101)
@@ -6309,6 +6314,7 @@ package Einfo is
    function Limited_View                        (Id : E) return E;
    function Lit_Indexes                         (Id : E) return E;
    function Lit_Strings                         (Id : E) return E;
+   function Loop_Entry_Attributes               (Id : E) return L;
    function Low_Bound_Tested                    (Id : E) return B;
    function Machine_Radix_10                    (Id : E) return B;
    function Master_Id                           (Id : E) return E;
@@ -6905,6 +6911,7 @@ package Einfo is
    procedure Set_Limited_View                    (Id : E; V : E);
    procedure Set_Lit_Indexes                     (Id : E; V : E);
    procedure Set_Lit_Strings                     (Id : E; V : E);
+   procedure Set_Loop_Entry_Attributes           (Id : E; V : L);
    procedure Set_Low_Bound_Tested                (Id : E; V : B := True);
    procedure Set_Machine_Radix_10                (Id : E; V : B := True);
    procedure Set_Master_Id                       (Id : E; V : E);
@@ -7623,6 +7630,7 @@ package Einfo is
    pragma Inline (Limited_View);
    pragma Inline (Lit_Indexes);
    pragma Inline (Lit_Strings);
+   pragma Inline (Loop_Entry_Attributes);
    pragma Inline (Low_Bound_Tested);
    pragma Inline (Machine_Radix_10);
    pragma Inline (Master_Id);
@@ -8028,6 +8036,7 @@ package Einfo is
    pragma Inline (Set_Limited_View);
    pragma Inline (Set_Lit_Indexes);
    pragma Inline (Set_Lit_Strings);
+   pragma Inline (Set_Loop_Entry_Attributes);
    pragma Inline (Set_Low_Bound_Tested);
    pragma Inline (Set_Machine_Radix_10);
    pragma Inline (Set_Master_Id);

gcc/ada/errout.adb

@@ -18,6 +18,10 @@
 -- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
 -- http://www.gnu.org/licenses for a complete copy of the license.          --
 --                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
 -- GNAT was originally developed  by the GNAT team at  New York University. --
 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
 --                                                                          --
@@ -205,10 +209,9 @@ package body Errout is
    procedure Cascaded_Error is
    begin
       --  An anomaly has been detected which is assumed to be a consequence of
-      --  a previous error. Raise an exception if no serious error has been
-      --  found so far.
+      --  a previous error. Raise an exception if no error found previously.
 
-      if Serious_Errors_Detected = 0 then
+      if Total_Errors_Detected = 0 then
          raise Program_Error;
       end if;
    end Cascaded_Error;

gcc/ada/exp_attr.adb

@@ -2953,7 +2953,7 @@ package body Exp_Attr is
       -- Length --
       ------------
 
-      when Attribute_Length => declare
+      when Attribute_Length => Length : declare
          Ityp : Entity_Id;
          Xnum : Uint;
 
@@ -3103,7 +3103,13 @@ package body Exp_Attr is
          else
             Apply_Universal_Integer_Attribute_Checks (N);
          end if;
-      end;
+      end Length;
+
+      --  The expansion of this attribute is carried out when the target loop
+      --  is processed. See Expand_Loop_Entry_Attributes for details.
+
+      when Attribute_Loop_Entry =>
+         null;
 
       -------------
       -- Machine --

gcc/ada/exp_ch2.adb

@@ -635,8 +635,13 @@ package body Exp_Ch2 is
    ---------------------------
 
    procedure Expand_N_Real_Literal (N : Node_Id) is
+      pragma Unreferenced (N);
+
    begin
-      --  Vax real literal are now allowed by gigi
+      --  Historically, this routine existed because there were expansion
+      --  requirements for Vax real literals, but now Vax real literals
+      --  are now handled by gigi, so this routine no longer does anything.
+
       null;
    end Expand_N_Real_Literal;
 

gcc/ada/exp_prag.adb

@@ -1076,12 +1076,18 @@ package body Exp_Prag is
    --  Start of processing for Expand_Pragma_Loop_Assertion
 
    begin
-      --  Locate the enclosing loop for which this assertion applies
+      --  Locate the enclosing loop for which this assertion applies. In the
+      --  case of Ada 2012 array iteration, we might be dealing with nested
+      --  loops. Only the outermost loop has an identifier.
 
       Loop_Stmt := N;
-      while Present (Loop_Stmt)
-        and then Nkind (Loop_Stmt) /= N_Loop_Statement
-      loop
+      while Present (Loop_Stmt) loop
+         if Nkind (Loop_Stmt) = N_Loop_Statement
+           and then Present (Identifier (Loop_Stmt))
+         then
+            exit;
+         end if;
+
          Loop_Stmt := Parent (Loop_Stmt);
       end loop;
 

gcc/ada/exp_vfpt.adb

@@ -80,8 +80,8 @@ package body Exp_VFpt is
    --  +--------------------------------+
 
    --  Note that the fraction bits are not continuous in memory. Bytes in a
-   --  words are stored using little endianness, but words are stored using
-   --  big endianness (PDP endian)
+   --  words are stored in little endian format, but words are stored using
+   --  big endian format (PDP endian).
 
    --  Like Float F but with 55 bits for the fraction.
 

gcc/ada/exp_vfpt.ads

@@ -54,10 +54,10 @@ package Exp_VFpt is
 
    function Get_Vax_Real_Literal_As_Signed (N : Node_Id) return Uint;
    --  Get the Vax binary representation of a real literal whose type is a Vax
-   --  floating-point type. This is used by gigi. Previously we expanded
-   --  real literal to a call to a LIB$OTS routine that performed the
-   --  conversion. This worked well, but was not efficient and generated huge
-   --  functions for aggregate initialization.
+   --  floating-point type. This is used by gigi. Previously we expanded real
+   --  literal to a call to a LIB$OTS routine that performed the conversion.
+   --  This worked correctly from a funcional point of view, but was
+   --  inefficient and generated huge functions for aggregate initializations.
 
    procedure Expand_Vax_Valid (N : Node_Id);
    --  The node N is an attribute reference node for the Valid attribute where

gcc/ada/par_sco.adb

@@ -34,6 +34,8 @@ with Opt;      use Opt;
 with Output;   use Output;
 with Put_SCOs;
 with SCOs;     use SCOs;
+with Sem;      use Sem;
+with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 with Sinput;   use Sinput;
 with Snames;   use Snames;
@@ -926,9 +928,14 @@ package body Par_SCO is
       Sloc_Range (Orig, Start, Dummy);
       Index := Condition_Pragma_Hash_Table.Get (Start);
 
-      --  The test here for zero is to deal with possible previous errors
+      --  Index can be zero for boolean expressions that do not have SCOs
+      --  (simple decisions outside of a control flow structure), or in case
+      --  of a previous error.
 
-      if Index /= 0 then
+      if Index = 0 then
+         return;
+
+      else
          pragma Assert (SCO_Table.Table (Index).C1 = ' ');
          SCO_Table.Table (Index).C2 := Constant_Condition_Code (Val);
       end if;
@@ -942,6 +949,17 @@ package body Par_SCO is
       Index : Nat;
 
    begin
+      --  Nothing to do if not generating SCO, or if we're not processing the
+      --  original source occurrence of the pragma.
+
+      if not (Generate_SCO
+               and then
+                 In_Extended_Main_Source_Unit (Cunit_Entity (Current_Sem_Unit))
+               and then not (In_Instance or In_Inlined_Body))
+      then
+         return;
+      end if;
+
       --  Note: the reason we use the Sloc value as the key is that in the
       --  generic case, the call to this procedure is made on a copy of the
       --  original node, so we can't use the Node_Id value.
@@ -950,7 +968,10 @@ package body Par_SCO is
 
       --  The test here for zero is to deal with possible previous errors
 
-      if Index /= 0 then
+      if Index = 0 then
+         Cascaded_Error;
+
+      else
          declare
             T : SCO_Table_Entry renames SCO_Table.Table (Index);
 

gcc/ada/sem_attr.adb

@@ -30,6 +30,7 @@ with Casing;   use Casing;
 with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
+with Elists;   use Elists;
 with Errout;   use Errout;
 with Eval_Fat;
 with Exp_Dist; use Exp_Dist;
@@ -375,6 +376,10 @@ package body Sem_Attr is
       pragma No_Return (Error_Attr);
       --  Like Error_Attr, but error is posted at the start of the prefix
 
+      procedure S14_Attribute;
+      --  Called for all attributes defined for formal verification to check
+      --  that the S14_Extensions flag is set.
+
       procedure Standard_Attribute (Val : Int);
       --  Used to process attributes whose prefix is package Standard which
       --  yield values of type Universal_Integer. The attribute reference
@@ -1950,6 +1955,18 @@ package body Sem_Attr is
          Set_Etype (N, Standard_Boolean);
       end Legal_Formal_Attribute;
 
+      -------------------
+      -- S14_Attribute --
+      -------------------
+
+      procedure S14_Attribute is
+      begin
+         if not Formal_Extensions then
+            Error_Attr
+              ("attribute % requires the use of debug switch -gnatd.V", N);
+         end if;
+      end S14_Attribute;
+
       ------------------------
       -- Standard_Attribute --
       ------------------------
@@ -3584,6 +3601,231 @@ package body Sem_Attr is
               ("prefix of % attribute must be a protected object");
          end if;
 
+      ----------------
+      -- Loop_Entry --
+      ----------------
+
+      when Attribute_Loop_Entry => Loop_Entry : declare
+         procedure Check_References_In_Prefix (Loop_Id : Entity_Id);
+         --  Inspect the prefix for any uses of entities declared within the
+         --  related loop. Loop_Id denotes the loop identifier.
+
+         --------------------------------
+         -- Check_References_In_Prefix --
+         --------------------------------
+
+         procedure Check_References_In_Prefix (Loop_Id : Entity_Id) is
+            Loop_Decl : constant Node_Id := Label_Construct (Parent (Loop_Id));
+
+            function Check_Reference (Nod : Node_Id) return Traverse_Result;
+            --  Determine whether a reference mentions an entity declared
+            --  within the related loop.
+
+            function Declared_Within (Nod : Node_Id) return Boolean;
+            --  Determine whether Nod appears in the subtree of Loop_Decl
+
+            ---------------------
+            -- Check_Reference --
+            ---------------------
+
+            function Check_Reference (Nod : Node_Id) return Traverse_Result is
+            begin
+               if Nkind (Nod) = N_Identifier
+                 and then Present (Entity (Nod))
+                 and then Declared_Within (Declaration_Node (Entity (Nod)))
+               then
+                  Error_Attr
+                    ("prefix of attribute % cannot reference local entities",
+                     Nod);
+                  return Abandon;
+               else
+                  return OK;
+               end if;
+            end Check_Reference;
+
+            procedure Check_References is new Traverse_Proc (Check_Reference);
+
+            ---------------------
+            -- Declared_Within --
+            ---------------------
+
+            function Declared_Within (Nod : Node_Id) return Boolean is
+               Stmt : Node_Id;
+
+            begin
+               Stmt := Nod;
+               while Present (Stmt) loop
+                  if Stmt = Loop_Decl then
+                     return True;
+
+                  --  Prevent the search from going too far
+
+                  elsif Nkind_In (Stmt, N_Entry_Body,
+                                        N_Package_Body,
+                                        N_Package_Declaration,
+                                        N_Protected_Body,
+                                        N_Subprogram_Body,
+                                        N_Task_Body)
+                  then
+                     exit;
+                  end if;
+
+                  Stmt := Parent (Stmt);
+               end loop;
+
+               return False;
+            end Declared_Within;
+
+         --  Start of processing for Check_Prefix_For_Local_References
+
+         begin
+            Check_References (P);
+         end Check_References_In_Prefix;
+
+         --  Local variables
+
+         Enclosing_Loop    : Node_Id;
+         In_Loop_Assertion : Boolean   := False;
+         Loop_Id           : Entity_Id := Empty;
+         Scop              : Entity_Id;
+         Stmt              : Node_Id;
+
+      --  Start of processing for Loop_Entry
+
+      begin
+         S14_Attribute;
+         Check_E1;
+         Analyze (E1);
+
+         --  The prefix must denote an object
+
+         if not Is_Object_Reference (P) then
+            Error_Attr_P ("prefix of attribute % must denote an object");
+         end if;
+
+         --  The prefix cannot be of a limited type because the expansion of
+         --  Loop_Entry must create a constant initialized by the evaluated
+         --  prefix.
+
+         if Is_Immutably_Limited_Type (Etype (P)) then
+            Error_Attr_P ("prefix of attribute % cannot be limited");
+         end if;
+
+         --  The sole argument of a Loop_Entry must be a loop name
+
+         if Is_Entity_Name (E1) then
+            Loop_Id := Entity (E1);
+         end if;
+
+         if No (Loop_Id)
+           or else Ekind (Loop_Id) /= E_Loop
+           or else not In_Open_Scopes (Loop_Id)
+         then
+            Error_Attr ("argument of % must be a valid loop name", E1);
+            return;
+         end if;
+
+         --  Climb the parent chain to verify the location of the attribute and
+         --  find the enclosing loop.
+
+         Stmt := N;
+         while Present (Stmt) loop
+
+            --  Locate the enclosing Loop_Assertion pragma (if any). Note that
+            --  when Loop_Assertion is expanded, we must look for an Assertion
+            --  pragma.
+
+            if Nkind (Original_Node (Stmt)) = N_Pragma
+              and then
+                (Pragma_Name (Original_Node (Stmt)) = Name_Assert
+                   or else
+                 Pragma_Name (Original_Node (Stmt)) = Name_Loop_Assertion)
+            then
+               In_Loop_Assertion := True;
+
+            --  Locate the enclosing loop (if any). Note that Ada 2012 array
+            --  iteration may be expanded into several nested loops, we are
+            --  interested in the outermost one which has the loop identifier.
+
+            elsif Nkind (Stmt) = N_Loop_Statement
+              and then Present (Identifier (Stmt))
+            then
+               Enclosing_Loop := Stmt;
+               exit;
+
+            --  Prevent the search from going too far
+
+            elsif Nkind_In (Stmt, N_Entry_Body,
+                                  N_Package_Body,
+                                  N_Package_Declaration,
+                                  N_Protected_Body,
+                                  N_Subprogram_Body,
+                                  N_Task_Body)
+            then
+               exit;
+            end if;
+
+            Stmt := Parent (Stmt);
+         end loop;
+
+         --  Loop_Entry must appear within a Loop_Assertion pragma
+
+         if not In_Loop_Assertion then
+            Error_Attr
+              ("attribute % must appear within pragma Loop_Assertion", N);
+         end if;
+
+         --  A Loop_Entry that applies to a given loop statement shall not
+         --  appear within a body of accept statement, if this construct is
+         --  itself enclosed by the given loop statement.
+
+         for J in reverse 0 .. Scope_Stack.Last loop
+            Scop := Scope_Stack.Table (J).Entity;
+
+            if Ekind (Scop) = E_Loop and then Scop = Loop_Id then
+               exit;
+
+            elsif Ekind_In (Scop, E_Block, E_Loop, E_Return_Statement) then
+               null;
+
+            else
+               Error_Attr
+                 ("cannot appear in program unit or accept statement", N);
+               exit;
+            end if;
+         end loop;
+
+         --  The prefix cannot mention entities declared within the related
+         --  loop because they will not be visible once the prefix is moved
+         --  outside the loop.
+
+         Check_References_In_Prefix (Loop_Id);
+
+         --  The prefix must denote a static entity if the pragma does not
+         --  apply to the innermost enclosing loop statement.
+
+         if Present (Enclosing_Loop)
+           and then Entity (Identifier (Enclosing_Loop)) /= Loop_Id
+           and then not Is_Entity_Name (P)
+         then
+            Error_Attr_P ("prefix of attribute % must denote an entity");
+         end if;
+
+         Set_Etype (N, Etype (P));
+
+         --  Associate the attribute with its related loop
+
+         if No (Loop_Entry_Attributes (Loop_Id)) then
+            Set_Loop_Entry_Attributes (Loop_Id, New_Elmt_List);
+         end if;
+
+         --  A Loop_Entry may be [pre]analyzed several times, depending on the
+         --  context. Ensure that it appears only once in the attributes list
+         --  of the related loop.
+
+         Append_Unique_Elmt (N, Loop_Entry_Attributes (Loop_Id));
+      end Loop_Entry;
+
       -------------
       -- Machine --
       -------------
@@ -6989,6 +7231,13 @@ package body Sem_Attr is
          end;
       end Length;
 
+      ----------------
+      -- Loop_Entry --
+      ----------------
+
+      when Attribute_Loop_Entry =>
+         null;
+
       -------------
       -- Machine --
       -------------

gcc/ada/sem_ch8.adb

@@ -739,7 +739,8 @@ package body Sem_Ch8 is
             --  expanded. Limited types with discriminants are included.
 
             elsif Is_Limited_Record (Typ)
-              or else (Ekind (Typ) = E_Limited_Private_Type
+              or else
+                (Ekind (Typ) = E_Limited_Private_Type
                   and then Has_Discriminants (Typ)
                   and then Is_Access_Type (Etype (First_Discriminant (Typ))))
             then

gcc/ada/snames.ads-tmpl

@@ -771,6 +771,10 @@ package Snames is
    --  The entries marked VMS are recognized only in OpenVMS implementations
    --  of GNAT, and are treated as illegal in all other contexts.
 
+   --  The entries marked HiLite are attributes that are defined by Hi-Lite
+   --  and implemented in GNAT operating under formal verification mode. The
+   --  entries are treated as illegal in all other contexts.
+
    First_Attribute_Name                : constant Name_Id := N + $;
    Name_Abort_Signal                   : constant Name_Id := N + $; -- GNAT
    Name_Access                         : constant Name_Id := N + $;
@@ -832,6 +836,7 @@ package Snames is
    Name_Leading_Part                   : constant Name_Id := N + $;
    Name_Length                         : constant Name_Id := N + $;
    Name_Lock_Free                      : constant Name_Id := N + $; -- GNAT
+   Name_Loop_Entry                     : constant Name_Id := N + $; -- HiLite
    Name_Machine_Emax                   : constant Name_Id := N + $;
    Name_Machine_Emin                   : constant Name_Id := N + $;
    Name_Machine_Mantissa               : constant Name_Id := N + $;
@@ -1442,6 +1447,7 @@ package Snames is
       Attribute_Leading_Part,
       Attribute_Length,
       Attribute_Lock_Free,
+      Attribute_Loop_Entry,
       Attribute_Machine_Emax,
       Attribute_Machine_Emin,
       Attribute_Machine_Mantissa,