[multiple changes]

2014-02-06  Arnaud Charlet  <charlet@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Rewrite as a null statement
	in GNATprove_Mode.

2014-02-06  Robert Dewar  <dewar@adacore.com>

	* einfo.ads, einfo.adb (Is_Discriminant_Check_Function): New flag.
	* exp_ch3.adb (Build_Dcheck_Function): Set
	Is_Discriminant_Check_Function.

2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Is_Subprogram_Call): Inspect
	the original tree in certain cases where a construct has been
	factored out and replaced by a reference to a temporary.

2014-02-06  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb (Process_Full_View): Fix typo in the order of
	parameters when propagating predicate function to full view.
	(Find_Type_Of_Object): Freeze base type of object type to catch
	premature use of discriminated private type without a full view.

From-SVN: r207535

gcc/ada/ChangeLog

+2014-02-06  Arnaud Charlet  <charlet@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Rewrite as a null statement
+	in GNATprove_Mode.
+
+2014-02-06  Robert Dewar  <dewar@adacore.com>
+
+	* einfo.ads, einfo.adb (Is_Discriminant_Check_Function): New flag.
+	* exp_ch3.adb (Build_Dcheck_Function): Set
+	Is_Discriminant_Check_Function.
+
+2014-02-06  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch7.adb (Is_Subprogram_Call): Inspect
+	the original tree in certain cases where a construct has been
+	factored out and replaced by a reference to a temporary.
+
+2014-02-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb (Process_Full_View): Fix typo in the order of
+	parameters when propagating predicate function to full view.
+	(Find_Type_Of_Object): Freeze base type of object type to catch
+	premature use of discriminated private type without a full view.
+
 2014-02-06  Robert Dewar  <dewar@adacore.com>
 
 	* sprint.adb: Minor reformatting.

gcc/ada/einfo.adb

@@ -101,6 +101,7 @@ package body Einfo is
    --    Entry_Component                 Node11
    --    Enumeration_Pos                 Uint11
    --    Generic_Homonym                 Node11
+   --    Last_Aggregate_Assignment       Node11
    --    Protected_Body_Subprogram       Node11
    --    Block_Node                      Node11
 
@@ -552,6 +553,7 @@ package body Einfo is
    --    Has_Delayed_Rep_Aspects         Flag261
    --    May_Inherit_Delayed_Rep_Aspects Flag262
    --    Has_Visible_Refinement          Flag263
+   --    Is_Discriminant_Check_Function  Flag264
    --    SPARK_Pragma_Inherited          Flag265
    --    SPARK_Aux_Pragma_Inherited      Flag266
 
@@ -559,7 +561,6 @@ package body Einfo is
    --    (unused)                        Flag2
    --    (unused)                        Flag3
 
-   --    (unused)                        Flag264
    --    (unused)                        Flag267
    --    (unused)                        Flag268
    --    (unused)                        Flag269
@@ -1962,6 +1963,11 @@ package body Einfo is
       return Flag176 (Id);
    end Is_Discrim_SO_Function;
 
+   function Is_Discriminant_Check_Function (Id : E) return B is
+   begin
+      return Flag264 (Id);
+   end Is_Discriminant_Check_Function;
+
    function Is_Dispatch_Table_Entity (Id : E) return B is
    begin
       return Flag234 (Id);
@@ -2395,6 +2401,12 @@ package body Einfo is
       return Flag207 (Id);
    end Known_To_Have_Preelab_Init;
 
+   function Last_Aggregate_Assignment (Id : E) return N is
+   begin
+      pragma Assert (Ekind (Id) = E_Variable);
+      return Node11 (Id);
+   end Last_Aggregate_Assignment;
+
    function Last_Assignment (Id : E) return N is
    begin
       pragma Assert (Is_Assignable (Id));
@@ -4660,6 +4672,11 @@ package body Einfo is
       Set_Flag176 (Id, V);
    end Set_Is_Discrim_SO_Function;
 
+   procedure Set_Is_Discriminant_Check_Function (Id : E; V : B := True) is
+   begin
+      Set_Flag264 (Id, V);
+   end Set_Is_Discriminant_Check_Function;
+
    procedure Set_Is_Dispatch_Table_Entity (Id : E; V : B := True) is
    begin
       Set_Flag234 (Id, V);
