[multiple changes]

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

	* checks.adb (Apply_Predicate_Check): If the expression is an
	aggregate that is the RHS of an assignment, apply the check to
	the LHS after the assignment, rather than to the aggregate. This
	is more efficient than creating a temporary for the aggregate,
	and prevents back-end crashes when the aggregate includes a
	dynamic "others' association.

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

	* sem_ch12.adb (Analyze_Instance_And_Renamings):
	Set variable to ignore SPARK_Mode in instance before the analysis
	of the generated package declaration.

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

	* sem_res.adb (Resolve_Call): Do not issue a
	message for calls inside expression function, unless body was
	seen and is candidate for inlining.

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

	* sem_aux.adb (Is_Generic_Formal): Handle properly formal packages.
	* sem_ch3.adb (Analyze_Declarations): In a generic subprogram
	body. do not freeze the formals of the generic unit.

2017-09-06  Gary Dismukes  <dismukes@adacore.com>

	* errout.adb (Error_Msg): Separate the
	treatment for warning vs. style messages in inlinings and
	instantiations. Prevents blowups on calls to Warn_Insertion for
	style messages, which should not be called in that case because
	Warning_Msg_Char is not set.

2017-09-06  Justin Squirek  <squirek@adacore.com>

	* sem_prag.adb (Check_VFA_Conflicts): Created
	to group all Volatile_Full_Access checks relating to other
	representation pragmas (Mark_Component_Or_Object): Created
	to centeralize the flagging of attributes for the record type
	component case, a pragma applied individually to a component, and
	the object case.
	(Process_Atomic_Independent_Shared_Volatile):
	Add propagation of certain pragmas to record components and move
	evaluation of VFA checks

From-SVN: r251793

gcc/ada/ChangeLog

 2017-09-06  Ed Schonberg  <schonberg@adacore.com>
 
+	* checks.adb (Apply_Predicate_Check): If the expression is an
+	aggregate that is the RHS of an assignment, apply the check to
+	the LHS after the assignment, rather than to the aggregate. This
+	is more efficient than creating a temporary for the aggregate,
+	and prevents back-end crashes when the aggregate includes a
+	dynamic "others' association.
+
+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch12.adb (Analyze_Instance_And_Renamings):
+	Set variable to ignore SPARK_Mode in instance before the analysis
+	of the generated package declaration.
+
+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Do not issue a
+	message for calls inside expression function, unless body was
+	seen and is candidate for inlining.
+
+2017-09-06  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_aux.adb (Is_Generic_Formal): Handle properly formal packages.
+	* sem_ch3.adb (Analyze_Declarations): In a generic subprogram
+	body. do not freeze the formals of the generic unit.
+
+2017-09-06  Gary Dismukes  <dismukes@adacore.com>
+
+	* errout.adb (Error_Msg): Separate the
+	treatment for warning vs. style messages in inlinings and
+	instantiations. Prevents blowups on calls to Warn_Insertion for
+	style messages, which should not be called in that case because
+	Warning_Msg_Char is not set.
+
+2017-09-06  Justin Squirek  <squirek@adacore.com>
+
+	* sem_prag.adb (Check_VFA_Conflicts): Created
+	to group all Volatile_Full_Access checks relating to other
+	representation pragmas (Mark_Component_Or_Object): Created
+	to centeralize the flagging of attributes for the record type
+	component case, a pragma applied individually to a component, and
+	the object case.
+	(Process_Atomic_Independent_Shared_Volatile):
+	Add propagation of certain pragmas to record components and move
+	evaluation of VFA checks
+
+2017-09-06  Ed Schonberg  <schonberg@adacore.com>
+
 	* sem_prag.adb (Check_Postcondition_Use_In_Inlined_Subprogram):
 	Do not warn on conditions that are not obeyed for Inline_Always
 	subprograms, when assertions are not enabled.

gcc/ada/checks.adb

@@ -2711,6 +2711,20 @@ package body Checks is
             --  it. We disable checks during its analysis, to prevent an
             --  infinite recursion.
 
