2013-10-14 Hristian Kirtchev <kirtchev@adacore.com>
+ * einfo.adb: Flag 263 is now known as Has_Visible_Refinement.
+ (Has_Non_Null_Refinement): New routine.
+ (Has_Null_Refinement): The routine is now synthesized.
+ (Has_Visible_Refinement): New routine.
+ (Set_Has_Visible_Refinement): New routine.
+ (Write_Entity_Flags): Remove the output for
+ Has_Null_Refinement. Add output for Has_Visible_Refinement.
+ * einfo.ads: Update the occurrences of Has_Non_Null_Refinement,
+ Has_Null_Refinement and Has_Visible_Refinement in entities.
+ (Has_Non_Null_Refinement): New synthesized attribute.
+ (Has_Null_Refinement): This attribute is now synthesized.
+ (Has_Visible_Refinement): New routine with corresponding
+ pragma Inline.
+ (Set_Has_Visible_Refinement): New routine with corresponding pragma
+ Inline.
+ * sem_ch3.adb (Analyze_Declarations): Add new local
+ variable In_Package_Body. Remove state refinements from
+ visibility at the end of the package body declarations.
+ (Remove_Visible_Refinements): New routine.
+ * sem_prag.adb (Analyze_Constituent): Collect a null
+ constituent and mark the state as having visible refinement.
+ (Analyze_Global_Item): Use attribute Has_Visible_Refinement to
+ detect a state with visible refinement.
+ (Analyze_Input_Output): Use attribute Has_Visible_Refinement to detect
+ a state with visible refinement.
+ (Check_Dependency_Clause): Use attribute Has_Non_Null_Refinement rather
+ than checking the contents of list Refinement_Constituents.
+ (Check_In_Out_States): Use attribute Has_Non_Null_Refinement rather
+ than checking the contents of list Refinement_Constituents.
+ (Check_Input_States): Use attribute Has_Non_Null_Refinement rather
+ than checking the contents of list Refinement_Constituents.
+ (Check_Matching_Constituent): Mark a state as having visible refinement.
+ (Check_Output_States): Use attribute Has_Non_Null_Refinement rather than
+ checking the contents of list Refinement_Constituents.
+ (Check_Refined_Global_Item): Use attribute Has_Visible_Refinement
+ to detect a state with visible refinement.
+ (Is_Matching_Input): Use attribute Has_Non_Null_Refinement rather than
+ checking the contents of list Refinement_Constituents.
+ * sem_util.adb (Is_Refined_State): Use attribute
+ Has_Visible_Refinement to detect a state with visible refinement.
+
+2013-10-14 Hristian Kirtchev <kirtchev@adacore.com>
+
* sem_prag.adb (Check_Mode): Do not emit an
error when inspecting a self referencial output item of an
unconstrained type.
-- Has_Delayed_Rep_Aspects Flag261
-- May_Inherit_Delayed_Rep_Aspects Flag262
- -- Has_Null_Refinement Flag263
+ -- Has_Visible_Refinement Flag263
-- (unused) Flag264
-- (unused) Flag265
return Flag75 (Implementation_Base_Type (Id));
end Has_Non_Standard_Rep;
- function Has_Null_Refinement (Id : E) return B is
- begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- return Flag263 (Id);
- end Has_Null_Refinement;
-
function Has_Object_Size_Clause (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
return Flag215 (Id);
end Has_Up_Level_Access;
+ function Has_Visible_Refinement (Id : E) return B is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ return Flag263 (Id);
+ end Has_Visible_Refinement;
+
function Has_Volatile_Components (Id : E) return B is
begin
return Flag87 (Implementation_Base_Type (Id));
Set_Flag75 (Id, V);
end Set_Has_Non_Standard_Rep;
- procedure Set_Has_Null_Refinement (Id : E; V : B := True) is
- begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- Set_Flag263 (Id, V);
- end Set_Has_Null_Refinement;
-
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True) is
begin
pragma Assert (Is_Type (Id));
Set_Flag72 (Id, V);
end Set_Has_Unknown_Discriminants;
+ procedure Set_Has_Visible_Refinement (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+ Set_Flag263 (Id, V);
+ end Set_Has_Visible_Refinement;
+
procedure Set_Has_Volatile_Components (Id : E; V : B := True) is
begin
pragma Assert (not Is_Type (Id) or else Is_Base_Type (Id));
end Has_Interrupt_Handler;
-----------------------------
+ -- Has_Non_Null_Refinement --
+ -----------------------------
+
+ function Has_Non_Null_Refinement (Id : E) return B is
+ begin
+ -- "Refinement" is a concept applicable only to abstract states
+
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+
+ if Has_Visible_Refinement (Id) then
+ pragma Assert (Present (Refinement_Constituents (Id)));
+
+ -- For a refinement to be non-null, the first constituent must be
+ -- anything other than null.
+
+ return
+ Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null;
+ end if;
+
+ return False;
+ end Has_Non_Null_Refinement;
+
+ -----------------------------
-- Has_Null_Abstract_State --
-----------------------------
and then Is_Null_State (Node (First_Elmt (Abstract_States (Id))));
end Has_Null_Abstract_State;
+ -------------------------
+ -- Has_Null_Refinement --
+ -------------------------
+
+ function Has_Null_Refinement (Id : E) return B is
+ begin
+ -- "Refinement" is a concept applicable only to abstract states
+
+ pragma Assert (Ekind (Id) = E_Abstract_State);
+
+ if Has_Visible_Refinement (Id) then
+ pragma Assert (Present (Refinement_Constituents (Id)));
+
+ -- For a refinement to be null, the state's sole constituent must be
+ -- a null.
+
+ return
+ Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null;
+ end if;
+
+ return False;
+ end Has_Null_Refinement;
+
--------------------
-- Has_Unmodified --
--------------------
W ("Has_Missing_Return", Flag142 (Id));
W ("Has_Nested_Block_With_Handler", Flag101 (Id));
W ("Has_Non_Standard_Rep", Flag75 (Id));
- W ("Has_Null_Refinement", Flag263 (Id));
W ("Has_Object_Size_Clause", Flag172 (Id));
W ("Has_Per_Object_Constraint", Flag154 (Id));
W ("Has_Postconditions", Flag240 (Id));
W ("Has_Unchecked_Union", Flag123 (Id));
W ("Has_Unknown_Discriminants", Flag72 (Id));
W ("Has_Up_Level_Access", Flag215 (Id));
+ W ("Has_Visible_Refinement", Flag263 (Id));
W ("Has_Volatile_Components", Flag87 (Id));
W ("Has_Xref_Entry", Flag182 (Id));
W ("In_Package_Body", Flag48 (Id));
-- optimizations to ensure that they are consistent with exceptions.
-- See documentation in Gigi for further details.
+-- Has_Non_Null_Refinement (synth)
+-- Defined in E_Abstract_State entities. True if the state has at least
+-- one variable or state constituent in aspect/pragma Refined_State.
+
-- Has_Non_Standard_Rep (Flag75) [implementation base type only]
-- Defined in all type entities. Set when some representation clause
-- or pragma causes the representation of the item to be significantly
-- Defined in package entities. True if the package is subject to a null
-- Abstract_State aspect/pragma.
--- Has_Null_Refinement (Flag263)
--- Defined in E_Abstract_State entities. Set if the state has a null
+-- Has_Null_Refinement (synth)
+-- Defined in E_Abstract_State entities. True if the state has a null
-- refinement in aspect/pragma Refined_State.
-- Has_Object_Size_Clause (Flag172)
-- VM_Target /= No_VM, for efficiency, since only the .NET back-end
-- makes use of it to generate proper code for up-level references.
+-- Has_Visible_Refinement (Flag263)
+-- Defined in E_Abstract_State entities. Set when a state has at least
+-- one refinement constituent and analysis is in the region between
+-- pragma Refined_State and the end of the package body declarations.
+
-- Has_Volatile_Components (Flag87) [implementation base type only]
-- Defined in all types and objects. Set only for an array type or array
-- object if a valid pragma Volatile_Components or a valid pragma
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Refined_State (Node10)
- -- Has_Null_Refinement (Flag263)
+ -- Has_Visible_Refinement (Flag263)
+ -- Has_Non_Null_Refinement (synth)
+ -- Has_Null_Refinement (synth)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
function Has_Missing_Return (Id : E) return B;
function Has_Nested_Block_With_Handler (Id : E) return B;
function Has_Non_Standard_Rep (Id : E) return B;
- function Has_Null_Refinement (Id : E) return B;
function Has_Object_Size_Clause (Id : E) return B;
function Has_Per_Object_Constraint (Id : E) return B;
function Has_Postconditions (Id : E) return B;
function Has_Unchecked_Union (Id : E) return B;
function Has_Unknown_Discriminants (Id : E) return B;
function Has_Up_Level_Access (Id : E) return B;
+ function Has_Visible_Refinement (Id : E) return B;
function Has_Volatile_Components (Id : E) return B;
function Has_Xref_Entry (Id : E) return B;
function Hiding_Loop_Variable (Id : E) return E;
function Has_Attach_Handler (Id : E) return B;
function Has_Entries (Id : E) return B;
function Has_Foreign_Convention (Id : E) return B;
+ function Has_Non_Null_Refinement (Id : E) return B;
function Has_Null_Abstract_State (Id : E) return B;
+ function Has_Null_Refinement (Id : E) return B;
function Implementation_Base_Type (Id : E) return E;
function Is_Base_Type (Id : E) return B;
function Is_Boolean_Type (Id : E) return B;
procedure Set_Has_Missing_Return (Id : E; V : B := True);
procedure Set_Has_Nested_Block_With_Handler (Id : E; V : B := True);
procedure Set_Has_Non_Standard_Rep (Id : E; V : B := True);
- procedure Set_Has_Null_Refinement (Id : E; V : B := True);
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True);
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True);
procedure Set_Has_Postconditions (Id : E; V : B := True);
procedure Set_Has_Unchecked_Union (Id : E; V : B := True);
procedure Set_Has_Unknown_Discriminants (Id : E; V : B := True);
procedure Set_Has_Up_Level_Access (Id : E; V : B := True);
+ procedure Set_Has_Visible_Refinement (Id : E; V : B := True);
procedure Set_Has_Volatile_Components (Id : E; V : B := True);
procedure Set_Has_Xref_Entry (Id : E; V : B := True);
procedure Set_Hiding_Loop_Variable (Id : E; V : E);
pragma Inline (Has_Missing_Return);
pragma Inline (Has_Nested_Block_With_Handler);
pragma Inline (Has_Non_Standard_Rep);
- pragma Inline (Has_Null_Refinement);
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Per_Object_Constraint);
pragma Inline (Has_Postconditions);
pragma Inline (Has_Unchecked_Union);
pragma Inline (Has_Unknown_Discriminants);
pragma Inline (Has_Up_Level_Access);
+ pragma Inline (Has_Visible_Refinement);
pragma Inline (Has_Volatile_Components);
pragma Inline (Has_Xref_Entry);
pragma Inline (Hiding_Loop_Variable);
pragma Inline (Set_Has_Missing_Return);
pragma Inline (Set_Has_Nested_Block_With_Handler);
pragma Inline (Set_Has_Non_Standard_Rep);
- pragma Inline (Set_Has_Null_Refinement);
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Per_Object_Constraint);
pragma Inline (Set_Has_Postconditions);
pragma Inline (Set_Has_Unchecked_Union);
pragma Inline (Set_Has_Unknown_Discriminants);
pragma Inline (Set_Has_Up_Level_Access);
+ pragma Inline (Set_Has_Visible_Refinement);
pragma Inline (Set_Has_Volatile_Components);
pragma Inline (Set_Has_Xref_Entry);
pragma Inline (Set_Hiding_Loop_Variable);
-- (They have the sloc of the label as found in the source, and that
-- is ahead of the current declarative part).
+ procedure Remove_Visible_Refinements (Spec_Id : Entity_Id);
+ -- Spec_Id is the entity of a package that may define abstract states.
+ -- If the states have visible refinement, remove the visibility of each
+ -- constituent at the end of the package body declarations.
+
-----------------
-- Adjust_Decl --
-----------------
end loop;
end Adjust_Decl;
+ --------------------------------
+ -- Remove_Visible_Refinements --
+ --------------------------------
+
+ procedure Remove_Visible_Refinements (Spec_Id : Entity_Id) is
+ State_Elmt : Elmt_Id;
+
+ begin
+ if Present (Abstract_States (Spec_Id)) then
+ State_Elmt := First_Elmt (Abstract_States (Spec_Id));
+ while Present (State_Elmt) loop
+ Set_Has_Visible_Refinement (Node (State_Elmt), False);
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+ end Remove_Visible_Refinements;
+
-- Local variables
Body_Id : Entity_Id;
Prag : Node_Id;
Spec_Id : Entity_Id;
+ In_Package_Body : Boolean := False;
+ -- Flag set when the current declaration list belongs to a package body
+
-- Start of processing for Analyze_Declarations
begin
-- Refined_Global because the last two may mention constituents.
elsif Nkind (Context) = N_Package_Body then
+ In_Package_Body := True;
+
Body_Id := Defining_Entity (Context);
Spec_Id := Corresponding_Spec (Context);
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
Next (Decl);
end loop;
+
+ -- State refinements are visible upto the end the of the package body
+ -- declarations. Hide the refinements from visibility to restore the
+ -- original state conditions.
+
+ if In_Package_Body then
+ Remove_Visible_Refinements (Spec_Id);
+ end if;
end Analyze_Declarations;
-----------------------------------
-- appear in pragma [Refined_]Global as its place must
-- be taken by some of its constituents.
- elsif not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
- then
+ elsif Has_Visible_Refinement (Item_Id) then
Error_Msg_NE
("cannot mention state & in global refinement, "
& "use its constituents instead", Item, Item_Id);
-- in pragma [Refined_]Global as its place must be taken by
-- some of its constituents.
- elsif not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
- then
+ elsif Has_Visible_Refinement (Item_Id) then
Error_Msg_NE
("cannot mention state & in global refinement, use its "
& "constituents instead", Item, Item_Id);
-- Depends => (<output> => State)
-- Refined_Depends => (<output> => (C1, C2))
- elsif not Is_Empty_Elmt_List
- (Refinement_Constituents (Dep_Id))
- then
+ elsif Has_Non_Null_Refinement (Dep_Id) then
Has_Refined_State := True;
if Is_Entity_Name (Ref_Input) then
-- Refined_Depends => (C1 => <input>,
-- C2 => <input>)
- elsif not Is_Empty_Elmt_List
- (Refinement_Constituents (Dep_Id))
- then
+ elsif Has_Non_Null_Refinement (Dep_Id) then
Has_Refined_State := True;
-- Store the entities of all output constituents of an
-- Ensure that one of the three coverage variants is satisfied
if Ekind (Item_Id) = E_Abstract_State
- and then not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
+ and then Has_Non_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
-- is of mode Input.
if Ekind (Item_Id) = E_Abstract_State
- and then not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
+ and then Has_Non_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
-- have mode Output.
if Ekind (Item_Id) = E_Abstract_State
- and then not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
+ and then Has_Non_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
-- occurrences in Global and Refined_Global match.
if No (Refined_State (Item_Id))
- and then Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id))
+ and then not Has_Visible_Refinement (Item_Id)
then
Check_Matching_Modes (Item_Id);
end if;
Add_Item (Constit_Id, Constituents_Seen);
Remove_Elmt (Hidden_States, State_Elmt);
- -- Establish a relation between the refined state and its
- -- constituent.
+ -- Collect the constituent in the list of refinement
+ -- items. Establish a relation between the refined state
+ -- and its constituent.
Append_Elmt
(Constit_Id, Refinement_Constituents (State_Id));
Set_Refined_State (Constit_Id, State_Id);
+ -- The state has at least one legal constituent, mark the
+ -- start of the refinement region. The region ends when
+ -- the body declarations end (see Analyze_Declarations).
+
+ Set_Has_Visible_Refinement (State_Id);
+
return;
end if;
Error_Msg_N
("cannot mix null and non-null constituents", Constit);
- -- Mark the related state as having a null refinement
-
else
Null_Seen := True;
- Set_Has_Null_Refinement (State_Id);
+
+ -- Collect the constituent in the list of refinement items
+
+ Append_Elmt (Constit, Refinement_Constituents (State_Id));
+
+ -- The state has at least one legal constituent, mark the
+ -- start of the refinement region. The region ends when the
+ -- body declarations end (see Analyze_Declarations).
+
+ Set_Has_Visible_Refinement (State_Id);
end if;
-- Non-null constituents
if Ekind (Item_Id) = E_Abstract_State then
if Has_Null_Refinement (Item_Id) then
Has_Null_State := True;
- elsif Mode = Name_Input then
- Has_In_State := True;
- elsif Mode = Name_In_Out then
- Has_In_Out_State := True;
- elsif Mode = Name_Output then
- Has_Out_State := True;
+
+ elsif Has_Non_Null_Refinement (Item_Id) then
+ if Mode = Name_Input then
+ Has_In_State := True;
+ elsif Mode = Name_In_Out then
+ Has_In_Out_State := True;
+ elsif Mode = Name_Output then
+ Has_Out_State := True;
+ end if;
end if;
end if;
return
Ekind (Item_Id) = E_Abstract_State
- and then not Is_Empty_Elmt_List
- (Refinement_Constituents (Item_Id));
+ and then Has_Visible_Refinement (Item_Id);
end if;
end Is_Refined_State;
projects / platform / upstream / gcc.git / commitdiff