@@ -5110,6 +5127,12 @@ package body Einfo is
       Set_Flag207 (Id, V);
    end Set_Known_To_Have_Preelab_Init;
 
+   procedure Set_Last_Aggregate_Assignment (Id : E; V : N) is
+   begin
+      pragma Assert (Ekind (Id) = E_Variable);
+      Set_Node11 (Id, V);
+   end Set_Last_Aggregate_Assignment;
+
    procedure Set_Last_Assignment (Id : E; V : N) is
    begin
       pragma Assert (Is_Assignable (Id));
@@ -8204,6 +8227,7 @@ package body Einfo is
       W ("Is_Controlling_Formal",           Flag97  (Id));
       W ("Is_Descendent_Of_Address",        Flag223 (Id));
       W ("Is_Discrim_SO_Function",          Flag176 (Id));
+      W ("Is_Discriminant_Check_Function",  Flag264 (Id));
       W ("Is_Dispatch_Table_Entity",        Flag234 (Id));
       W ("Is_Dispatching_Operation",        Flag6   (Id));
       W ("Is_Eliminated",                   Flag124 (Id));
@@ -8621,6 +8645,9 @@ package body Einfo is
          when E_Generic_Package                            =>
             Write_Str ("Generic_Homonym");
 
+         when E_Variable                                   =>
+            Write_Str ("Last_Aggregate_Assignment");
+
          when E_Function                                   |
               E_Procedure                                  |
               E_Entry                                      |

gcc/ada/einfo.ads

@@ -2228,6 +2228,10 @@ package Einfo is
 --       Defined in all entities. Set only in E_Function entities that Layout
 --       creates to compute discriminant-dependent dynamic size/offset values.
 
+--    Is_Discriminant_Check_Function (Flag264)
+--       Defined in all entities. Set only in E_Function entities for functions
+--       created to do discriminant checks.
+
 --    Is_Discriminal (synthesized)
 --       Applies to all entities, true for renamings of discriminants. Such
 --       entities appear as constants or IN parameters.
@@ -3018,6 +3022,12 @@ package Einfo is
 --       initialization, it may or may not be set if the type does have
 --       preelaborable initialization.
 
+--    Last_Aggregate_Assignment (Node11)
+--       Applies to controlled variables initialized by an aggregate. Points to
+--       the last statement associated with the expansion of the aggregate. The
+--       attribute is used by the finalization machinery when marking an object
+--       as successfully initialized.
+
 --    Last_Assignment (Node26)
 --       Defined in entities for variables, and OUT or IN OUT formals. Set for
 --       a local variable or formal to point to the left side of an assignment
@@ -4983,6 +4993,7 @@ package Einfo is
    --    Is_Completely_Hidden                (Flag103)
    --    Is_Descendent_Of_Address            (Flag223)
    --    Is_Discrim_SO_Function              (Flag176)
+   --    Is_Discriminant_Check_Function      (Flag264)
    --    Is_Dispatch_Table_Entity            (Flag234)
    --    Is_Dispatching_Operation            (Flag6)
    --    Is_Entry_Formal                     (Flag52)
@@ -5497,6 +5508,7 @@ package Einfo is
    --    Is_Called                           (Flag102)  (non-generic case only)
    --    Is_Constructor                      (Flag76)
    --    Is_Discrim_SO_Function              (Flag176)
+   --    Is_Discriminant_Check_Function      (Flag264)
    --    Is_Eliminated                       (Flag124)
    --    Is_Instantiated                     (Flag126)  (generic case only)
    --    Is_Intrinsic_Subprogram             (Flag64)
@@ -5983,6 +5995,7 @@ package Einfo is
    --    Hiding_Loop_Variable                (Node8)
    --    Current_Value                       (Node9)
    --    Encapsulating_State                 (Node10)
+   --    Last_Aggregate_Assignment           (Node11)
    --    Esize                               (Uint12)
    --    Extra_Accessibility                 (Node13)
    --    Alignment                           (Uint14)
@@ -6487,6 +6500,7 @@ package Einfo is
    function Is_Controlling_Formal               (Id : E) return B;
    function Is_Descendent_Of_Address            (Id : E) return B;
    function Is_Discrim_SO_Function              (Id : E) return B;
