[multiple changes]

2015-10-27  Javier Miranda  <miranda@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve previous patch.

2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch12.adb (Analyze_Formal_Package_Declaration): Code cleanup. Set
	and restore the value of global flag Ignore_Pragma_SPARK_Mode. A
	formal package declaration acts as a package instantation with
	respect to SPARK_Mode legality.

2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Constituent_Usage): Use
	logical operators rather than short circuit operators. Emit an
	error when a state with visible refinement is not refined.
	* snames.ads-tmpl: Add names for detecting
	predefined potentially blocking subprograms.

2015-10-27  Arnaud Charlet  <charlet@adacore.com>

	* exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Revert previous
	change.
	(Expand_Array_Aggregate): Rewrite previous change here
	as done for other non GCC back-ends.
	(Build_Record_Aggr_Code): Add special case.

From-SVN: r229414

gcc/ada/ChangeLog

+2015-10-27  Javier Miranda  <miranda@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve previous patch.
+
+2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch12.adb (Analyze_Formal_Package_Declaration): Code cleanup. Set
+	and restore the value of global flag Ignore_Pragma_SPARK_Mode. A
+	formal package declaration acts as a package instantation with
+	respect to SPARK_Mode legality.
+
+2015-10-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Check_Constituent_Usage): Use
+	logical operators rather than short circuit operators. Emit an
+	error when a state with visible refinement is not refined.
+	* snames.ads-tmpl: Add names for detecting
+	predefined potentially blocking subprograms.
+
+2015-10-27  Arnaud Charlet  <charlet@adacore.com>
+
+	* exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Revert previous
+	change.
+	(Expand_Array_Aggregate): Rewrite previous change here
+	as done for other non GCC back-ends.
+	(Build_Record_Aggr_Code): Add special case.
+
 2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Add_Item_To_Name_Buffer): Update the comment on usage.

gcc/ada/exp_aggr.adb

@@ -2924,13 +2924,33 @@ package body Exp_Aggr is
                   end if;
                end if;
 
-               Instr :=
-                 Make_OK_Assignment_Statement (Loc,
-                   Name       => Comp_Expr,
-                   Expression => Expr_Q);
+               if Generate_C_Code
+                 and then Nkind (Expr_Q) = N_Aggregate
+                 and then Is_Array_Type (Etype (Expr_Q))
+                 and then Present (First_Index (Etype (Expr_Q)))
+               then
+                  declare
+                     Expr_Q_Type : constant Node_Id := Etype (Expr_Q);
+                  begin
+                     Append_List_To (L,
+                       Build_Array_Aggr_Code
+                         (N           => Expr_Q,
+                          Ctype       => Component_Type (Expr_Q_Type),
+                          Index       => First_Index (Expr_Q_Type),
+                          Into        => Comp_Expr,
+                          Scalar_Comp => Is_Scalar_Type
+                                           (Component_Type (Expr_Q_Type))));
+                  end;
+
+               else
+                  Instr :=
+                    Make_OK_Assignment_Statement (Loc,
+                      Name       => Comp_Expr,
+                      Expression => Expr_Q);
 
-               Set_No_Ctrl_Actions (Instr);
-               Append_To (L, Instr);
+                  Set_No_Ctrl_Actions (Instr);
+                  Append_To (L, Instr);
+               end if;
 
                --  Adjust the tag if tagged (because of possible view
                --  conversions), unless compiling for a VM where tags are
@@ -4105,8 +4125,6 @@ package body Exp_Aggr is
       --  Backend processing by Gigi/gcc is possible only if all the following
       --  conditions are met:
 
-      --    0. We are not generating C code
-
       --    1. N consists of a single OTHERS choice, possibly recursively
 
       --    2. The array type is not packed
@@ -4137,10 +4155,6 @@ package body Exp_Aggr is
          Nunits    : Nat;
 
       begin
-         if Generate_C_Code then
-            return False;
-         end if;
-
          --  Recurse as far as possible to find the innermost component type
 
          Ctyp := Etype (N);
