einfo.adb: Flag 263 is now known as Has_Visible_Refinement.
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. From-SVN: r203546
This commit is contained in:
Hristian Kirtchev
Arnaud Charlet
parent
26168a32da
commit
c5c0ce68a4
|
|
@ -1,3 +1,46 @@
|
|||
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
|
||||
|
|
|
|||
|
|
@ -551,7 +551,7 @@ package body Einfo is
|
|||
|
||||
-- Has_Delayed_Rep_Aspects Flag261
|
||||
-- May_Inherit_Delayed_Rep_Aspects Flag262
|
||||
-- Has_Null_Refinement Flag263
|
||||
-- Has_Visible_Refinement Flag263
|
||||
|
||||
-- (unused) Flag264
|
||||
-- (unused) Flag265
|
||||
|
|
@ -1483,12 +1483,6 @@ package body Einfo is
|
|||
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));
|
||||
|
|
@ -1716,6 +1710,12 @@ package body Einfo is
|
|||
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));
|
||||
|
|
@ -4110,12 +4110,6 @@ package body Einfo is
|
|||
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));
|
||||
|
|
@ -4343,6 +4337,12 @@ package body Einfo is
|
|||
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));
|
||||
|
|
@ -6471,6 +6471,29 @@ package body Einfo is
|
|||
return False;
|
||||
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 --
|
||||
-----------------------------
|
||||
|
|
@ -6484,6 +6507,29 @@ package body Einfo is
|
|||
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 --
|
||||
--------------------
|
||||
|
|
@ -7969,7 +8015,6 @@ package body Einfo is
|
|||
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));
|
||||
|
|
@ -8011,6 +8056,7 @@ package body Einfo is
|
|||
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));
|
||||
|
|
|
|||
|
|
@ -1636,6 +1636,10 @@ package Einfo is
|
|||
-- 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
|
||||
|
|
@ -1650,8 +1654,8 @@ package Einfo is
|
|||
-- 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)
|
||||
|
|
@ -1913,6 +1917,11 @@ package Einfo is
|
|||
-- 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
|
||||
|
|
@ -5108,7 +5117,9 @@ package Einfo is
|
|||
-- 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)
|
||||
|
|
@ -6349,7 +6360,6 @@ package Einfo is
|
|||
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;
|
||||
|
|
@ -6391,6 +6401,7 @@ package Einfo is
|
|||
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;
|
||||
|
|
@ -6696,7 +6707,9 @@ package Einfo is
|
|||
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;
|
||||
|
|
@ -6963,7 +6976,6 @@ package Einfo is
|
|||
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);
|
||||
|
|
@ -7005,6 +7017,7 @@ package Einfo is
|
|||
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);
|
||||
|
|
@ -7679,7 +7692,6 @@ package Einfo is
|
|||
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);
|
||||
|
|
@ -7721,6 +7733,7 @@ package Einfo is
|
|||
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);
|
||||
|
|
@ -8140,7 +8153,6 @@ package Einfo is
|
|||
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);
|
||||
|
|
@ -8182,6 +8194,7 @@ package Einfo is
|
|||
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);
|
||||
|
|
|
|||
|
|
@ -2067,6 +2067,11 @@ package body Sem_Ch3 is
|
|||
-- (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 --
|
||||
-----------------
|
||||
|
|
@ -2080,6 +2085,24 @@ package body Sem_Ch3 is
|
|||
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;
|
||||
|
|
@ -2089,6 +2112,9 @@ package body Sem_Ch3 is
|
|||
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
|
||||
|
|
@ -2220,6 +2246,8 @@ package body Sem_Ch3 is
|
|||
-- 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);
|
||||
|
|
@ -2256,6 +2284,14 @@ package body Sem_Ch3 is
|
|||
|
||||
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;
|
||||
|
||||
-----------------------------------
|
||||
|
|
|
|||
|
|
@ -798,9 +798,7 @@ package body Sem_Prag is
|
|||
-- 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);
|
||||
|
|
@ -1625,9 +1623,7 @@ package body Sem_Prag is
|
|||
-- 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);
|
||||
|
|
@ -19677,9 +19673,7 @@ package body Sem_Prag is
|
|||
-- 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
|
||||
|
|
@ -20033,9 +20027,7 @@ package body Sem_Prag is
|
|||
-- 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
|
||||
|
|
@ -20452,8 +20444,7 @@ package body Sem_Prag is
|
|||
-- 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;
|
||||
|
|
@ -20536,8 +20527,7 @@ package body Sem_Prag is
|
|||
-- 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;
|
||||
|
|
@ -20607,8 +20597,7 @@ package body Sem_Prag is
|
|||
-- 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;
|
||||
|
|
@ -20730,8 +20719,7 @@ package body Sem_Prag is
|
|||
-- 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;
|
||||
|
|
@ -21088,13 +21076,20 @@ package body Sem_Prag is
|
|||
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;
|
||||
|
||||
|
|
@ -21129,11 +21124,18 @@ package body Sem_Prag is
|
|||
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
|
||||
|
|
@ -21717,12 +21719,15 @@ package body Sem_Prag is
|
|||
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;
|
||||
|
||||
|
|
|
|||
|
|
@ -3418,8 +3418,7 @@ package body Sem_Util is
|
|||
|
||||
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;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue