[multiple changes]

2017-09-06  Bob Duff  <duff@adacore.com>

	* a-comlin.ads, a-comlin.adb (Argument): Move the constraint
	check back to the body, because SPARK is not yet ready for
	"or else raise Constraint_Error".

2017-09-06  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch6.adb (Expand_Call_Helper): Replace call to null
	procedure by a single null statement, after evaluating the
	actuals that require it.

2017-09-06  Javier Miranda  <miranda@adacore.com>

	* exp_aggr.adb (Backend_Processing_Possible.Component_Check):
	Generating C code improve the code that checks the use of nested
	aggregates to initialize object declarations.

2017-09-06  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Derived_Type_Declaration): Detect
	violations of new rule SPARK RM 3.4(1).  Also refactor existing
	check to use the new function Find_Partial_View.

2017-09-06  Vincent Celier  <celier@adacore.com>

	* gnatcmd.adb: gnat ls -V -P... invokes gprls -V -P...	The code
	from the Prj hierarchy has been removed from the GNAT driver.

2017-09-06  Ed Schonberg  <schonberg@adacore.com>

	* sem_type.adb (Interface_Present_In_Ancestor): Within an
	expression function, or within a spec expression (default value,
	etc) a reference to an incomplete type is legal: legality of
	the operation will be checked when some related entity (type,
	object or subprogram) is frozen.

From-SVN: r251776

gcc/ada/ChangeLog

+2017-09-06  Bob Duff  <duff@adacore.com>
+
+	* a-comlin.ads, a-comlin.adb (Argument): Move the constraint
+	check back to the body, because SPARK is not yet ready for
+	"or else raise Constraint_Error".
+
+2017-09-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch6.adb (Expand_Call_Helper): Replace call to null
+	procedure by a single null statement, after evaluating the
+	actuals that require it.
+
+2017-09-06  Javier Miranda  <miranda@adacore.com>
+
+	* exp_aggr.adb (Backend_Processing_Possible.Component_Check):
+	Generating C code improve the code that checks the use of nested
+	aggregates to initialize object declarations.
+
+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch3.adb (Derived_Type_Declaration): Detect
+	violations of new rule SPARK RM 3.4(1).  Also refactor existing
+	check to use the new function Find_Partial_View.
+
+2017-09-06  Vincent Celier  <celier@adacore.com>
+
+	* gnatcmd.adb: gnat ls -V -P... invokes gprls -V -P...	The code
+	from the Prj hierarchy has been removed from the GNAT driver.
+
+2017-09-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_type.adb (Interface_Present_In_Ancestor): Within an
+	expression function, or within a spec expression (default value,
+	etc) a reference to an incomplete type is legal: legality of
+	the operation will be checked when some related entity (type,
+	object or subprogram) is frozen.
+
 2017-09-06  Gary Dismukes  <dismukes@adacore.com>
 
 	* exp_ch5.adb, s-diinio.ads, sem_ch4.adb, s-diflio.ads: Minor spelling

gcc/ada/a-comlin.adb

@@ -56,12 +56,19 @@ package body Ada.Command_Line is
    --------------
 
    function Argument (Number : Positive) return String is
+   begin
+      if Number > Argument_Count then
+         raise Constraint_Error;
+      end if;
+
+      declare
          Num : constant Positive :=
            (if Remove_Args = null then Number else Remove_Args (Number));
          Arg : aliased String (1 .. Len_Arg (Num));
       begin
          Fill_Arg (Arg'Address, Num);
          return Arg;
+      end;
    end Argument;
 
    --------------------

gcc/ada/a-comlin.ads

@@ -43,8 +43,14 @@ package Ada.Command_Line is
    --
    --  In GNAT: Corresponds to (argc - 1) in C.
 
+   pragma Assertion_Policy (Pre => Ignore);
+   --  We need to ignore the precondition of Argument, below, so that we don't
+   --  raise Assertion_Error. The body raises Constraint_Error. It would be
+   --  cleaner to add "or else raise Constraint_Error" to the precondition, but
+   --  SPARK does not yet support raise expressions.
+
    function Argument (Number : Positive) return String with
-      Pre => Number <= Argument_Count or else raise Constraint_Error;
+      Pre => Number <= Argument_Count;
    --  If the external execution environment supports passing arguments to
    --  a program, then Argument returns an implementation-defined value
    --  corresponding to the argument at relative position Number. If Number

gcc/ada/exp_aggr.adb

@@ -644,16 +644,28 @@ package body Exp_Aggr is
             return False;
          end if;
 
-         --  Checks 11: (part of an object declaration)
+         --  Checks 11: The C code generator cannot handle aggregates that
+         --  are not part of an object declaration.
 
-         if Modify_Tree_For_C
-           and then Nkind (Parent (N)) /= N_Object_Declaration
-           and then
-             (Nkind (Parent (N)) /= N_Qualified_Expression
-               or else Nkind (Parent (Parent (N))) /= N_Object_Declaration)
-         then
+         if Modify_Tree_For_C then
+            declare
+               Par : Node_Id := Parent (N);
+
+            begin
+               --  Skip enclosing nested aggregates and their qualified
+               --  expressions
+
+               while Nkind (Par) = N_Aggregate
+                 or else Nkind (Par) = N_Qualified_Expression
+               loop
+                  Par := Parent (Par);
+               end loop;
+
+               if Nkind (Par) /= N_Object_Declaration then
                   return False;
                end if;
+            end;
+         end if;
 
          --  Checks on components
 

gcc/ada/exp_ch6.adb

@@ -3951,6 +3951,20 @@ package body Exp_Ch6 is
               Unchecked_Convert_To
                 (RTE (RE_Address), Relocate_Node (First_Actual (Call_Node))));
             return;