+   function Is_Discriminant_Check_Function      (Id : E) return B;
    function Is_Dispatch_Table_Entity            (Id : E) return B;
    function Is_Dispatching_Operation            (Id : E) return B;
    function Is_Eliminated                       (Id : E) return B;
@@ -6563,6 +6577,7 @@ package Einfo is
    function Kill_Elaboration_Checks             (Id : E) return B;
    function Kill_Range_Checks                   (Id : E) return B;
    function Known_To_Have_Preelab_Init          (Id : E) return B;
+   function Last_Aggregate_Assignment           (Id : E) return N;
    function Last_Assignment                     (Id : E) return N;
    function Last_Entity                         (Id : E) return E;
    function Limited_View                        (Id : E) return E;
@@ -7107,6 +7122,7 @@ package Einfo is
    procedure Set_Is_Controlling_Formal           (Id : E; V : B := True);
    procedure Set_Is_Descendent_Of_Address        (Id : E; V : B := True);
    procedure Set_Is_Discrim_SO_Function          (Id : E; V : B := True);
+   procedure Set_Is_Discriminant_Check_Function  (Id : E; V : B := True);
    procedure Set_Is_Dispatch_Table_Entity        (Id : E; V : B := True);
    procedure Set_Is_Dispatching_Operation        (Id : E; V : B := True);
    procedure Set_Is_Eliminated                   (Id : E; V : B := True);
@@ -7187,6 +7203,7 @@ package Einfo is
    procedure Set_Kill_Elaboration_Checks         (Id : E; V : B := True);
    procedure Set_Kill_Range_Checks               (Id : E; V : B := True);
    procedure Set_Known_To_Have_Preelab_Init      (Id : E; V : B := True);
+   procedure Set_Last_Aggregate_Assignment       (Id : E; V : N);
    procedure Set_Last_Assignment                 (Id : E; V : N);
    procedure Set_Last_Entity                     (Id : E; V : E);
    procedure Set_Limited_View                    (Id : E; V : E);
@@ -7853,6 +7870,7 @@ package Einfo is
    pragma Inline (Is_Discrete_Or_Fixed_Point_Type);
    pragma Inline (Is_Discrete_Type);
    pragma Inline (Is_Discrim_SO_Function);
+   pragma Inline (Is_Discriminant_Check_Function);
    pragma Inline (Is_Dispatch_Table_Entity);
    pragma Inline (Is_Dispatching_Operation);
    pragma Inline (Is_Elementary_Type);
@@ -7959,6 +7977,7 @@ package Einfo is
    pragma Inline (Kill_Elaboration_Checks);
    pragma Inline (Kill_Range_Checks);
    pragma Inline (Known_To_Have_Preelab_Init);
+   pragma Inline (Last_Aggregate_Assignment);
    pragma Inline (Last_Assignment);
    pragma Inline (Last_Entity);
    pragma Inline (Limited_View);
@@ -8306,6 +8325,7 @@ package Einfo is
    pragma Inline (Set_Is_Controlling_Formal);
    pragma Inline (Set_Is_Descendent_Of_Address);
    pragma Inline (Set_Is_Discrim_SO_Function);
+   pragma Inline (Set_Is_Discriminant_Check_Function);
    pragma Inline (Set_Is_Dispatch_Table_Entity);
    pragma Inline (Set_Is_Dispatching_Operation);
    pragma Inline (Set_Is_Eliminated);
@@ -8386,6 +8406,7 @@ package Einfo is
    pragma Inline (Set_Kill_Elaboration_Checks);
    pragma Inline (Set_Kill_Range_Checks);
    pragma Inline (Set_Known_To_Have_Preelab_Init);
+   pragma Inline (Set_Last_Aggregate_Assignment);
    pragma Inline (Set_Last_Assignment);
    pragma Inline (Set_Last_Entity);
    pragma Inline (Set_Limited_View);

gcc/ada/exp_ch3.adb

@@ -1070,6 +1070,7 @@ package body Exp_Ch3 is
          Func_Id :=
            Make_Defining_Identifier (Loc,
              Chars => New_External_Name (Chars (Rec_Id), 'D', Sequence));
+         Set_Is_Discriminant_Check_Function (Func_Id);
 
          Spec_Node := New_Node (N_Function_Specification, Loc);
          Set_Defining_Unit_Name (Spec_Node, Func_Id);

