[multiple changes]

2015-10-26  Claire Dross  <dross@adacore.com>

	* sem_aux.ads (Number_Components): Can return 0 when called on
	an empty record.

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

	* contracts.adb (Analyze_Subprogram_Body_Contract): Use
	Unique_Defining_Entity instead of Corresponding_Spec_Of.
	* einfo.adb SPARK_Pragma and SPARK_Aux_Pragma are now Node40 and
	Node41 respectively.
	(SPARK_Aux_Pragma): Update the assertion and node querry.
	(SPARK_Aux_Pragma_Inherited): Update the assertion and node query.
	(SPARK_Pragma): Update the assertion and node query.
	(SPARK_Pragma_Inherited): Update the assertion and node query.
	(Set_SPARK_Aux_Pragma): Update the assertion and node setting.
	(Set_SPARK_Aux_Pragma_Inherited): Update the assertion and node setting.
	(Set_SPARK_Pragma): Update the assertion and node setting.
	(Set_SPARK_Pragma_Inherited): Update the assertion and node setting.
	(Write_Field32_Name): Remove the output for SPARK_Pragma.
	(Write_Field33_Name): Remove the output for SPARK_Aux_Pragma.
	(Write_Field40_Name): Add output for SPARK_Pragma.
	(Write_Field41_Name): Add output for SPARK_Aux_Pragma.
	* einfo.ads Rewrite the documentation on attributes
	SPARK_Pragma, SPARK_Aux_Pragma, SPARK_Pragma_Inherited and
	SPARK_Aux_Pragma_Inherited. Update their uses in nodes.
	* exp_ch4.adb (Create_Anonymous_Master): Use
	Unique_Defining_Entity instead of Corresponding_Spec_Of.
	* exp_ch9.adb (Expand_Entry_Declaration): Mark the barrier
	function as such.
	(Expand_N_Task_Body): Mark the task body as such.
	(Expand_N_Task_Type_Declaration): Mark the task body as such.
	* exp_unst.adb (Visit_Node): Use Unique_Defining_Entity instead
	of Corresponding_Spec_Of.
	* sem_attr.adb (Analyze_Attribute_Old_Result): Use
	Unique_Defining_Entity instead of Corresponding_Spec_Of.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Entry barrier
	functions do not inherit the SPARK_Mode from the context.
	(Build_Subprogram_Declaration): The matching spec is now marked
	as a source construct to mimic the original stand alone body.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Code cleanup.
	* sem_ch9.adb Add with and use clauses for Contracts.
	(Analyze_Entry_Body): An entry body freezes the contract of
	the nearest enclosing package body. The entry body now inherits
	the SPARK_Mode from the context.
	(Analyze_Entry_Declaration): A protected entry declaration now inherits
	the SPARK_Mode from the context.
	(Analyze_Protected_Body): A protected body freezes
	the contract of the nearest enclosing package body. Set the
	Etype of a protected body as this is neede for proper aspect
	analysis. Protected bodies can now carry meaningful aspects and
	those are now analyzed.
	(Analyze_Protected_Type_Declaration): A protected type now inherits the
	SPARK_Mode from the context.
	(Analyze_Task_Body): A task body freezes the contract of the
	nearest enclosing package body. Set the Etype of a task body
	as this is needed for proper aspect analysis. A task body
	now inherits the SPARK_Mode from the context.  Task bodies
	can now carry meaningful aspects and those are now analyzed.
	(Analyze_Task_Type_Declaration): A task type declaration now
	inherits the SPARK_Mode of from the context.
	* sem_ch10.adb (Analyze_Protected_Body_Stub): Protected body
	stubs can now carry meaningful aspects.
	(Analyze_Task_Body_Stub): Task body stubs can now carry meaningful
	aspects.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Aspects SPARK_Mode
	Warnings now use routine Insert_Pragma as means of insertion into
	the tree.
	(Insert_After_SPARK_Mode): Clean up documentation.
	(Insert_Pragma): Clean up documentation. The routine is now
	capable of operating on synchronized units.
	* sem_prag.adb (Add_Entity_To_Name_Buffer): New routine.
	(Analyze_Contract_Cases_In_Decl_Part): Use
	Unique_Defining_Entity instead of Corresponding_Spec_Of.
	(Analyze_Depends_Global): Use Unique_Defining_Entity instead
	of Corresponding_Spec_Of.
	(Analyze_Depends_In_Decl_Part): Use Unique_Defining_Entity instead of
	Corresponding_Spec_Of.
	(Analyze_Global_In_Decl_Part): Use Unique_Defining_Entity instead of
	Corresponding_Spec_Of.
	(Analyze_Pragma): Use Unique_Defining_Entity instead of
	Corresponding_Spec_Of.
	Update the detection of an illegal pragma Ghost when it applies
	to a task or protected unit. Reimplement the handling of
	pragma SPARK_Mode.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Use Unique_Defining_Entity
	instead of Corresponding_Spec_Of.
	(Analyze_Test_Case_In_Decl_Part): Use Unique_Defining_Entity instead of
	Corresponding_Spec_Of.
	(Check_Library_Level_Entity): Update the comment on usage.
	Reimplemented to offer a more specialized errror context.
	(Check_Pragma_Conformance): Update profile and comment on usage.
	Handle error message output on single protected or task units.
	(Collect_Subprogram_Inputs_Outputs): Use Unique_Defining_Entity
	instead of Corresponding_Spec_Of.
	(Process_Body): New routine.
	(Process_Overloadable): New routine.
	(Process_Private_Part): New routine.
	(Process_Statement_Part): New routine.
	(Process_Visible_Part): New routine.
	(Set_SPARK_Context): New routine.
	(Set_SPARK_Flags): Removed.
	* sem_util.adb (Corresponding_Spec_Of): Removed.
	(Unique_Entity): Reimplemented to handle many more cases.
	* sem_util.ads (Corresponding_Spec_Of): Removed.
	(Unique_Defining_Entity): Update the comment on usage.
	* sinfo.ads (Is_Entry_Barrier_Function): Update the assertion.
	(Is_Task_Body_Procedure): New routine.
	(Set_Is_Entry_Barrier_Function): Update the assertion.
	(Set_Is_Task_Body_Procedure): New routine.
	* sinfo.adb Update the documentation of attribute
	Is_Entry_Barrier_Function along with use in nodes. Add new
	attribute Is_Task_Body_Procedure along with use in nodes.
	(Is_Task_Body_Procedure): New routine along with pragma Inline.
	(Set_Is_Task_Body_Procedure): New routine along with pragma Inline.

