[multiple changes]

2013-04-24  Robert Dewar  <dewar@adacore.com>

	* sem_ch3.adb, sem_ch7.adb: Minor reformatting.
	* gnat_rm.texi: Document pragma Loop_Invariant.
	* sem_attr.adb (Analyze_Attribute, case Loop_Entry): This is
	no longer an S14_Attribute.
	* sem_prag.adb (Analyze_Pragma, case Loop_Invariant): Combine
	processing with Assert, allow message parameter, remove call
	to S14_Pragma.

2013-04-24  Thomas Quinot  <quinot@adacore.com>

	* exp_ch4.adb: Minor reformatting.

From-SVN: r198241

7 files changed, 105 insertions, 65 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 345f9d2..5cbe4b1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2013-04-24  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch3.adb, sem_ch7.adb: Minor reformatting.
+	* gnat_rm.texi: Document pragma Loop_Invariant.
+	* sem_attr.adb (Analyze_Attribute, case Loop_Entry): This is
+	no longer an S14_Attribute.
+	* sem_prag.adb (Analyze_Pragma, case Loop_Invariant): Combine
+	processing with Assert, allow message parameter, remove call
+	to S14_Pragma.
+
+2013-04-24  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_ch4.adb: Minor reformatting.
+
 2013-04-24  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch7.adb (Swap_Private_Dependents): New internal routine
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 22cbe79..e1b6cf0 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -4191,7 +4191,7 @@ package body Exp_Ch4 is
 
       --  Local variables
 
-      Dtyp    : constant Entity_Id  := Available_View (Designated_Type (PtrT));
+      Dtyp    : constant Entity_Id := Available_View (Designated_Type (PtrT));
       Desig   : Entity_Id;
       Nod     : Node_Id;
       Pool    : Entity_Id;
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 2d162ef..023cd12 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -179,6 +179,7 @@ Implementation Defined Pragmas
 * Pragma Linker_Destructor::
 * Pragma Linker_Section::
 * Pragma Long_Float::
+* Pragma Loop_Invariant::
 * Pragma Loop_Optimize::
 * Pragma Loop_Variant::
 * Pragma Machine_Attribute::
@@ -937,6 +938,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Linker_Destructor::
 * Pragma Linker_Section::
 * Pragma Long_Float::
+* Pragma Loop_Invariant::
 * Pragma Loop_Optimize::
 * Pragma Loop_Variant::
 * Pragma Machine_Attribute::
@@ -3993,6 +3995,33 @@ For further details on this pragma, see the
 @cite{DEC Ada Language Reference Manual}, section 3.5.7b.  Note that to use
 this pragma, the standard runtime libraries must be recompiled.
 
+@node Pragma Loop_Invariant
+@unnumberedsec Pragma Loop_Invariant
+@findex Loop_Invariant
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Loop_Invariant ( boolean_EXPRESSION );
+
+@end smallexample
+
+@noindent
+The effect of this pragma is similar to that of pragma @code{Assert},
+except that in an @code{Assertion_Policy} pragma, the identifier
+@code{Loop_Invariant} is used to control whether it is ignored or checked
+(or disabled).
+
+@code{Loop_Invariant} can only appear as one of the items in the sequence
+of statements of a loop body. The intention is that it be used to
+represent a "loop invariant" assertion, i.e. something that is true each
+time through the loop, and which can be used to show that the loop is
+achieving its purpose.
+
+To aid in writing such invariants, the special attribute @code{Loop_Entry}
+may be used to refer to the value of an expression on entry to the loop. This
+attribute can only be used within the expression of a @code{Loop_Invariant}
+pragma. For full details, see documentation of attribute @code{Loop_Entry}.
+
 @node Pragma Loop_Optimize
 @unnumberedsec Pragma Loop_Optimize
 @findex Loop_Optimize
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 30509dc..f3845f6 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -379,6 +379,8 @@ package body Sem_Attr is
       procedure S14_Attribute;
       --  Called for all attributes defined for formal verification to check
       --  that the S14_Extensions flag is set.
+      --  Bad name ???
+      --  No such thing as S14_Extensions flag ???
 
       procedure Standard_Attribute (Val : Int);
       --  Used to process attributes whose prefix is package Standard which
@@ -3729,8 +3731,6 @@ package body Sem_Attr is
          --  expression list. Instead, all available expressions are stored as
          --  indexed components.
 