gcc/ada/exp_ch7.adb

@@ -4439,20 +4439,28 @@ package body Exp_Ch7 is
 
          function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
          begin
-            --  Aggregates are usually rewritten into component by component
-            --  assignments and replaced by a reference to a temporary in the
-            --  original tree. Peek in the aggregate to detect function calls.
+            --  Complex constructs are factored out by the expander and their
+            --  occurrences are replaced with references to temporaries. Due to
+            --  this expansion activity, inspect the original tree to detect
+            --  subprogram calls.
 
-            if Nkind (N) = N_Identifier
-              and then Nkind_In (Original_Node (N), N_Aggregate,
-                                                    N_Extension_Aggregate)
-            then
+            if Nkind (N) = N_Identifier and then Original_Node (N) /= N then
                Detect_Subprogram_Call (Original_Node (N));
-               return OK;
 
-            --  Detect a call to a function that returns on the secondary stack
+               --  The original construct contains a subprogram call, there is
+               --  no point in continuing the tree traversal.
+
+               if Must_Hook then
+                  return Abandon;
+               else
+                  return OK;
+               end if;
+
+            --  The original construct contains a subprogram call, there is no
+            --  point in continuing the tree traversal.
 
             elsif Nkind (N) = N_Object_Declaration
+              and then Present (Expression (N))
               and then Nkind (Original_Node (Expression (N))) = N_Function_Call
             then
                Must_Hook := True;

gcc/ada/sem_ch3.adb

@@ -15772,8 +15772,12 @@ package body Sem_Ch3 is
            and then No (Expression (P))
          then
             null;
+
+         --  Here we freeze the base type of object type to catch premature use
+         --  of discriminated private type without a full view.
+
          else
-            Insert_Actions (Obj_Def, Freeze_Entity (T, P));
+            Insert_Actions (Obj_Def, Freeze_Entity (Base_Type (T), P));
          end if;
 
       --  Ada 2005 AI-406: the object definition in an object declaration
@@ -18675,7 +18679,7 @@ package body Sem_Ch3 is
          end;
       end if;
 
-      --  Ada 2005 AI 161: Check preelaboratable initialization consistency
+      --  Ada 2005 AI 161: Check preelaborable initialization consistency
 
       if Known_To_Have_Preelab_Init (Priv_T) then
 
@@ -18737,10 +18741,16 @@ package body Sem_Ch3 is
          Set_Has_Inheritable_Invariants (Full_T);
       end if;
 
-      --  Propagate predicates to full type
+      --  Propagate predicates to full type, and predicate function if already
+      --  defined. It is not clear that this can actually happen? the partial
+      --  view cannot be frozen yet, and the predicate function has not been
+      --  built. Still it is a cheap check and seems safer to make it.
 
       if Has_Predicates (Priv_T) then
-         Set_Predicate_Function (Priv_T, Predicate_Function (Full_T));
+         if Present (Predicate_Function (Priv_T)) then
+            Set_Predicate_Function (Full_T, Predicate_Function (Priv_T));
+         end if;
+
          Set_Has_Predicates (Full_T);
       end if;
    end Process_Full_View;

gcc/ada/sem_prag.adb

@@ -12603,13 +12603,20 @@ package body Sem_Prag is
                Freeze_Before (N, Entity (Name (Call)));
             end if;
 
-            Rewrite (N, Make_Implicit_If_Statement (N,
-              Condition => Cond,
-                 Then_Statements => New_List (
-                   Make_Block_Statement (Loc,
-                     Handled_Statement_Sequence =>
-                       Make_Handled_Sequence_Of_Statements (Loc,
-                         Statements => New_List (Relocate_Node (Call)))))));
+            --  Ignore pragma Debug in GNATprove mode
+
+            if GNATprove_Mode then
+               Rewrite (N, Make_Null_Statement (Loc));
+            else
+               Rewrite (N, Make_Implicit_If_Statement (N,
+                 Condition => Cond,
+                    Then_Statements => New_List (
+                      Make_Block_Statement (Loc,
+                        Handled_Statement_Sequence =>
+                          Make_Handled_Sequence_Of_Statements (Loc,
+                            Statements => New_List (Relocate_Node (Call)))))));
+            end if;
+
             Analyze (N);
          end Debug;