From-SVN: r229328

1 files changed, 88 insertions, 43 deletions

diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 5cca0fa..08072f2 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -255,11 +255,9 @@ package body Einfo is
    --    Activation_Record_Component     Node31
 
    --    Encapsulating_State             Node32
-   --    SPARK_Pragma                    Node32
    --    No_Tagged_Streams_Pragma        Node32
 
    --    Linker_Section_Pragma           Node33
-   --    SPARK_Aux_Pragma                Node33
 
    --    Contract                        Node34
 
@@ -267,12 +265,13 @@ package body Einfo is
 
    --    Anonymous_Master                Node36
 
-   --    (Class_Wide_Preconds)           List38
+   --    Class_Wide_Preconds             List38
 
-   --    (Class_Wide_Postconds)          List39
+   --    Class_Wide_Postconds            List39
 
-   --    (unused)                        Node40
-   --    (unused)                        Node41
+   --    SPARK_Pragma                    Node40
+
+   --    SPARK_Aux_Pragma                Node41
 
    ---------------------------------------------
    -- Usage of Flags in Defining Entity Nodes --
@@ -3113,8 +3112,11 @@ package body Einfo is
       pragma Assert
         (Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-      return Node33 (Id);
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Type,   --  synchronized variants
+                       E_Task_Type));
+      return Node41 (Id);
    end SPARK_Aux_Pragma;
 
    function SPARK_Aux_Pragma_Inherited (Id : E) return B is
@@ -3122,14 +3124,19 @@ package body Einfo is
       pragma Assert
         (Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Type,   --  synchronized variants
+                       E_Task_Type));
       return Flag266 (Id);
    end SPARK_Aux_Pragma_Inherited;
 
    function SPARK_Pragma (Id : E) return N is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Function,         --  subprogram variants
+        (Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
                        E_Generic_Function,
                        E_Generic_Procedure,
                        E_Procedure,
@@ -3137,14 +3144,21 @@ package body Einfo is
            or else
          Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-      return Node32 (Id);
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Body,   --  synchronized variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type));
+      return Node40 (Id);
    end SPARK_Pragma;
 
    function SPARK_Pragma_Inherited (Id : E) return B is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Function,         --  subprogram variants
+        (Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
                        E_Generic_Function,
                        E_Generic_Procedure,
                        E_Procedure,
@@ -3152,7 +3166,12 @@ package body Einfo is
            or else
          Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Body,   --  synchronized variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type));
       return Flag265 (Id);
    end SPARK_Pragma_Inherited;
 
