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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@193227 138bc75d-0d04-0410-961f-82ee72b054a4

15 files changed, 721 insertions, 36 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7ca698e339c..e3c04aaeb24 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,35 @@
+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
diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb
index bcc01c3d299..71741441d09 100644
--- a/gcc/ada/bindgen.adb
+++ b/gcc/ada/bindgen.adb
@@ -498,9 +498,9 @@ 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," &
-                   " ""__gnat_attach_all_handlers"");");
+            WBI ("      pragma Import (C," &
+                 "Install_Restricted_Handlers_Sequential," &
+                 " ""__gnat_attach_all_handlers"");");
             WBI ("");
          end if;
 
@@ -509,7 +509,7 @@ package body Bindgen is
          then
             WBI ("      Partition_Elaboration_Policy : Character;");
             WBI ("      pragma Import (C, Partition_Elaboration_Policy," &
-                  " ""__gnat_partition_elaboration_policy"");");
+                 " ""__gnat_partition_elaboration_policy"");");
             WBI ("");
             WBI ("      procedure Activate_All_Tasks_Sequential;");
             WBI ("      pragma Import (C, Activate_All_Tasks_Sequential," &
@@ -617,16 +617,15 @@ 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," &
-                   " ""__gnat_attach_all_handlers"");");
+            WBI ("      pragma Import (C," &
+                 "Install_Restricted_Handlers_Sequential," &
+                 " ""__gnat_attach_all_handlers"");");
             WBI ("");
          end if;
 
@@ -638,7 +637,7 @@ package body Bindgen is
          then
             WBI ("      Partition_Elaboration_Policy : Character;");
             WBI ("      pragma Import (C, Partition_Elaboration_Policy," &
-                  " ""__gnat_partition_elaboration_policy"");");
+                 " ""__gnat_partition_elaboration_policy"");");
             WBI ("");
             WBI ("      procedure Activate_All_Tasks_Sequential;");
             WBI ("      pragma Import (C, Activate_All_Tasks_Sequential," &
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index bfa7593dc5d..7e3073ef384 100644
--- a/gcc/ada/einfo.adb
+++ b/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");
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 08fba5a80c9..e4af8cf23fb 100644
--- a/gcc/ada/einfo.ads
+++ b/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);
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 64062b29e9c..48bbc983b19 100644
--- a/gcc/ada/errout.adb
+++ b/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;
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 1b50d293f8c..417bad98847 100644
--- a/gcc/ada/exp_attr.adb
+++ b/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 --
diff --git a/gcc/ada/exp_ch2.adb b/gcc/ada/exp_ch2.adb
index bbd23ba0fdc..64e561cde52 100644
--- a/gcc/ada/exp_ch2.adb
+++ b/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;
 
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index eb861d28933..80aabc5acd8 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -28,6 +28,7 @@ with Atree;    use Atree;
 with Checks;   use Checks;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
+with Elists;   use Elists;
 with Errout;   use Errout;
 with Exp_Aggr; use Exp_Aggr;
 with Exp_Ch6;  use Exp_Ch6;
@@ -110,6 +111,10 @@ package body Exp_Ch5 is
    procedure Expand_Iterator_Loop_Over_Array (N : Node_Id);
    --  Expand loop over arrays that uses the form "for X of C"
 
+   procedure Expand_Loop_Entry_Attributes (N : Node_Id);
+   --  Given a loop statement subject to at least one Loop_Entry attribute,
+   --  expand both the loop and all related Loop_Entry references.
+
    procedure Expand_Predicated_Loop (N : Node_Id);
    --  Expand for loop over predicated subtype
 
@@ -1522,6 +1527,324 @@ package body Exp_Ch5 is
       end;
    end Expand_Assign_Record;
 