+
+         --  A call to a null procedure is replaced by a null statement, but
+         --  we are not allowed to ignore possible side effects of the call,
+         --  so we make sure that actuals are evaluated.
+
+         elsif Is_Null_Procedure (Subp) then
+            Actual := First_Actual (Call_Node);
+            while Present (Actual) loop
+               Remove_Side_Effects (Actual);
+               Next_Actual (Actual);
+            end loop;
+
+            Rewrite (Call_Node, Make_Null_Statement (Loc));
+            return;
          end if;
 
          --  Handle inlining. No action needed if the subprogram is not inlined

gcc/ada/sem_ch3.adb

@@ -16241,6 +16241,9 @@ package body Sem_Ch3 is
       --  Check whether the parent type is a generic formal, or derives
       --  directly or indirectly from one.
 
+      function Find_Partial_View (T : Entity_Id) return Entity_Id;
+      --  Return the partial view for a type entity T, when there is one
+
       ------------------------
       -- Comes_From_Generic --
       ------------------------
@@ -16267,6 +16270,28 @@ package body Sem_Ch3 is
          end if;
       end Comes_From_Generic;
 
+      -----------------------
+      -- Find_Partial_View --
+      -----------------------
+
+      function Find_Partial_View (T : Entity_Id) return Entity_Id is
+         Partial_View : Entity_Id;
+
+      begin
+         --  Look for the associated private type declaration
+
+         Partial_View := First_Entity (Scope (T));
+         loop
+            exit when No (Partial_View)
+              or else (Has_Private_Declaration (Partial_View)
+                        and then Full_View (Partial_View) = T);
+
+            Next_Entity (Partial_View);
+         end loop;
+
+         return Partial_View;
+      end Find_Partial_View;
+
       --  Local variables
 
       Def          : constant Node_Id := Type_Definition (N);
@@ -16281,6 +16306,28 @@ package body Sem_Ch3 is
    begin
       Parent_Type := Find_Type_Of_Subtype_Indic (Indic);
 
+      if SPARK_Mode = On
+        and then Is_Tagged_Type (Parent_Type)
+      then
+         declare
+            Partial_View : constant Entity_Id :=
+              Find_Partial_View (Parent_Type);
+
+         begin
+            --  If the partial view was not found then the parent type is not a
+            --  private type. Otherwise check that the partial view is declared
+            --  as tagged.
+
+            if Present (Partial_View)
+              and then not Is_Tagged_Type (Partial_View)
+            then
+               Error_Msg_NE ("cannot derive from & declared as "
+                             & "untagged private (SPARK RM 3.4(1))",
+                             N, Partial_View);
+            end if;
+         end;
+      end if;
+
       --  Ada 2005 (AI-251): In case of interface derivation check that the
       --  parent is also an interface.
 
@@ -16468,14 +16515,7 @@ package body Sem_Ch3 is
          begin
             --  Look for the associated private type declaration
 
-            Partial_View := First_Entity (Current_Scope);
-            loop
-               exit when No (Partial_View)
-                 or else (Has_Private_Declaration (Partial_View)
-                           and then Full_View (Partial_View) = T);
-
-               Next_Entity (Partial_View);
-            end loop;
+            Partial_View := Find_Partial_View (T);
 
             --  If the partial view was not found then the source code has
             --  errors and the transformation is not needed.

gcc/ada/sem_type.adb

@@ -2704,9 +2704,18 @@ package body Sem_Type is
          if Present (Full_View (Target_Typ)) then
             Target_Typ := Full_View (Target_Typ);
          else
+            --  In a spec expression or in an expression function, the use of
+            --  an incomplete type is legal; legality of the conversion will be
+            --  checked at freeze point of related entity.
+
+            if In_Spec_Expression then
+               return True;
+
+            else
                pragma Assert (Present (Non_Limited_View (Target_Typ)));
                Target_Typ := Non_Limited_View (Target_Typ);
             end if;
+         end if;
 
          --  Protect the front end against previously detected errors