[multiple changes]

2011-08-01  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Enter_Name): issue error in formal mode on declaration
	of homonym, unless the homonym is one of the cases allowed in SPARK
	* par-ch5.adb (Parse_Decls_Begin_End): issue error in SPARK mode for
	package declaration occurring after a body.

2011-08-01  Robert Dewar  <dewar@adacore.com>

	* checks.adb, exp_ch4.adb: Minor reformatting.

2011-08-01  Javier Miranda  <miranda@adacore.com>

	* einfo.ads (Access_Disp_Table): Fix documentation.
	(Dispatch_Table_Wrappers): Fix documentation.

2011-08-01  Pascal Obry  <obry@adacore.com>

	* prj-env.adb, prj-env.ads: Minor reformatting.

From-SVN: r177053

gcc/ada/ChangeLog

 2011-08-01  Yannick Moy  <moy@adacore.com>
 
+	* sem_util.adb (Enter_Name): issue error in formal mode on declaration
+	of homonym, unless the homonym is one of the cases allowed in SPARK
+	* par-ch5.adb (Parse_Decls_Begin_End): issue error in SPARK mode for
+	package declaration occurring after a body.
+
+2011-08-01  Robert Dewar  <dewar@adacore.com>
+
+	* checks.adb, exp_ch4.adb: Minor reformatting.
+
+2011-08-01  Javier Miranda  <miranda@adacore.com>
+
+	* einfo.ads (Access_Disp_Table): Fix documentation.
+	(Dispatch_Table_Wrappers): Fix documentation.
+
+2011-08-01  Pascal Obry  <obry@adacore.com>
+
+	* prj-env.adb, prj-env.ads: Minor reformatting.
+
+2011-08-01  Yannick Moy  <moy@adacore.com>
+
 	* sem_util.ads, sem_util.adb, par.adb, par_util.adb
 	(Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
 	procedures out of these packages.

gcc/ada/checks.adb

@@ -4565,8 +4565,10 @@ package body Checks is
       ----------------------
 
       function Entity_Of_Prefix return Entity_Id is
-         P : Node_Id := Prefix (N);
+         P : Node_Id;
+
       begin
+         P := Prefix (N);
          while not Is_Entity_Name (P) loop
             if not Nkind_In (P, N_Selected_Component,
                                 N_Indexed_Component)

gcc/ada/einfo.ads

@@ -338,18 +338,18 @@ package Einfo is
 --       statements referencing the same entry.
 
 --    Access_Disp_Table (Elist16) [implementation base type only]
---       Present in record types and subtypes. Set in tagged types to point to
---       the dispatch tables associated with the tagged type. The first two
---       entities correspond with the primary dispatch table: 1) primary
---       dispatch table with user-defined primitives, 2) primary dispatch table
---       with predefined primitives. For each interface type covered by the
---       tagged type we also have: 3) secondary dispatch table with thunks of
---       primitives covering user-defined interface primitives, 4) secondary
---       dispatch table with thunks of predefined primitives, 5) secondary
---       dispatch table with user-defined primitives, and 6) secondary dispatch
---       table with predefined primitives. The last entity of this list is an
---       access type declaration used to expand dispatching calls through the
---       primary dispatch table. For a non-tagged record, contains No_Elist.
+--       Present in E_Record_Type and E_Record_Subtype entities. Set in tagged
+--       types to point to their dispatch tables. The first two entities are
+--       associated with the primary dispatch table: 1) primary dispatch table
+--       with user-defined primitives 2) primary dispatch table with predefined
+--       primitives. For each interface type covered by the tagged type we also
+--       have: 3) secondary dispatch table with thunks of primitives covering
+--       user-defined interface primitives, 4) secondary dispatch table with
+--       thunks of predefined primitives, 5) secondary dispatch table with user
+--       defined primitives, and 6) secondary dispatch table with predefined
+--       primitives. The last entity of this list is an access type declaration
+--       used to expand dispatching calls through the primary dispatch table.
+--       For a non-tagged record, contains No_Elist.
 
 --    Actual_Subtype (Node17)
 --       Present in variables, constants, and formal parameters. This is the