@@ -5476,7 +5490,8 @@ package body Exp_Aggr is
 
          if (In_Place_Assign_OK_For_Declaration or else Maybe_In_Place_OK)
            and then not AAMP_On_Target
-           and then not Generate_SCIL
+           and then not CodePeer_Mode
+           and then not Generate_C_Code
            and then not Possible_Bit_Aligned_Component (Target)
            and then not Is_Possibly_Unaligned_Slice (Target)
            and then Aggr_Assignment_OK_For_Backend (N)

gcc/ada/sem_ch12.adb

@@ -2379,22 +2379,17 @@ package body Sem_Ch12 is
    ----------------------------------------
 
    procedure Analyze_Formal_Package_Declaration (N : Node_Id) is
-      Loc              : constant Source_Ptr := Sloc (N);
-      Pack_Id          : constant Entity_Id  := Defining_Identifier (N);
-      Formal           : Entity_Id;
-      Gen_Id           : constant Node_Id    := Name (N);
-      Gen_Decl         : Node_Id;
-      Gen_Unit         : Entity_Id;
-      New_N            : Node_Id;
-      Parent_Installed : Boolean := False;
-      Renaming         : Node_Id;
-      Parent_Instance  : Entity_Id;
-      Renaming_In_Par  : Entity_Id;
-      Associations     : Boolean := True;
+      Gen_Id   : constant Node_Id    := Name (N);
+      Loc      : constant Source_Ptr := Sloc (N);
+      Pack_Id  : constant Entity_Id  := Defining_Identifier (N);
+      Formal   : Entity_Id;
+      Gen_Decl : Node_Id;
+      Gen_Unit : Entity_Id;
+      Renaming : Node_Id;
 
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
-      --  to match the visibility of the formal type
+      --  to match the visibility of the formal type.
 
       function Build_Local_Package return Node_Id;
       --  The formal package is rewritten so that its parameters are replaced
@@ -2506,6 +2501,17 @@ package body Sem_Ch12 is
          return Pack_Decl;
       end Build_Local_Package;
 
+      --  Local variables
+
+      Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
+      --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
+
+      Associations     : Boolean := True;
+      New_N            : Node_Id;
+      Parent_Installed : Boolean := False;
+      Parent_Instance  : Entity_Id;
+      Renaming_In_Par  : Entity_Id;
+
    --  Start of processing for Analyze_Formal_Package_Declaration
 
    begin
@@ -2605,19 +2611,18 @@ package body Sem_Ch12 is
       Formal := New_Copy (Pack_Id);
       Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment);
 
-      begin
-         --  Make local generic without formals. The formals will be replaced
-         --  with internal declarations.
+      --  Make local generic without formals. The formals will be replaced with
+      --  internal declarations.
 
+      begin
          New_N := Build_Local_Package;
 
-         --  If there are errors in the parameter list, Analyze_Associations
-         --  raises Instantiation_Error. Patch the declaration to prevent
-         --  further exception propagation.
+      --  If there are errors in the parameter list, Analyze_Associations
+      --  raises Instantiation_Error. Patch the declaration to prevent further
+      --  exception propagation.
 
       exception
          when Instantiation_Error =>
-
             Enter_Name (Formal);
             Set_Ekind  (Formal, E_Variable);
             Set_Etype  (Formal, Any_Type);
@@ -2669,6 +2674,15 @@ package body Sem_Ch12 is
          Append_Entity (Renaming_In_Par, Parent_Instance);
       end if;
 
+      --  A formal package declaration behaves as a package instantiation with
+      --  respect to SPARK_Mode "off". If the annotation is "off" or altogether
+      --  missing, set the global flag which signals Analyze_Pragma to ingnore
+      --  all SPARK_Mode pragmas within the generic_package_name.
+
+      if SPARK_Mode /= On then
+         Ignore_Pragma_SPARK_Mode := True;
+      end if;
+
       Analyze (Specification (N));
 
       --  The formals for which associations are provided are not visible