+            --  If the prefix is an aggregate in an assignment, apply the
+            --  check to the LHS after assignment, rather than create a
+            --  redundant temporary. This is only necessary in rare cases
+            --  of array types (including strings) initialized with an
+            --  aggregate with an "others" clause, either coming from source
+            --  or generated by an Initialize_Scalars pragma.
+
+            elsif Nkind (N) = N_Aggregate
+              and then Nkind (Parent (N)) = N_Assignment_Statement
+            then
+               Insert_Action_After (Parent (N),
+                 Make_Predicate_Check
+                   (Typ, Duplicate_Subexpr (Name (Parent (N)))));
+
             else
                Insert_Action (N,
                  Make_Predicate_Check

gcc/ada/errout.adb

@@ -503,11 +503,16 @@ package body Errout is
                        ("info: in inlined body #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
 
-                  elsif Is_Warning_Msg or Is_Style_Msg then
+                  elsif Is_Warning_Msg then
                      Error_Msg_Internal
                        (Warn_Insertion & "in inlined body #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
 
+                  elsif Is_Style_Msg then
+                     Error_Msg_Internal
+                       ("style: in inlined body #",
+                        Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   else
                      Error_Msg_Internal
                        ("error in inlined body #",
@@ -522,11 +527,16 @@ package body Errout is
                        ("info: in instantiation #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
 
-                  elsif Is_Warning_Msg or else Is_Style_Msg then
+                  elsif Is_Warning_Msg then
                      Error_Msg_Internal
                        (Warn_Insertion & "in instantiation #",
                         Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
 
+                  elsif Is_Style_Msg then
+                     Error_Msg_Internal
+                       ("style: in instantiation #",
+                        Actual_Error_Loc, Flag_Location, Msg_Cont_Status);
+
                   else
                      Error_Msg_Internal
                        ("instantiation error #",

gcc/ada/sem_aux.adb

@@ -1053,9 +1053,13 @@ package body Sem_Aux is
 
          return
            Nkind_In (Kind, N_Formal_Object_Declaration,
-                           N_Formal_Package_Declaration,
                            N_Formal_Type_Declaration)
-             or else Is_Formal_Subprogram (E);
+             or else Is_Formal_Subprogram (E)
+
+             or else
+               (Ekind (E) = E_Package
+                 and then Nkind (Original_Node (Unit_Declaration_Node (E))) =
+                    N_Formal_Package_Declaration);
       end if;
    end Is_Generic_Formal;
 

gcc/ada/sem_ch12.adb

@@ -5089,6 +5089,15 @@ package body Sem_Ch12 is
             Set_Parent_Spec (Pack_Decl, Parent_Spec (N));
          end if;
 
+         --  If the context of the instance is subject to SPARK_Mode "off" or
+         --  the annotation is altogether missing, set the global flag which
+         --  signals Analyze_Pragma to ignore all SPARK_Mode pragmas within
+         --  the instance.
+
+         if SPARK_Mode /= On then
+            Ignore_SPARK_Mode_Pragmas_In_Instance := True;
+         end if;
+
          Analyze (Pack_Decl);
          Check_Formal_Packages (Pack_Id);
          Set_Is_Generic_Instance (Pack_Id, False);

gcc/ada/sem_ch3.adb

@@ -2649,8 +2649,26 @@ package body Sem_Ch3 is
                --  in order to perform visibility checks on delayed aspects.
 
                Adjust_Decl;
-               Freeze_All (First_Entity (Current_Scope), Decl);
-               Freeze_From := Last_Entity (Current_Scope);
+
+               --  If the current scope is a generic subprogram body. skip
+               --  the generic formal parameters that are not frozen here.
+
+               if Is_Subprogram (Current_Scope)
+                 and then Nkind (Unit_Declaration_Node (Current_Scope))
+                   = N_Generic_Subprogram_Declaration
+                 and then Present (First_Entity (Current_Scope))
+               then
+                  while Is_Generic_Formal (Freeze_From) loop
+                     Freeze_From := Next_Entity (Freeze_From);
+                  end loop;
+
+                  Freeze_All (Freeze_From, Decl);
+                  Freeze_From := Last_Entity (Current_Scope);
+
+               else
+                  Freeze_All (First_Entity (Current_Scope), Decl);
+                  Freeze_From := Last_Entity (Current_Scope);
+               end if;
 
             --  Current scope is a package specification
 

gcc/ada/sem_res.adb

@@ -6657,10 +6657,28 @@ package body Sem_Res is
 
             elsif Full_Analysis then
 
+               --  Do not inline calls inside expression functions, as this
+               --  would prevent interpreting them as logical formulas in
+               --  GNATprove. Only issue a message when the body has been seen,
+               --  otherwise this leads to spurious messages on callees that
+               --  are themselves expression functions.
+
+               if Present (Current_Subprogram)
+                    and then
+                  Is_Expression_Function_Or_Completion (Current_Subprogram)
+               then
+                  if Present (Body_Id)
+                    and then Present (Body_To_Inline (Nam_Decl))
+                  then
+                     Cannot_Inline
+                       ("cannot inline & (inside expression function)?",
+                        N, Nam_UA);
+                  end if;
+
                --  With the one-pass inlining technique, a call cannot be
                --  inlined if the corresponding body has not been seen yet.
 
-               if No (Body_Id) then
+               elsif No (Body_Id) then
                   Cannot_Inline
                     ("cannot inline & (body not seen yet)?", N, Nam_UA);
 
@@ -6671,18 +6689,6 @@ package body Sem_Res is
                elsif No (Body_To_Inline (Nam_Decl)) then
                   null;
 
-               --  Do not inline calls inside expression functions, as this
-               --  would prevent interpreting them as logical formulas in
-               --  GNATprove.
-
-               elsif Present (Current_Subprogram)
-                       and then
-                     Is_Expression_Function_Or_Completion (Current_Subprogram)
-               then
-                  Cannot_Inline
-                    ("cannot inline & (inside expression function)?",
-                     N, Nam_UA);
-
                --  Calls cannot be inlined inside potentially unevaluated
                --  expressions, as this would create complex actions inside
                --  expressions, that are not handled by GNATprove.