@@ -855,10 +855,11 @@ package Einfo is
 --       index starting at 1 and ranging up to number of discriminants.
 
 --    Dispatch_Table_Wrappers (Elist26) [implementation base type only]
---       Present in record types and subtypes. Set in library level tagged type
---       entities if we are generating statically allocated dispatch tables.
---       Points to the list of dispatch table wrappers associated with the
---       tagged type. For a non-tagged record, contains No_Elist.
+--       Present in E_Record_Type and E_Record_Subtype entities. Set in library
+--       level tagged type entities if we are generating statically allocated
+--       dispatch tables. Points to the list of dispatch table wrappers
+--       associated with the tagged type. For a non-tagged record, contains
+--       No_Elist.
 
 --    DTC_Entity (Node16)
 --       Present in function and procedure entities. Set to Empty unless

gcc/ada/exp_ch4.adb

@@ -876,7 +876,6 @@ package body Exp_Ch4 is
          if Present (TagT) then
             declare
                Full_T : constant Entity_Id := Underlying_Type (TagT);
-
             begin
                Tag_Assign :=
                  Make_Assignment_Statement (Loc,

gcc/ada/par-ch5.adb

@@ -2114,6 +2114,8 @@ package body Ch5 is
       --  The same is true for the SPARK mode: although SPARK 95 removes
       --  the distinction between initial and later declarative items,
       --  the distinction remains in the Examiner. (JB01-005)
+      --  Note that the Examiner does not count package declarations in later
+      --  declarative items.
 
       if Ada_Version = Ada_83 or else SPARK_Mode then
          Decl := First (Decls);
@@ -2135,7 +2137,9 @@ package body Ch5 is
                Body_Sloc := Sloc (Decl);
 
                Inner : while Present (Decl) loop
-                  if Nkind (Decl) not in N_Later_Decl_Item
+                  if (Nkind (Decl) not in N_Later_Decl_Item
+                      or else (SPARK_Mode
+                               and then Nkind (Decl) = N_Package_Declaration))
                     and then Nkind (Decl) /= N_Pragma
                   then
                      if Ada_Version = Ada_83 then

gcc/ada/prj-env.ads

@@ -75,7 +75,7 @@ package Prj.Env is
      (In_Tree   : Project_Tree_Ref;
       Path_FD   : out File_Descriptor;
       Path_Name : out Path_Name_Type);
-   --  Create a new temporary path file. Get the file name in Path_Name.
+   --  Create a new temporary path file. Get the file name in Path_Name
 
    function Ada_Include_Path
      (Project   : Project_Id;

gcc/ada/sem_util.adb

@@ -3200,6 +3200,45 @@ package body Sem_Util is
       Append_Entity     (Def_Id, S);
       Set_Public_Status (Def_Id);
 
+      --  Declaring an homonym is not allowed in SPARK or ALFA...
+
+      if Formal_Verification_Mode and then Present (C)
+
+        --  ...unless the new declaration is in a subprogram, and the visible
+        --  declaration is a variable declaration or a parameter specification
+        --  outside that subprogram;
+
+        and then not
+          (Nkind_In (Parent (Parent (Def_Id)),
+                     N_Subprogram_Body,
+                     N_Function_Specification,
+                     N_Procedure_Specification)
+           and then
+             Nkind_In (Parent (C),
+                       N_Object_Declaration,
+                       N_Parameter_Specification))
+
+        --  ...or the new declaration is in a package, and the visible
+        --  declaration occurs outside that package;
+
+        and then not Nkind_In (Parent (Parent (Def_Id)),
+                               N_Package_Specification,
+                               N_Package_Body)
+
+        --  ...or the new declaration is a component declaration in a record
+        --  type definition.
+
+        and then Nkind (Parent (Def_Id)) /= N_Component_Declaration
+
+        --  Don't issue error for non-source entities
+
+        and then Comes_From_Source (Def_Id)
+        and then Comes_From_Source (C)
+      then
+         Error_Msg_Sloc := Sloc (C);
+         Formal_Error_Msg_N ("redeclaration of identifier &#", Def_Id);
+      end if;
+
       --  Warn if new entity hides an old one
 
       if Warn_On_Hiding and then Present (C)