[multiple changes]

2014-07-29  Thomas Quinot  <quinot@adacore.com>

	* gnat_rm.texi: Document internal attributes used for PolyORB/DSA
	distributed stubs generation.
	* exp_ch3.adb: Minor reformatting.

2014-07-29  Yannick Moy  <moy@adacore.com>

	* sinfo.ads: Document constraint between frontend and GNATprove.

From-SVN: r213193

gcc/ada/ChangeLog

@@ -1,3 +1,13 @@
+2014-07-29  Thomas Quinot  <quinot@adacore.com>
+
+	* gnat_rm.texi: Document internal attributes used for PolyORB/DSA
+	distributed stubs generation.
+	* exp_ch3.adb: Minor reformatting.
+
+2014-07-29  Yannick Moy  <moy@adacore.com>
+
+	* sinfo.ads: Document constraint between frontend and GNATprove.
+
 2014-07-29  Robert Dewar  <dewar@adacore.com>
 
 	* a-except.adb: Minor comment clarification.

gcc/ada/exp_ch3.adb

@@ -3173,7 +3173,7 @@ package body Exp_Ch3 is
 
       exception
          when RE_Not_Available =>
-         return Empty_List;
+            return Empty_List;
       end Build_Init_Statements;
 
       -------------------------

gcc/ada/gnat_rm.texi

@@ -8501,7 +8501,9 @@ In addition, Ada allows implementations to define additional
 attributes whose meaning is defined by the implementation.  GNAT provides
 a number of these implementation-dependent attributes which can be used
 to extend and enhance the functionality of the compiler.  This section of
-the GNAT reference manual describes these additional attributes.
+the GNAT reference manual describes these additional attributes.  It also
+describes additional implementation-dependent features of standard
+language-defined attributes.
 
 Note that any program using these attributes may not be portable to
 other compilers (although GNAT implements this set of attributes on all
@@ -8983,7 +8985,8 @@ input-output functions for fixed-point values.
 @unnumberedsec Attribute From_Any
 @findex From_Any
 @noindent
-PLEASE ADD DOCUMENTATION HERE???
+This internal attribute is used for the generation of remote subprogram
+stubs in the context of the Distributed Systems Annex.
 
 @node Attribute Has_Access_Values
 @unnumberedsec Attribute Has_Access_Values
@@ -9322,7 +9325,13 @@ statically matching subtypes.
 @unnumberedsec Attribute Old
 @findex Old
 @noindent
-PLEASE ADD DOCUMENTATION HERE???
+In addition to the usage of Old defined in the Ada 2012 RM (usage
+within @code{Post} aspect), GNAT also permits the use of this attribute
+in implementation defined pragmas @code{Postcondition},
+@code{Loop_Entry}, and @code{Contract_Cases}. Also usages of
+@code{Old} which would be illegal according to the Ada 2012 RM
+definition are allowed under control of
+implementation defined pragma @code{Allow_Unevaluated_Use_Of_Old}.
 
 @node Attribute Passed_By_Reference
 @unnumberedsec Attribute Passed_By_Reference
@@ -9725,7 +9734,8 @@ a 32 bits machine).
 @unnumberedsec Attribute To_Any
 @findex To_Any
 @noindent
-PLEASE ADD DOCUMENTATION HERE???
+This internal attribute is used for the generation of remote subprogram
+stubs in the context of the Distributed Systems Annex.
 
 @node Attribute Type_Class
 @unnumberedsec Attribute Type_Class
@@ -9759,13 +9769,17 @@ be compatible with the DEC Ada 83 attribute of the same name.
 @unnumberedsec Attribute Type_Key
 @findex Type_Key
 @noindent
-PLEASE ADD DOCUMENTATION HERE???
+The @code{Type_Key} attribute is applicable to a type or subtype and
+yields a value of type Standard.String containing encoded information
+about the type or subtype. This provides improved compatibility with
+other implementations that support this attribute.
 
 @node Attribute TypeCode
 @unnumberedsec Attribute TypeCode
 @findex TypeCode
 @noindent
-PLEASE ADD DOCUMENTATION HERE???
+This internal attribute is used for the generation of remote subprogram
+stubs in the context of the Distributed Systems Annex.
 
 @node Attribute UET_Address
 @unnumberedsec Attribute UET_Address

gcc/ada/sinfo.ads

@@ -562,12 +562,20 @@ package Sinfo is
    --  not make sense from a user point-of-view, and that cross-references that
    --  do not lead to data dependences for subprograms can be safely ignored.
 
-   --  In addition pragma Debug statements are removed from the tree (rewritten
-   --  to NULL stmt), since they should be ignored in formal verification.
+   --  GNATprove relies on the following frontend behaviors:
 
-   --  An error is also issued for missing subunits, similar to the warning
-   --  issued when generating code, to avoid formal verification of a partial
-   --  unit.
+   --    1. The first declarations in the list of visible declarations of
+   --       a package declaration for a generic instance, up to the first
+   --       declaration which comes from source, should correspond to
+   --       the "mappings nodes" between formal and actual generic parameters.
+
+   --    2. In addition pragma Debug statements are removed from the tree
+   --       (rewritten to NULL stmt), since they should be ignored in formal
+   --       verification.
+
+   --    3. An error is also issued for missing subunits, similar to the
+   --       warning issued when generating code, to avoid formal verification
+   --       of a partial unit.
 
    -----------------------
    -- Check Flag Fields --