[multiple changes]

2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb Flag264 is now unused.
	(Has_Body_References): Removed.
	(Set_Has_Body_References): Removed.
	(Write_Entity_Flags): Remove the output for flag Has_Body_References.
	* einfo.ads Update the comment on usage of attribute
	Body_References. Remove attribute Has_Body_References and its
	usage in nodes.
	(Has_Body_References): Removed along with pragma Inline.
	(Set_Has_Body_References): Removed along with pragma Inline.
	* sem_prag.adb (Analyze_Global_Item): Move the call to
	Record_Possible_Body_Reference in the state related checks
	section. Add a comment intended function.
	(Analyze_Input_Output): Move the call to Record_Possible_Body_Reference
	in the state related checks section. Add a comment intended function.
	(Analyze_Refinement_Clause): Cleanup the illegal body reference
	reporting. Add a comment on timing of error reporting.
	(Record_Possible_Body_Reference): Reimplement the routine.

2014-01-29  Vincent Celier  <celier@adacore.com>

	* makeutl.adb (Mains.Find_File_Add_Extension): Only look for specs for
	unit-based languages.
	(Mains.Complete_Mains.Do_Complete): Use the source file project
	tree when calling Find_File_Add_Extension. Use the correct
	project name when reporting an error.

From-SVN: r207252

5 files changed, 126 insertions, 70 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4f853b9..86168ba 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,33 @@
 2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* einfo.adb Flag264 is now unused.
+	(Has_Body_References): Removed.
+	(Set_Has_Body_References): Removed.
+	(Write_Entity_Flags): Remove the output for flag Has_Body_References.
+	* einfo.ads Update the comment on usage of attribute
+	Body_References. Remove attribute Has_Body_References and its
+	usage in nodes.
+	(Has_Body_References): Removed along with pragma Inline.
+	(Set_Has_Body_References): Removed along with pragma Inline.
+	* sem_prag.adb (Analyze_Global_Item): Move the call to
+	Record_Possible_Body_Reference in the state related checks
+	section. Add a comment intended function.
+	(Analyze_Input_Output): Move the call to Record_Possible_Body_Reference
+	in the state related checks section. Add a comment intended function.
+	(Analyze_Refinement_Clause): Cleanup the illegal body reference
+	reporting. Add a comment on timing of error reporting.
+	(Record_Possible_Body_Reference): Reimplement the routine.
+
+2014-01-29  Vincent Celier  <celier@adacore.com>
+
+	* makeutl.adb (Mains.Find_File_Add_Extension): Only look for specs for
+	unit-based languages.
+	(Mains.Complete_Mains.Do_Complete): Use the source file project
+	tree when calling Find_File_Add_Extension. Use the correct
+	project name when reporting an error.
+
+2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* aspects.adb Add an entry for aspect Part_Of in table
 	Canonical_Aspect.
 	* aspects.ads Add an entry for aspect Part_Of in tables Aspect_Id,
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index cc1c23f..cd59211 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -552,7 +552,6 @@ package body Einfo is
    --    Has_Delayed_Rep_Aspects         Flag261
    --    May_Inherit_Delayed_Rep_Aspects Flag262
    --    Has_Visible_Refinement          Flag263
-   --    Has_Body_References             Flag264
    --    SPARK_Pragma_Inherited          Flag265
    --    SPARK_Aux_Pragma_Inherited      Flag266
 
@@ -560,6 +559,7 @@ package body Einfo is
    --    (unused)                        Flag2
    --    (unused)                        Flag3
 
+   --    (unused)                        Flag264
    --    (unused)                        Flag267
    --    (unused)                        Flag268
    --    (unused)                        Flag269
@@ -1334,12 +1334,6 @@ package body Einfo is
       return Flag139 (Id);
    end Has_Biased_Representation;
 
-   function Has_Body_References (Id : E) return B is
-   begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      return Flag264 (Id);
-   end Has_Body_References;
-
    function Has_Completion (Id : E) return B is
    begin
       return Flag26 (Id);
@@ -4007,12 +4001,6 @@ package body Einfo is
       Set_Flag139 (Id, V);
    end Set_Has_Biased_Representation;
 
-   procedure Set_Has_Body_References (Id : E; V : B := True) is
-   begin
-      pragma Assert (Ekind (Id) = E_Abstract_State);
-      Set_Flag264 (Id, V);
-   end Set_Has_Body_References;
-
    procedure Set_Has_Completion (Id : E; V : B := True) is
    begin
       Set_Flag26 (Id, V);
