[multiple changes]

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

	* sem_ch6.adb: Add comments.

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

	* s-os_lib.ads (GM_Time_Of): Clarify documentation.

2014-07-30  Robert Dewar  <dewar@adacore.com>

	* sem_aggr.adb, sem_res.adb: Minor reformatting.

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

	* sem_ch13.adb (Analyze_Attribute_Definition_Clause, case
	Bit_Order): Set Reverse_Bit_Order on the base type of the
	specified first subtype.

From-SVN: r213261

gcc/ada/ChangeLog

+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb: Add comments.
+
+2014-07-30  Thomas Quinot  <quinot@adacore.com>
+
+	* s-os_lib.ads (GM_Time_Of): Clarify documentation.
+
+2014-07-30  Robert Dewar  <dewar@adacore.com>
+
+	* sem_aggr.adb, sem_res.adb: Minor reformatting.
+
+2014-07-30  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_ch13.adb (Analyze_Attribute_Definition_Clause, case
+	Bit_Order): Set Reverse_Bit_Order on the base type of the
+	specified first subtype.
+
 2014-07-30  Ed Schonberg  <schonberg@adacore.com>
 
 	* inline.adb (Expand_Inlined_Call): Use a renaming declaration

gcc/ada/s-os_lib.ads

@@ -160,8 +160,8 @@ package System.OS_Lib is
       Minute : Minute_Type;
       Second : Second_Type) return OS_Time;
    --  Analogous to the Time_Of routine in Ada.Calendar, takes a set of time
-   --  component parts and returns an OS_Time. Returns Invalid_Time if the
-   --  creation fails.
+   --  component parts to be interpreted in the local time zone, and returns
+   --  an OS_Time. Returns Invalid_Time if the creation fails.
 
    function Current_Time_String return String;
    --  Returns current local time in the form YYYY-MM-DD HH:MM:SS. The result

gcc/ada/sem_aggr.adb

@@ -111,7 +111,8 @@ package body Sem_Aggr is
    --  Check that Expr is either not limited or else is one of the cases of
    --  expressions allowed for a limited component association (namely, an
    --  aggregate, function call, or <> notation). Report error for violations.
-   --  Expression is also OK in an instance or inlining context.
+   --  Expression is also OK in an instance or inlining context, because we
+   --  have already analyzed and checked it.
 
    procedure Check_Qualified_Aggregate (Level : Nat; Expr : Node_Id);
    --  Given aggregate Expr, check that sub-aggregates of Expr that are nested

gcc/ada/sem_ch13.adb

@@ -4293,7 +4293,7 @@ package body Sem_Ch13 is
 
                else
                   if (Expr_Value (Expr) = 0) /= Bytes_Big_Endian then
-                     Set_Reverse_Bit_Order (U_Ent, True);
+                     Set_Reverse_Bit_Order (Base_Type (U_Ent), True);
                   end if;
                end if;
             end if;

gcc/ada/sem_ch6.adb

@@ -3031,16 +3031,44 @@ package body Sem_Ch6 is
                --  We make two copies of the given spec, one for the new
                --  declaration, and one for the body.
 
-               --  This cannot be done for a compilation unit, which is not
-               --  in a context where we can insert a new spec.
-
                if No (Spec_Id)
                  and then GNATprove_Mode
+
+                 --  Under a debug flag until remaining issues are fixed
+
                  and then Debug_Flag_QQ
+
+                 --  Inlining does not apply during pre-analysis of code
+
                  and then Full_Analysis
+
+                 --  Inlining only applies to full bodies, not stubs
+
                  and then Nkind (N) /= N_Subprogram_Body_Stub
+
+                 --  Inlining only applies to bodies in the source code, not to
+                 --  those generated by the compiler. In particular, expression
+                 --  functions, whose body is generated by the compiler, are
+                 --  treated specially by GNATprove.
+
                  and then Comes_From_Source (Body_Id)
+
+                 --  This cannot be done for a compilation unit, which is not
+                 --  in a context where we can insert a new spec.
+
                  and then Is_List_Member (N)
+
+                 --  Inlining only applies to subprograms without contracts,
+                 --  as a contract is a sign that GNATprove should perform a
+                 --  modular analysis of the subprogram instead of a contextual
+                 --  analysis at each call site. The same test is performed in
+                 --  Inline.Can_Be_Inlined_In_GNATprove_Mode. It is repeated
+                 --  here in another form (because the contract has not
+                 --  been attached to the body) to avoid frontend errors in
+                 --  case pragmas are used instead of aspects, because the
+                 --  corresponding pragmas in the body would not be transferred
+                 --  to the spec, leading to legality errors.
+
                  and then not Body_Has_Contract
                then
                   declare

gcc/ada/sem_res.adb

@@ -10686,10 +10686,9 @@ package body Sem_Res is
       --  (In other contexts conversions cannot apply to literals).
 
       if In_Inlined_Body
-        and then
-          (Opnd_Type = Any_Character or else
-           Opnd_Type = Any_Integer   or else
-           Opnd_Type = Any_Real)
+        and then (Opnd_Type = Any_Character or else
+                  Opnd_Type = Any_Integer   or else
+                  Opnd_Type = Any_Real)
       then
          Set_Etype (Operand, Typ);
       end if;