@@ -2714,8 +2728,8 @@ package body Sem_Ch12 is
 
       Set_Has_Completion (Formal, True);
 
-      --  Add semantic information to the original defining identifier.
-      --  for ASIS use.
+      --  Add semantic information to the original defining identifier for ASIS
+      --  use.
 
       Set_Ekind (Pack_Id, E_Package);
       Set_Etype (Pack_Id, Standard_Void_Type);
@@ -2726,6 +2740,8 @@ package body Sem_Ch12 is
       if Has_Aspects (N) then
          Analyze_Aspect_Specifications (N, Pack_Id);
       end if;
+
+      Ignore_Pragma_SPARK_Mode := Save_IPSM;
    end Analyze_Formal_Package_Declaration;
 
    ---------------------------------

gcc/ada/sem_ch6.adb

@@ -4062,7 +4062,7 @@ package body Sem_Ch6 is
       --  that carries the return value.
 
       if Present (Cloned_Body_For_C) then
-         Replace (N,
+         Rewrite (N,
            Build_Procedure_Body_Form (Spec_Id, Cloned_Body_For_C));
          Analyze (N);
       end if;

gcc/ada/sem_prag.adb

@@ -24184,15 +24184,24 @@ package body Sem_Prag is
             --  A pair of one Input and one Output constituent is a valid
             --  completion.
 
-            elsif In_Seen and then Out_Seen then
+            elsif In_Seen and Out_Seen then
                null;
 
             --  A single Output constituent is a valid completion only when
             --  some of the other constituents are missing (SPARK RM 7.2.4(5)).
 
-            elsif Has_Missing and then Out_Seen then
+            elsif Out_Seen and Has_Missing then
                null;
 
+            --  The state lacks a completion
+
+            elsif not In_Seen and not In_Out_Seen and not Out_Seen then
+               SPARK_Msg_NE
+                 ("missing global refinement of state &", N, State_Id);
+
+            --  Otherwise the state has a malformed completion where at least
+            --  one of the constituents has a different mode.
+
             else
                SPARK_Msg_NE
                  ("global refinement of state & redefines the mode of its "

gcc/ada/snames.ads-tmpl

@@ -261,6 +261,29 @@ package Snames is
    Name_Wide_Text_IO                   : constant Name_Id := N + $;
    Name_Wide_Wide_Text_IO              : constant Name_Id := N + $;
 
+   --  Names for detecting predefined potentially blocking subprograms
+
+   Name_Abort_Task                     : constant Name_Id := N + $;
+   Name_Bounded_IO                     : constant Name_Id := N + $;
+   Name_C_Streams                      : constant Name_Id := N + $;
+   Name_Complex_IO                     : constant Name_Id := N + $;
+   Name_Directories                    : constant Name_Id := N + $;
+   Name_Direct_IO                      : constant Name_Id := N + $;
+   Name_Dispatching                    : constant Name_Id := N + $;
+   Name_Editing                        : constant Name_Id := N + $;
+   Name_EDF                            : constant Name_Id := N + $;
+   Name_Reset_Standard_Files           : constant Name_Id := N + $;
+   Name_Sequential_IO                  : constant Name_Id := N + $;
+   Name_Streams                        : constant Name_Id := N + $;
+   Name_Suspend_Until_True             : constant Name_Id := N + $;
+   Name_Suspend_Until_True_And_Set_Deadline : constant Name_Id := N + $;
+   Name_Synchronous_Barriers           : constant Name_Id := N + $;
+   Name_Task_Identification            : constant Name_Id := N + $;
+   Name_Text_Streams                   : constant Name_Id := N + $;
+   Name_Unbounded_IO                   : constant Name_Id := N + $;
+   Name_Wait_For_Release               : constant Name_Id := N + $;
+   Name_Yield                          : constant Name_Id := N + $;
+
    --  Names of implementations of the distributed systems annex
 
    First_PCS_Name                      : constant Name_Id := N + $;