@@ -6124,9 +6143,11 @@ package body Einfo is
       pragma Assert
         (Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-
-      Set_Node33 (Id, V);
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Type,   --  synchronized variants
+                       E_Task_Type));
+      Set_Node41 (Id, V);
    end Set_SPARK_Aux_Pragma;
 
    procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
@@ -6134,15 +6155,19 @@ package body Einfo is
       pragma Assert
         (Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Type,   --  synchronized variants
+                       E_Task_Type));
       Set_Flag266 (Id, V);
    end Set_SPARK_Aux_Pragma_Inherited;
 
    procedure Set_SPARK_Pragma (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Function,         --  subprogram variants
+        (Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
                        E_Generic_Function,
                        E_Generic_Procedure,
                        E_Procedure,
@@ -6150,15 +6175,21 @@ package body Einfo is
            or else
          Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-
-      Set_Node32 (Id, V);
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Body,   --  synchronized variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type));
+      Set_Node40 (Id, V);
    end Set_SPARK_Pragma;
 
    procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Function,         --  subprogram variants
+        (Ekind_In (Id, E_Entry,            --  overloadable variants
+                       E_Entry_Family,
+                       E_Function,
                        E_Generic_Function,
                        E_Generic_Procedure,
                        E_Procedure,
@@ -6166,8 +6197,12 @@ package body Einfo is
            or else
          Ekind_In (Id, E_Generic_Package,  --  package variants
                        E_Package,
-                       E_Package_Body));
-
+                       E_Package_Body)
+           or else
+         Ekind_In (Id, E_Protected_Body,   --  synchronized variants
+                       E_Protected_Type,
+                       E_Task_Body,
+                       E_Task_Type));
       Set_Flag265 (Id, V);
    end Set_SPARK_Pragma_Inherited;
 
@@ -10141,16 +10176,6 @@ package body Einfo is
               E_Variable                                   =>
             Write_Str ("Encapsulating_State");
 
-         when E_Function                                   |
-              E_Generic_Function                           |
-              E_Generic_Package                            |
-              E_Generic_Procedure                          |
-              E_Package                                    |
-              E_Package_Body                               |
-              E_Procedure                                  |
-              E_Subprogram_Body                            =>
-            Write_Str ("SPARK_Pragma");
-
          when Type_Kind                                    =>
             Write_Str ("No_Tagged_Streams_Pragma");
 
@@ -10166,11 +10191,6 @@ package body Einfo is
    procedure Write_Field33_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
-         when E_Generic_Package                            |
-              E_Package                                    |
-              E_Package_Body                               =>
-            Write_Str ("SPARK_Aux_Pragma");
-
          when E_Constant                                   |
               E_Variable                                   |
               Subprogram_Kind                              |
@@ -10259,7 +10279,8 @@ package body Einfo is
    procedure Write_Field38_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
-         when E_Function | E_Procedure                     =>
+         when E_Function                                   |
+              E_Procedure                                  =>
             Write_Str ("Class-wide preconditions");
 
          when others                                       =>
@@ -10274,7 +10295,8 @@ package body Einfo is
    procedure Write_Field39_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
-         when E_Function | E_Procedure                     =>
+         when E_Function                                   |
+              E_Procedure                                  =>
             Write_Str ("Class-wide postcondition");
 
          when others                                       =>
@@ -10289,6 +10311,22 @@ package body Einfo is
    procedure Write_Field40_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Entry                                      |
+              E_Entry_Family                               |
+              E_Function                                   |
+              E_Generic_Function                           |
+              E_Generic_Package                            |
+              E_Generic_Procedure                          |
+              E_Package                                    |
+              E_Package_Body                               |
+              E_Procedure                                  |
+              E_Protected_Body                             |
+              E_Protected_Type                             |
+              E_Subprogram_Body                            |
+              E_Task_Body                                  |
+              E_Task_Type                                  =>
+            Write_Str ("SPARK_Pragma");
+
          when others                                       =>
             Write_Str ("Field40??");
       end case;
@@ -10301,6 +10339,13 @@ package body Einfo is
    procedure Write_Field41_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Generic_Package                            |
+              E_Package                                    |
+              E_Package_Body                               |
+              E_Protected_Type                             |
+              E_Task_Type                                  =>
+            Write_Str ("SPARK_Aux_Pragma");
+
          when others                                       =>
             Write_Str ("Field41??");
       end case;