+   ----------------------------------
+   -- Expand_Loop_Entry_Attributes --
+   ----------------------------------
+
+   procedure Expand_Loop_Entry_Attributes (N : Node_Id) is
+      procedure Build_Conditional_Block
+        (Loc      : Source_Ptr;
+         Cond     : Node_Id;
+         Stmt     : Node_Id;
+         If_Stmt  : out Node_Id;
+         Blk_Stmt : out Node_Id);
+      --  Create a block Blk_Stmt with an empty declarative list and a single
+      --  statement Stmt. The block is encased in an if statement If_Stmt with
+      --  condition Cond. If_Stmt is Empty when there is no condition provided.
+
+      function Is_Array_Iteration (N : Node_Id) return Boolean;
+      --  Determine whether loop statement N denotes an Ada 2012 iteration over
+      --  an array object.
+
+      -----------------------------
+      -- Build_Conditional_Block --
+      -----------------------------
+
+      procedure Build_Conditional_Block
+        (Loc      : Source_Ptr;
+         Cond     : Node_Id;
+         Stmt     : Node_Id;
+         If_Stmt  : out Node_Id;
+         Blk_Stmt : out Node_Id)
+      is
+      begin
+         Blk_Stmt :=
+           Make_Block_Statement (Loc,
+             Declarations               => New_List,
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => New_List (Stmt)));
+
+         if Present (Cond) then
+            If_Stmt :=
+              Make_If_Statement (Loc,
+                Condition       => Cond,
+                Then_Statements => New_List (Blk_Stmt));
+         else
+            If_Stmt := Empty;
+         end if;
+      end Build_Conditional_Block;
+
+      ------------------------
+      -- Is_Array_Iteration --
+      ------------------------
+
+      function Is_Array_Iteration (N : Node_Id) return Boolean is
+         Stmt : constant Node_Id := Original_Node (N);
+         Iter : Node_Id;
+
+      begin
+         if Nkind (Stmt) = N_Loop_Statement
+           and then Present (Iteration_Scheme (Stmt))
+           and then Present (Iterator_Specification (Iteration_Scheme (Stmt)))
+         then
+            Iter := Iterator_Specification (Iteration_Scheme (Stmt));
+
+            return
+              Of_Present (Iter)
+                and then Is_Array_Type (Etype (Name (Iter)));
+         end if;
+
+         return False;
+      end Is_Array_Iteration;
+
+      --  Local variables
+
+      Loc     : constant Source_Ptr := Sloc (N);
+      Loop_Id : constant Entity_Id  := Identifier (N);
+      Scheme  : constant Node_Id    := Iteration_Scheme (N);
+      Blk     : Node_Id;
+      LE      : Node_Id;
+      LE_Elmt : Elmt_Id;
+      Result  : Node_Id;
+      Temp    : Entity_Id;
+      Typ     : Entity_Id;
+
+   --  Start of processing for Expand_Loop_Entry_Attributes
+
+   begin
+      --  The loop will never execute after it has been expanded, no point in
+      --  processing it.
+
+      if Is_Null_Loop (N) then
+         return;
+
+      --  A loop without an identifier cannot be referenced in 'Loop_Entry
+
+      elsif No (Loop_Id) then
+         return;
+
+      --  The loop is not subject to 'Loop_Entry
+
+      elsif No (Loop_Entry_Attributes (Entity (Loop_Id))) then
+         return;
+
+      --  Step 1: Loop transformations
+
+      --  While loops are transformed into:
+
+      --    if <Condition> then
+      --       declare
+      --          Temp1 : constant <type of Pref1> := <Pref1>;
+      --          . . .
+      --          TempN : constant <type of PrefN> := <PrefN>;
+      --       begin
+      --          loop
+      --             <original source statements with attribute rewrites>
+      --             exit when not <Condition>;
+      --          end loop;
+      --       end;
+      --    end if;
+
+      --  Note that loops over iterators and containers are already converted
+      --  into while loops.
+
+      elsif Present (Condition (Scheme)) then
+         declare
+            Cond : constant Node_Id := Condition (Scheme);
+
+         begin
+            --  Transform the original while loop into an infinite loop where
+            --  the last statement checks the negated condition. This placement
+            --  ensures that the condition will not be evaluated twice on the
+            --  first iteration.
+
+            --  Generate:
+            --    exit when not <Cond>:
+
+            Append_To (Statements (N),
+              Make_Exit_Statement (Loc,
+                Condition => Make_Op_Not (Loc, New_Copy_Tree (Cond))));
+
+            Build_Conditional_Block (Loc,
+              Cond     => Relocate_Node (Cond),
+              Stmt     => Relocate_Node (N),
+              If_Stmt  => Result,
+              Blk_Stmt => Blk);
+         end;
+
+      --  Ada 2012 iteration over an array is transformed into:
+
+      --    if <Array_Nam>'Length (1) > 0
+      --      and then <Array_Nam>'Length (N) > 0
+      --    then
+      --       declare
+      --          Temp1 : constant <type of Pref1> := <Pref1>;
+      --          . . .
+      --          TempN : constant <type of PrefN> := <PrefN>;
+      --       begin
+      --          for X in ... loop  --  multiple loops depending on dims
+      --             <original source statements with attribute rewrites>
+      --          end loop;
+      --       end;
+      --    end if;
+
+      elsif Is_Array_Iteration (N) then
+         declare
+            Array_Nam : constant Entity_Id :=
+                          Entity (Name (Iterator_Specification
+                            (Iteration_Scheme (Original_Node (N)))));
+            Num_Dims  : constant Pos :=
+                          Number_Dimensions (Etype (Array_Nam));
+            Cond      : Node_Id := Empty;
+            Check     : Node_Id;
+            Top_Loop  : Node_Id;
+
+         begin
+            --  Generate a check which determines whether all dimensions of
+            --  the array are non-null.
+
+            for Dim in 1 .. Num_Dims loop
+               Check :=
+                 Make_Op_Gt (Loc,
+                   Left_Opnd  =>
+                     Make_Attribute_Reference (Loc,
+                       Prefix         => New_Reference_To (Array_Nam, Loc),
+                       Attribute_Name => Name_Length,
+                       Expressions    => New_List (
+                         Make_Integer_Literal (Loc, Dim))),
+                   Right_Opnd =>
+                     Make_Integer_Literal (Loc, 0));
+
+               if No (Cond) then
+                  Cond := Check;
+               else
+                  Cond :=
+                    Make_And_Then (Loc,
+                      Left_Opnd  => Cond,
+                      Right_Opnd => Check);
+               end if;
+            end loop;
+
+            Top_Loop := Relocate_Node (N);
+            Set_Analyzed (Top_Loop);
+
+            Build_Conditional_Block (Loc,
+              Cond     => Cond,
+              Stmt     => Top_Loop,
+              If_Stmt  => Result,
+              Blk_Stmt => Blk);
+         end;
+
+      --  For loops are transformed into:
+
+      --    if <Low> <= <High> then
+      --       declare
+      --          Temp1 : constant <type of Pref1> := <Pref1>;
+      --          . . .
+      --          TempN : constant <type of PrefN> := <PrefN>;
+      --       begin
+      --          for <Def_Id> in <Low> .. <High> loop
+      --             <original source statements with attribute rewrites>
+      --          end loop;
+      --       end;
+      --    end if;
+
+      elsif Present (Loop_Parameter_Specification (Scheme)) then
+         declare
+            Loop_Spec : constant Node_Id :=
+                          Loop_Parameter_Specification (Scheme);
+            Subt_Def  : constant Node_Id :=
+                          Discrete_Subtype_Definition (Loop_Spec);
+            Cond      : Node_Id;
+
+         begin
+            --  At this point in the expansion all discrete subtype definitions
+            --  should be transformed into ranges.
+
+            pragma Assert (Nkind (Subt_Def) = N_Range);
+
+            --  Generate
+            --    Low <= High
+
+            Cond :=
+              Make_Op_Le (Loc,
+                Left_Opnd  => New_Copy_Tree (Low_Bound (Subt_Def)),
+                Right_Opnd => New_Copy_Tree (High_Bound (Subt_Def)));
+
+            Build_Conditional_Block (Loc,
+              Cond     => Cond,
+              Stmt     => Relocate_Node (N),
+              If_Stmt  => Result,
+              Blk_Stmt => Blk);
+         end;
+
+      --  Infinite loops are transformed into:
+
+      --    declare
+      --       Temp1 : constant <type of Pref1> := <Pref1>;
+      --       . . .
+      --       TempN : constant <type of PrefN> := <PrefN>;
+      --    begin
+      --       loop
+      --          <original source statements with attribute rewrites>
+      --       end loop;
+      --    end;
+
+      else
+         Build_Conditional_Block (Loc,
+           Cond     => Empty,
+           Stmt     => Relocate_Node (N),
+           If_Stmt  => Result,
+           Blk_Stmt => Blk);
+
+         Result := Blk;
+      end if;
+
+      --  Step 2: Loop_Entry attribute transformations
+
+      --  At this point the various loops have been augmented to contain a
+      --  block. Populate the declarative list of the block with constants
+      --  which store the value of their relative prefixes at the point of
+      --  entry in the loop.
+
+      LE_Elmt := First_Elmt (Loop_Entry_Attributes (Entity (Loop_Id)));
+      while Present (LE_Elmt) loop
+         LE  := Node (LE_Elmt);
+         Typ := Etype (Prefix (LE));
+
+         --  Declare a constant to capture the value of the previx of each
+         --  Loop_Entry attribute.
+
+         --  Generate:
+         --    Temp : constant <type of Pref> := <Pref>;
+
+         Temp := Make_Temporary (Loc, 'P');
+
+         Append_To (Declarations (Blk),
+           Make_Object_Declaration (Loc,
+             Defining_Identifier => Temp,
+             Constant_Present    => True,
+             Object_Definition   => New_Reference_To (Typ, Loc),
+             Expression          => Relocate_Node (Prefix (LE))));
+
+         --  Replace the original attribute with a reference to the constant
+
+         Rewrite (LE, New_Reference_To (Temp, Loc));
+         Set_Etype (LE, Typ);
+
+         Next_Elmt (LE_Elmt);
+      end loop;
+
+      --  Destroy the list of Loop_Entry attributes to prevent the infinite
+      --  expansion when analyzing and expanding the newly generated loops.
+
+      Set_Loop_Entry_Attributes (Entity (Loop_Id), No_Elist);
+
+      Rewrite (N, Result);
+      Analyze (N);
+   end Expand_Loop_Entry_Attributes;
+
    -----------------------------------
    -- Expand_N_Assignment_Statement --
    -----------------------------------
