+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
-- 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
-- (unused) Flag2
-- (unused) Flag3
+ -- (unused) Flag264
-- (unused) Flag267
-- (unused) Flag268
-- (unused) Flag269
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);
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);
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));
-- 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
-- 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,
-- 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)
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;
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);
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);
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);
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);
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
-- 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;
-- 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
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,
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
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
& "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
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);
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);
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);
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);
------------------------------------
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;
------------------------------
projects / gcc.git / commitdiff