Patchwork [Ada] Attribute Loop_Entry

login
register
mail settings
Submitter Arnaud Charlet
Date Nov. 6, 2012, 10:20 a.m.
Message ID <20121106102051.GA20718@adacore.com>
Download mbox | patch
Permalink /patch/197449/
State New
Headers show

Comments

Arnaud Charlet - Nov. 6, 2012, 10:20 a.m.
This patch provides the initial implementation of attribute Loop_Entry. This
attribute is indended for formal verification proofs.

The syntax of the attribute is as follows:

   Prefix'Loop_Entry (Target_Loop_Name)

The brief semantic rules for this attribute are:

The prefix must denote a non-limited object and the only attribute association
allowed must be a loop name. Attribute Loop_Entry can only appear inside pragma
Loop_Assertion.

For each prefix of a Loop_Entry attribute, a constant is implicitly declared at
the beginning of the associated loop statement. The constant's type is that of
the prefix. It is initialized to the result of evaluating the prefix as an
expression at the point of the constant declaration. The constant declaration
is not elaborated if the loop statement had a null iteration scheme.

The value of Prefix'Loop_Entry (Target_Loop_Name) is the value of the constant
and the type of Prefix'Loop_Entry (Target_Loop_Name) is that of the constant.

Example of usage:

procedure Main is
   Counter : Natural := 1;

begin
   Target : for Index in 1 .. 3 loop
      pragma Loop_Assertion
        (Invariant => Counter'Loop_Entry (Target) = Counter);

      Counter := Counter + 1;
   end loop Target;
end Main;

In the above example, the value of Counter at the point of entry into the loop
is 1. As a result, the Loop_Assertion should fail on the second iteration.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

Patch

Index: exp_ch5.adb
===================================================================
--- exp_ch5.adb	(revision 193215)
+++ exp_ch5.adb	(working copy)
@@ -28,6 +28,7 @@ 
 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 @@ 
    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 @@ 
       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 @@ 
       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 @@ 
             --  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,
Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 193219)
+++ exp_prag.adb	(working copy)
@@ -1076,12 +1076,18 @@ 
    --  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;
 
Index: exp_attr.adb
===================================================================
--- exp_attr.adb	(revision 193215)
+++ exp_attr.adb	(working copy)
@@ -2953,7 +2953,7 @@ 
       -- Length --
       ------------
 
-      when Attribute_Length => declare
+      when Attribute_Length => Length : declare
          Ityp : Entity_Id;
          Xnum : Uint;
 
@@ -3103,8 +3103,14 @@ 
          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 --
       -------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 193215)
+++ einfo.adb	(working copy)
@@ -33,6 +33,7 @@ 
 --  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 @@ 
    --    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 @@ 
       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 @@ 
       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 @@ 
             --  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 @@ 
               E_Procedure                                  =>
             Write_Str ("Handler_Records");
 
+         when E_Loop                                       =>
+            Write_Str ("Loop_Entry_Attributes");
+
          when E_Component                                  |
               E_Discriminant                               =>
             Write_Str ("Normalized_Position_Max");
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 193215)
+++ einfo.ads	(working copy)
@@ -2959,6 +2959,10 @@ 
 --       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 @@ 
 
    --  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 @@ 
    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 @@ 
    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 @@ 
    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 @@ 
    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);
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 193225)
+++ sem_attr.adb	(working copy)
@@ -30,6 +30,7 @@ 
 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 @@ 
       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 @@ 
          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 @@ 
               ("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 @@ 
          end;
       end Length;
 
+      ----------------
+      -- Loop_Entry --
+      ----------------
+
+      when Attribute_Loop_Entry =>
+         null;
+
       -------------
       -- Machine --
       -------------
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 193216)
+++ snames.ads-tmpl	(working copy)
@@ -771,6 +771,10 @@ 
    --  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 @@ 
    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 @@ 
       Attribute_Leading_Part,
       Attribute_Length,
       Attribute_Lock_Free,
+      Attribute_Loop_Entry,
       Attribute_Machine_Emax,
       Attribute_Machine_Emin,
       Attribute_Machine_Mantissa,