-         S14_Attribute;
-
          --  When the attribute is part of an indexed component, find the first
          --  expression as it will determine the semantics of 'Loop_Entry.
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 8e874af..89f11dc 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -8659,7 +8659,7 @@ package body Sem_Ch3 is
          Set_Known_To_Have_Preelab_Init
            (Def_Id, Known_To_Have_Preelab_Init (T));
 
-         --  private subtypes may have private dependents.
+         --  Private subtypes may have private dependents
 
          Set_Private_Dependents (Def_Id, New_Elmt_List);
 
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index c21874d..b98bf9c 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -1820,6 +1820,10 @@ package body Sem_Ch7 is
       --  same for its private dependents under proper visibility conditions.
       --  When compiling a grand-chid unit this needs to be done recursively.
 
+      -----------------------------
+      -- Swap_Private_Dependents --
+      -----------------------------
+
       procedure Swap_Private_Dependents (Priv_Deps : Elist_Id) is
          Deps      : Elist_Id;
          Priv      : Entity_Id;
@@ -1828,13 +1832,12 @@ package body Sem_Ch7 is
 
       begin
          Priv_Elmt := First_Elmt (Priv_Deps);
-
          while Present (Priv_Elmt) loop
             Priv := Node (Priv_Elmt);
 
-            --  Before the exchange, verify that the presence of the
-            --  Full_View field. It will be empty if the entity has already
-            --  been installed due to a previous call.
+            --  Before the exchange, verify that the presence of the Full_View
+            --  field. This field will be empty if the entity has already been
+            --  installed due to a previous call.
 
             if Present (Full_View (Priv))
               and then Is_Visible_Dependent (Priv)
@@ -1846,9 +1849,9 @@ package body Sem_Ch7 is
                   Is_Priv := False;
                end if;
 
-               --  For each subtype that is swapped, we also swap the
-               --  reference to it in Private_Dependents, to allow access
-               --  to it when we swap them out in End_Package_Scope.
+               --  For each subtype that is swapped, we also swap the reference
+               --  to it in Private_Dependents, to allow access to it when we
+               --  swap them out in End_Package_Scope.
 
                Replace_Elmt (Priv_Elmt, Full_View (Priv));
                Exchange_Declarations (Priv);
@@ -1857,7 +1860,7 @@ package body Sem_Ch7 is
                Set_Is_Potentially_Use_Visible
                  (Priv, Is_Potentially_Use_Visible (Node (Priv_Elmt)));
 
-               --  Within a child unit, recurse.
+               --  Within a child unit, recurse
 
                if Is_Priv
                  and then Is_Child_Unit (Cunit_Entity (Current_Sem_Unit))
@@ -1870,14 +1873,16 @@ package body Sem_Ch7 is
          end loop;
       end Swap_Private_Dependents;
 
+   --  Start processing for Install_Private_Declarations
+
    begin
       --  First exchange declarations for private types, so that the full
       --  declaration is visible. For each private type, we check its
       --  Private_Dependents list and also exchange any subtypes of or derived
       --  types from it. Finally, if this is a Taft amendment type, the
       --  incomplete declaration is irrelevant, and we want to link the
-      --  eventual full declaration with the original private one so we also
-      --  skip the exchange.
+      --  eventual full declaration with the original private one so we
+      --  also skip the exchange.
 
       Id := First_Entity (P);
       while Present (Id) and then Id /= First_Private_Entity (P) loop
@@ -1887,8 +1892,8 @@ package body Sem_Ch7 is
            and then Scope (Full_View (Id)) = Scope (Id)
            and then Ekind (Full_View (Id)) /= E_Incomplete_Type
          then
-            --  If there is a use-type clause on the private type, set the
-            --  full view accordingly.
+            --  If there is a use-type clause on the private type, set the full
+            --  view accordingly.
 
             Set_In_Use (Full_View (Id), In_Use (Id));
             Full := Full_View (Id);
@@ -1904,9 +1909,9 @@ package body Sem_Ch7 is
                --  from another private type which is not private anymore. This
                --  can only happen in a package nested within a child package,
                --  when the parent type is defined in the parent unit. At this
-               --  point the current type is not private either, and we have to
-               --  install the underlying full view, which is now visible. Save
-               --  the current full view as well, so that all views can be
+               --  point the current type is not private either, and we have
+               --  to install the underlying full view, which is now visible.
+               --  Save the current full view as well, so that all views can be
                --  restored on exit. It may seem that after compiling the child
                --  body there are not environments to restore, but the back-end
                --  expects those links to be valid, and freeze nodes depend on
@@ -2069,7 +2074,6 @@ package body Sem_Ch7 is
       else
          declare
             Prev : Entity_Id;