@@ -8109,7 +8097,6 @@ package body Einfo is
       W ("Has_Anonymous_Master",            Flag253 (Id));
       W ("Has_Atomic_Components",           Flag86  (Id));
       W ("Has_Biased_Representation",       Flag139 (Id));
-      W ("Has_Body_References",             Flag264 (Id));
       W ("Has_Completion",                  Flag26  (Id));
       W ("Has_Completion_In_Body",          Flag71  (Id));
       W ("Has_Complex_Representation",      Flag140 (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 538af8a..eec2708 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -494,10 +494,10 @@ package Einfo is
 --       when the unit is part of a standalone library.
 
 --    Body_References (Elist16)
---       Defined in abstract state entities. Only set if Has_Body_References
---       flag is set True, in which case it contains an element list of global
---       references (identifiers) in the current package body to this abstract
---       state that are illegal if the abstract state has a visible refinement.
+--       Defined in abstract state entities. Contains an element list of
+--       references (identifiers) that appear in a package body whose spec
+--       defines the related state. If the body refines the said state, all
+--       references on this list are illegal due to the visible refinement.
 
 --    C_Pass_By_Copy (Flag125) [implementation base type only]
 --       Defined in record types. Set if a pragma Convention for the record
@@ -1407,10 +1407,6 @@ package Einfo is
 --       size of the type, forcing biased representation for the object, but
 --       the subtype is still an unbiased type.
 
---    Has_Body_References (Flag264)
---       Defined in entities for abstract states. Set if Body_References has
---       at least one entry.
-
 --    Has_Completion (Flag26)
 --       Defined in all entities that require a completion (functions,
 --       procedures, private types, limited private types, incomplete types,
@@ -5155,7 +5151,6 @@ package Einfo is
    --    Body_References                     (Elist16)
    --    Non_Limited_View                    (Node17)
    --    From_Limited_With                   (Flag159)
-   --    Has_Body_References                 (Flag264)
    --    Has_Visible_Refinement              (Flag263)
    --    Has_Non_Null_Refinement             (synth)
    --    Has_Null_Refinement                 (synth)
@@ -6378,7 +6373,6 @@ package Einfo is
    function Has_Anonymous_Master                (Id : E) return B;
    function Has_Atomic_Components               (Id : E) return B;
    function Has_Biased_Representation           (Id : E) return B;
-   function Has_Body_References                 (Id : E) return B;
    function Has_Completion                      (Id : E) return B;
    function Has_Completion_In_Body              (Id : E) return B;
    function Has_Complex_Representation          (Id : E) return B;
@@ -6999,7 +6993,6 @@ package Einfo is
    procedure Set_Has_Anonymous_Master            (Id : E; V : B := True);
    procedure Set_Has_Atomic_Components           (Id : E; V : B := True);
    procedure Set_Has_Biased_Representation       (Id : E; V : B := True);
-   procedure Set_Has_Body_References             (Id : E; V : B := True);
    procedure Set_Has_Completion                  (Id : E; V : B := True);
    procedure Set_Has_Completion_In_Body          (Id : E; V : B := True);
    procedure Set_Has_Complex_Representation      (Id : E; V : B := True);
@@ -7731,7 +7724,6 @@ package Einfo is
    pragma Inline (Has_Anonymous_Master);
    pragma Inline (Has_Atomic_Components);
    pragma Inline (Has_Biased_Representation);
-   pragma Inline (Has_Body_References);
    pragma Inline (Has_Completion);
    pragma Inline (Has_Completion_In_Body);
    pragma Inline (Has_Complex_Representation);
@@ -8199,7 +8191,6 @@ package Einfo is
    pragma Inline (Set_Has_Anonymous_Master);
    pragma Inline (Set_Has_Atomic_Components);
    pragma Inline (Set_Has_Biased_Representation);
-   pragma Inline (Set_Has_Body_References);
    pragma Inline (Set_Has_Completion);
    pragma Inline (Set_Has_Completion_In_Body);
    pragma Inline (Set_Has_Complex_Representation);
diff --git a/gcc/ada/makeutl.adb b/gcc/ada/makeutl.adb
index 4a8f8a8..c546931 100644
--- a/gcc/ada/makeutl.adb
+++ b/gcc/ada/makeutl.adb
@@ -1654,9 +1654,11 @@ package body Makeutl is
                      end if;
                   end if;
 
-               elsif Source.Kind = Spec then
-                  --  A spec needs to be taken into account unless there is
-                  --  also a body. So we delay the decision for them.
+               elsif Source.Kind = Spec
+                 and then Source.Language.Config.Kind = Unit_Based
+               then
+                  --  An Ada spec needs to be taken into account unless there
+                  --  is also a body. So we delay the decision for them.
 
                   Get_Name_String (Source.File);
 
@@ -1785,7 +1787,7 @@ package body Makeutl is
 
                         if Source = No_Source then
                            Source := Find_File_Add_Extension
-                             (Tree, Get_Name_String (Main_Id));
+                             (File.Tree, Get_Name_String (Main_Id));
                         end if;
 
                         if Is_Absolute
@@ -1852,10 +1854,10 @@ package body Makeutl is
                            --  reported later.
 
                            Error_Msg_File_1 := Main_Id;
-                           Error_Msg_Name_1 := Root_Project.Name;
+                           Error_Msg_Name_1 := File.Project.Name;
                            Prj.Err.Error_Msg
                              (Flags, "{ is not a source of project %%",
-                              File.Location, Project);
+                              File.Location, File.Project);
                         end if;
                      end if;
                   end;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d976438..e0d275e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -280,11 +280,13 @@ package body Sem_Prag is
    --  spec expressions (i.e. similar to a default expression).
 
    procedure Record_Possible_Body_Reference
-     (Item    : Node_Id;
-      Item_Id : Entity_Id);
-   --  Given an entity reference (Item) and the corresponding Entity (Item_Id),
-   --  determines if we have a body reference to an abstract state, which may
-   --  be illegal if the state is refined within the body.
+     (State_Id : Entity_Id;
+      Ref      : Node_Id);
+   --  Subsidiary to the analysis of pragmas [Refined_]Depends and [Refined_]
+   --  Global. Given an abstract state denoted by State_Id and a reference Ref
+   --  to it, determine whether the reference appears in a package body that
+   --  will eventually refine the state. If this is the case, record the
+   --  reference for future checks (see Analyze_Refined_State_In_Decls).
 
    procedure Resolve_State (N : Node_Id);
    --  Handle the overloading of state names by functions. When N denotes a
@@ -799,8 +801,6 @@ package body Sem_Prag is
                Item_Id := Entity_Of (Item);
 
                if Present (Item_Id) then
-                  Record_Possible_Body_Reference (Item, Item_Id);
-
                   if Ekind_In (Item_Id, E_Abstract_State,
                                         E_In_Parameter,
                                         E_In_Out_Parameter,
@@ -842,14 +842,28 @@ package body Sem_Prag is
                         Add_Item (Item_Id, All_Inputs_Seen);
                      end if;
 
-                     if Ekind (Item_Id) = E_Abstract_State
-                       and then Has_Visible_Refinement (Item_Id)
-                     then
-                        Error_Msg_NE
-                          ("cannot mention state & in global refinement, use "
-                           & "its constituents instead (SPARK RM 6.1.5(3))",
-                           Item, Item_Id);
-                        return;
+                     --  State related checks
+
+                     if Ekind (Item_Id) = E_Abstract_State then
+                        if Has_Visible_Refinement (Item_Id) then
+                           Error_Msg_NE
+                             ("cannot mention state & in global refinement",
+                              Item, Item_Id);
+                           Error_Msg_N
+                              ("\use its constituents instead (SPARK RM "
+                               & "6.1.5(3))", Item);
+                           return;
+
+                        --  If the reference to the abstract state appears in
+                        --  an enclosing package body that will eventually
+                        --  refine the state, record the reference for future
+                        --  checks.
+
+                        else
+                           Record_Possible_Body_Reference
+                             (State_Id => Item_Id,
+                              Ref      => Item);
+                        end if;
                      end if;
 
                      --  When the item renames an entire object, replace the
@@ -1871,7 +1885,6 @@ package body Sem_Prag is
             Item_Id := Entity_Of (Item);
 
             if Present (Item_Id) then
-               Record_Possible_Body_Reference (Item, Item_Id);
 
                --  A global item may denote a formal parameter of an enclosing
                --  subprogram. Do this check first to provide a better error
@@ -1917,6 +1930,15 @@ package body Sem_Prag is
                         & "constituents instead (SPARK RM 6.1.4(8))",
                         Item, Item_Id);
                      return;
+
+                  --  If the reference to the abstract state appears in an
+                  --  enclosing package body that will eventually refine the
+                  --  state, record the reference for future checks.
+
+                  else
+                     Record_Possible_Body_Reference
+                       (State_Id => Item_Id,
+                        Ref      => Item);
                   end if;
 
                --  Variable related checks
@@ -22786,7 +22808,7 @@ package body Sem_Prag is
 
                procedure Collect_Constituent is
                begin
-                  --  Add the constituent to the lis of processed items to aid
+                  --  Add the constituent to the list of processed items to aid
                   --  with the detection of duplicates.
 
                   Add_Item (Constit_Id, Constituents_Seen);
@@ -23077,10 +23099,10 @@ package body Sem_Prag is
 
                   if Ekind (Constit_Id) = E_Abstract_State then
                      Error_Msg_NE
-                       ("\  abstract state & defined #", State, Constit_Id);
+                       ("\\  abstract state & defined #", State, Constit_Id);
                   else
                      Error_Msg_NE
-                       ("\  variable & defined #", State, Constit_Id);
+                       ("\\  variable & defined #", State, Constit_Id);
                   end if;
 
                   Next_Elmt (Constit_Elmt);
@@ -23122,18 +23144,20 @@ package body Sem_Prag is
                return;
             end if;
 
-            --  A global item cannot denote a state abstraction whose
-            --  refinement is visible, in other words a state abstraction
-            --  cannot be named within its enclosing package's body other than
-            --  in its refinement.
+            --  References to a state with visible refinement are illegal. In
+            --  the case where nested packages are involved, detecting such
+            --  references is tricky because pragma Refined_State is analyzed
+            --  later than the offending pragma Depends or Global. References
+            --  that occur in such nested context are stored in a list. Emit
+            --  errors for all references found in Body_References.
 
-            if Has_Body_References (State_Id) then
+            if Present (Body_References (State_Id)) then
                Body_Ref_Elmt := First_Elmt (Body_References (State_Id));
                while Present (Body_Ref_Elmt) loop
                   Body_Ref := Node (Body_Ref_Elmt);
 
                   Error_Msg_N
-                    ("global reference to & not allowed (SPARK RM 6.1.4(8))",
+                    ("reference to & not allowed (SPARK RM 6.1.4(8))",
                      Body_Ref);
                   Error_Msg_Sloc := Sloc (State);
                   Error_Msg_N ("\refinement of & is visible#", Body_Ref);
@@ -23389,9 +23413,10 @@ package body Sem_Prag is
 
                if Ekind (State_Id) = E_Abstract_State then
                   Error_Msg_NE
-                    ("\  abstract state & defined #", Body_Id, State_Id);
+                    ("\\  abstract state & defined #", Body_Id, State_Id);
                else
-                  Error_Msg_NE ("\  variable & defined #", Body_Id, State_Id);
+                  Error_Msg_NE
+                    ("\\  variable & defined #", Body_Id, State_Id);
                end if;
 
                Next_Elmt (State_Elmt);
@@ -25072,20 +25097,43 @@ package body Sem_Prag is
    ------------------------------------
 
    procedure Record_Possible_Body_Reference
-     (Item    : Node_Id;
-      Item_Id : Entity_Id)
+     (State_Id : Entity_Id;
+      Ref      : Node_Id)
    is
+      Context : Node_Id;
+      Spec_Id : Entity_Id;
+
    begin
-      if Is_Body_Name (Unit_Name (Get_Source_Unit (Item)))
-        and then Ekind (Item_Id) = E_Abstract_State
-      then
-         if not Has_Body_References (Item_Id) then
-            Set_Has_Body_References (Item_Id, True);
-            Set_Body_References (Item_Id, New_Elmt_List);
+      --  Ensure that we are dealing with a reference to a state
+
+      pragma Assert (Ekind (State_Id) = E_Abstract_State);
+
+      --  Climb the tree starting from the reference looking for a package body
+      --  whose spec declares the referenced state. This criteria automatically
+      --  excludes references in package specs which are legal. Note that it is
+      --  not wise to emit an error now as the package body may lack pragma
+      --  Refined_State or the referenced state may not be mentioned in the
+      --  refinement. This approach avoids the generation of misleading errors.
+
+      Context := Ref;
+      while Present (Context) loop
+         if Nkind (Context) = N_Package_Body then
+            Spec_Id := Corresponding_Spec (Context);
+
+            if Present (Abstract_States (Spec_Id))
+              and then Contains (Abstract_States (Spec_Id), State_Id)
+            then
+               if No (Body_References (State_Id)) then
+                  Set_Body_References (State_Id, New_Elmt_List);
+               end if;
+
+               Append_Elmt (Ref, Body_References (State_Id));
+               exit;
+            end if;
          end if;
 
-         Append_Elmt (Item, Body_References (Item_Id));
-      end if;
+         Context := Parent (Context);
+      end loop;
    end Record_Possible_Body_Reference;
 
    ------------------------------