@@ -3662,6 +3985,13 @@ package body Exp_Ch5 is
       then
          Expand_Iterator_Loop (N);
       end if;
+
+      --  If the loop is subject to at least one Loop_Entry attribute, it
+      --  requires additional processing.
+
+      if Nkind (N) = N_Loop_Statement then
+         Expand_Loop_Entry_Attributes (N);
+      end if;
    end Expand_N_Loop_Statement;
 
    ----------------------------
@@ -3854,10 +4184,10 @@ package body Exp_Ch5 is
             --  Rewrite the loop
 
             D :=
-               Make_Object_Declaration (Loc,
-                 Defining_Identifier => Loop_Id,
-                 Object_Definition   => New_Occurrence_Of (Ltype, Loc),
-                 Expression          => Lo_Val (First (Stat)));
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => Loop_Id,
+                Object_Definition   => New_Occurrence_Of (Ltype, Loc),
+                Expression          => Lo_Val (First (Stat)));
             Set_Suppress_Assignment_Checks (D);
 
             Rewrite (N,
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index c41cc815cb5..c21c21c5c80 100644
--- a/gcc/ada/exp_prag.adb
+++ b/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;
 
diff --git a/gcc/ada/exp_vfpt.adb b/gcc/ada/exp_vfpt.adb
index af4c3ef4d82..82d2fe16e7d 100644
--- a/gcc/ada/exp_vfpt.adb
+++ b/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.
 
diff --git a/gcc/ada/exp_vfpt.ads b/gcc/ada/exp_vfpt.ads
index 52aaf7dd3f3..db018669435 100644
--- a/gcc/ada/exp_vfpt.ads
+++ b/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
diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb
index be258bfb8b0..cec2afefdb2 100644
--- a/gcc/ada/par_sco.adb
+++ b/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);
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 1b9ebcb1ffe..223f3879155 100644
--- a/gcc/ada/sem_attr.adb
+++ b/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 --
       -------------
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 479798044a0..7b937a67ac5 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -739,9 +739,10 @@ 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
-                and then Has_Discriminants (Typ)
-                and then Is_Access_Type (Etype (First_Discriminant (Typ))))
+              or else
+                (Ekind (Typ) = E_Limited_Private_Type
+                  and then Has_Discriminants (Typ)
+                  and then Is_Access_Type (Etype (First_Discriminant (Typ))))
             then
                null;
 
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index be0b7ff7e37..864d8ed12c4 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/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,