-
          begin
             Prev := Find_Type_Name (N);
             pragma Assert (Prev = Id
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c421b5a..0b23215 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -8828,9 +8828,9 @@ package body Sem_Prag is
             end if;
          end Annotate;
 
-         ----------------------------------
-         -- Assert/Assert_And_Cut/Assume --
-         ----------------------------------
+         -------------------------------------------------
+         -- Assert/Assert_And_Cut/Assume/Loop_Invariant --
+         -------------------------------------------------
 
          --  pragma Assert
          --    (   [Check => ]  Boolean_EXPRESSION
@@ -8844,17 +8844,27 @@ package body Sem_Prag is
          --    (   [Check => ]  Boolean_EXPRESSION
          --     [, [Message =>] Static_String_EXPRESSION]);
 
+         --  pragma Loop_Invariant
+         --    (   [Check => ]  Boolean_EXPRESSION
+         --     [, [Message =>] Static_String_EXPRESSION]);
+
          when Pragma_Assert         |
               Pragma_Assert_And_Cut |
-              Pragma_Assume         =>
+              Pragma_Assume         |
+              Pragma_Loop_Invariant =>
          Assert : declare
             Expr : Node_Id;
             Newa : List_Id;
 
          begin
+            --  Assert is an Ada 2005 RM-defined pragma
+
             if Prag_Id = Pragma_Assert then
                Ada_2005_Pragma;
-            else -- Pragma_Assert_And_Cut
+
+            --  The remaining ones are GNAT pragmas
+
+            else
                GNAT_Pragma;
             end if;
 
@@ -8863,19 +8873,32 @@ package body Sem_Prag is
             Check_Arg_Order ((Name_Check, Name_Message));
             Check_Optional_Identifier (Arg1, Name_Check);
 
-            --  We treat pragma Assert[_And_Cut] as equivalent to:
+            --  Special processing for Loop_Invariant
 
-            --    pragma Check (Assert[_And_Cut], condition [, msg]);
+            if Prag_Id = Pragma_Loop_Invariant then
 
-            --  So rewrite pragma in this manner, transfer the message
-            --  argument if present, and analyze the result
+               --  Check restricted placement, must be within a loop
 
-            --  Pragma Assert_And_Cut is treated exactly like pragma Assert by
-            --  the frontend. Formal verification tools may use it to "cut" the
-            --  paths through the code, to make verification tractable. When
-            --  dealing with a semantically analyzed tree, the information that
-            --  a Check node N corresponds to a source Assert_And_Cut pragma
-            --  can be retrieved from the pragma kind of Original_Node(N).
+               Check_Loop_Pragma_Placement;
+
+               --  Do preanalyze to deal with embedded Loop_Entry attribute
+
+               Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
+            end if;
+
+            --  Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating
+            --  a corresponding Check pragma:
+
+            --    pragma Check (name, condition [, msg]);
+
+            --  Where name is the identifier matching the pragma name. So
+            --  rewrite pragma in this manner, transfer the message argument
+            --  if present, and analyze the result
+
+            --  Note: When dealing with a semantically analyzed tree, the
+            --  information that a Check node N corresponds to a source Assert,
+            --  Assume, or Assert_And_Cut pragma can be retrieved from the
+            --  pragma kind of Original_Node(N).
 
             Expr := Get_Pragma_Arg (Arg1);
             Newa := New_List (
@@ -13890,36 +13913,6 @@ package body Sem_Prag is
             Set_Standard_Fpt_Formats;
          end Long_Float;
 
-         --------------------
-         -- Loop_Invariant --
-         --------------------
-
-         --  pragma Loop_Invariant ( boolean_EXPRESSION );
-
-         when Pragma_Loop_Invariant => Loop_Invariant : declare
-         begin
-            GNAT_Pragma;
-            S14_Pragma;
-            Check_Arg_Count (1);
-            Check_Loop_Pragma_Placement;
-
-            Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
-
-            --  Transform pragma Loop_Invariant into equivalent pragma Check
-            --  Generate:
-            --    pragma Check (Loop_Invaraint, Arg1);
-
-            Rewrite (N,
-              Make_Pragma (Loc,
-                Chars                        => Name_Check,
-                Pragma_Argument_Associations => New_List (
-                  Make_Pragma_Argument_Association (Loc,
-                    Expression => Make_Identifier (Loc, Name_Loop_Invariant)),
-                  Relocate_Node (Arg1))));
-
-            Analyze (N);
-         end Loop_Invariant;
-
          -------------------
          -- Loop_Optimize --
          -------------------