[Ada] Handling of null refinements in aspect/pragma Refined_Global
Arnaud Charlet
charlet@adacore.com
Mon Oct 14 12:45:00 GMT 2013
This patch updates the analysis of aspect/pragma Refined_Global to accept
legal global refinements of states with null visible refinements.
------------
-- Source --
------------
-- global_null.ads
package Global_Null
with Abstract_State =>
((In_State with External, Input_Only),
(In_Error with External, Input_Only),
In_Out_State,
In_Out_Error,
(Out_State with External, Output_Only),
(Out_Error with External, Output_Only))
is
In_Var : Integer;
In_Out_Var : Integer;
Out_Var : Integer;
procedure OK_1
with Global =>
(Input => In_State,
In_Out => In_Out_State,
Output => Out_State);
procedure OK_2
with Global =>
(Input => In_State,
In_Out => In_Out_State,
Output => Out_State);
procedure OK_3
with Global =>
(Input => (In_State, In_Var),
In_Out => (In_Out_State, In_Out_Var),
Output => (Out_State, Out_Var));
procedure Error_1
with Global =>
(Input => In_Error,
In_Out => In_Out_Error,
Output => Out_Error);
procedure Error_2
with Global =>
(Input => In_Error,
In_Out => In_Out_Error,
Output => Out_Error);
procedure Error_3
with Global =>
(Input => (In_Error, In_Var),
In_Out => (In_Out_Error, In_Out_Var),
Output => (Out_Error, Out_Var));
end Global_Null;
-- global_null.adb
package body Global_Null
with Refined_State =>
(In_State => null,
In_Error => Var_1,
In_Out_State => null,
In_Out_Error => Var_2,
Out_State => null,
Out_Error => Var_3)
is
procedure OK_1
with Refined_Global => null
is begin null; end OK_1;
procedure OK_2
with Refined_Global =>
(Input => null,
In_Out => null,
Output => null)
is begin null; end OK_2;
procedure OK_3
with Refined_Global =>
(Input => In_Var,
In_Out => In_Out_Var,
Output => Out_Var)
is begin null; end OK_3;
procedure Error_1
with Refined_Global => null
is begin null; end Error_1;
procedure Error_2
with Refined_Global =>
(Input => null,
In_Out => null,
Output => null)
is begin null; end Error_2;
procedure Error_3
with Refined_Global =>
(Input => In_Var,
In_Out => In_Out_Var,
Output => Out_Var)
is begin null; end Error_3;
Var_1 : Integer;
Var_2 : Integer;
Var_3 : Integer;
end Global_Null;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnat12 -gnatd.V global_null.adb
global_null.adb:29:11: refinement cannot be null, subprogram "Error_1" has
global items
global_null.adb:33:11: global refinement of state "In_Error" must include at
least one constituent of mode Input
global_null.adb:40:11: global refinement of state "In_Error" must include at
least one constituent of mode Input
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-14 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb: Flag263 is now known as Has_Null_Refinement.
(Has_Null_Refinement): New routine.
(Set_Has_Null_Refinement): New routine.
(Write_Entity_Flags): Output the status of flag
Has_Null_Refinement.
* einfo.ads: Add new flag Has_Null_Refinement along with
comment on usage and update all nodes subject to the flag.
(Has_Null_Refinement): New routine along with pragma Inline.
(Set_Has_Null_Refinement): New rouitine along with pragma Inline.
* sem_prag.adb (Analyze_Constituent): Mark a state as having
a null refinement when the sole constituent is "null".
(Analyze_Global_List): Handle null input/output items.
(Analyze_Refined_Global_In_Decl_Part): Add local variable
Has_Null_State. Add logic to handle combinations of states
with null refinements and null global lists and/or items.
(Check_In_Out_States, Check_Input_States, Check_Output_States):
Use attribute Has_Null_Refinement to detect states with
constituents.
(Check_Refined_Global_List): Handle null input/output items.
(Process_Global_Item): Handle states with null refinements.
(Process_Global_List): Handle null input/output items.
-------------- next part --------------
Index: einfo.adb
===================================================================
--- einfo.adb (revision 203523)
+++ einfo.adb (working copy)
@@ -551,8 +551,8 @@
-- Has_Delayed_Rep_Aspects Flag261
-- May_Inherit_Delayed_Rep_Aspects Flag262
+ -- Has_Null_Refinement Flag263
- -- (unused) Flag263
-- (unused) Flag264
-- (unused) Flag265
-- (unused) Flag266
@@ -1483,6 +1483,12 @@
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));
@@ -4104,6 +4110,12 @@
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));
@@ -7957,6 +7969,7 @@
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));
Index: einfo.ads
===================================================================
--- einfo.ads (revision 203522)
+++ einfo.ads (working copy)
@@ -505,10 +505,10 @@
-- Can_Never_Be_Null (Flag38)
-- This flag is defined in all entities, but can only be set in an object
--- which can never have a null value. This is set True for constant
--- access values initialized to a non-null value. This is also True for
--- all access parameters in Ada 83 and Ada 95 modes, and for access
--- parameters that explicitly exclude null in Ada 2005.
+-- which can never have a null value. Set for constant access values
+-- initialized to a non-null value. This is also set for all access
+-- parameters in Ada 83 and Ada 95 modes, and for access parameters
+-- that explicitly exclude null in Ada 2005.
--
-- This is used to avoid unnecessary resetting of the Is_Known_Non_Null
-- flag for such entities. In Ada 2005 mode, this is also used when
@@ -651,7 +651,7 @@
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
-- represent task and protected types (Is_Concurrent_Record_Type flag
--- set True). Points to the entity for the corresponding task type or
+-- set). Points to the entity for the corresponding task type or the
-- protected type.
-- Corresponding_Discriminant (Node19)
@@ -1361,14 +1361,14 @@
-- of derived type declarations).
-- Has_All_Calls_Remote (Flag79)
--- Defined in all library unit entities. Set true if the library unit
--- has an All_Calls_Remote pragma. Note that such entities must also
--- be RCI entities, so the flag Is_Remote_Call_Interface will always
--- be set if this flag is set.
+-- Defined in all library unit entities. Set if the library unit has an
+-- All_Calls_Remote pragma. Note that such entities must also be RCI
+-- entities, so the flag Is_Remote_Call_Interface will always be set if
+-- this flag is set.
-- Has_Anonymous_Master (Flag253)
-- Defined in units (top-level functions and procedures, library-level
--- packages). Set to True if the associated unit contains a heterogeneous
+-- packages). Set if the associated unit contains a heterogeneous
-- finalization master. The master's name is of the form <unit>AM and it
-- services anonymous access-to-controlled types with an undetermined
-- lifetime.
@@ -1438,11 +1438,11 @@
-- in sem_aux is used to test for this case.
-- Has_Contiguous_Rep (Flag181)
--- Defined in enumeration types. True if the type as a representation
+-- Defined in enumeration types. Set if the type as a representation
-- clause whose entries are successive integers.
-- Has_Controlling_Result (Flag98)
--- Defined in E_Function entities. True if the function is a primitive
+-- Defined in E_Function entities. Set if the function is a primitive
-- function of a tagged type which can dispatch on result.
-- Has_Controlled_Component (Flag43) [base type only]
@@ -1452,13 +1452,13 @@
-- Has_Controlled_Component is set for at least one component).
-- Has_Convention_Pragma (Flag119)
--- Defined in all entities. Set true for an entity for which a valid
--- Convention, Import, or Export pragma has been given. Used to prevent
--- more than one such pragma appearing for a given entity (RM B.1(45)).
+-- Defined in all entities. Set for an entity for which a valid pragma
+-- Convention, Import, or Export has been given. Used to prevent more
+-- than one such pragma appearing for a given entity (RM B.1(45)).
-- Has_Delayed_Aspects (Flag200)
--- Defined in all entities. Set true if the Rep_Item chain for the entity
--- has one or more N_Aspect_Definition nodes chained which are not to be
+-- Defined in all entities. Set if the Rep_Item chain for the entity has
+-- one or more N_Aspect_Definition nodes chained which are not to be
-- evaluated till the freeze point. The aspect definition expression
-- clause has been preanalyzed to get visibility at the point of use,
-- but no other action has been taken.
@@ -1531,18 +1531,18 @@
-- Convention_Intrinsic, Convention_Entry or Convention_Protected).
-- Has_Forward_Instantiation (Flag175)
--- Defined in package entities. Set true for packages that contain
--- instantiations of local generic entities, before the corresponding
--- generic body has been seen. If a package has a forward instantiation,
--- we cannot inline subprograms appearing in the same package because
--- the placement requirements of the instance will conflict with the
--- linear elaboration of front-end inlining.
+-- Defined in package entities. Set for packages that instantiate local
+-- generic entities before the corresponding generic body has been seen.
+-- If a package has a forward instantiation, we cannot inline subprograms
+-- appearing in the same package because the placement requirements of
+-- the instance will conflict with the linear elaboration of front-end
+-- inlining.
-- Has_Fully_Qualified_Name (Flag173)
--- Defined in all entities. Set True if the name in the Chars field has
--- been replaced by the fully qualified name, as used for debug output.
--- See Exp_Dbug for a full description of the use of this flag and also
--- the related flag Has_Qualified_Name.
+-- Defined in all entities. Set if the name in the Chars field has been
+-- replaced by the fully qualified name, as used for debug output. See
+-- Exp_Dbug for a full description of the use of this flag and also the
+-- related flag Has_Qualified_Name.
-- Has_Gigi_Rep_Item (Flag82)
-- Defined in all entities. Set if the rep item chain (referenced by
@@ -1576,7 +1576,7 @@
-- applies (as set by coresponding pragma or aspect specification).
-- Has_Inheritable_Invariants (Flag248)
--- Defined in all type entities. Set True in private types from which one
+-- Defined in all type entities. Set in private types from which one
-- or more Invariant'Class aspects will be inherited if a another type is
-- derived from the type (i.e. those types which have an Invariant'Class
-- aspect, or which inherit one or more Invariant'Class aspects). Also
@@ -1599,7 +1599,7 @@
-- Interrupt_Handler applies.
-- Has_Invariants (Flag232)
--- Defined in all type entities and in subprogram entities. Set True in
+-- Defined in all type entities and in subprogram entities. Set in
-- private types if an Invariant or Invariant'Class aspect applies to the
-- type, or if the type inherits one or more Invariant'Class aspects.
-- Also set in the corresponding full type. Note: if this flag is set
@@ -1650,15 +1650,19 @@
-- 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
+-- refinement in aspect/pragma Refined_State.
+
-- Has_Object_Size_Clause (Flag172)
-- Defined in entities for types and subtypes. Set if an Object_Size
-- clause has been processed for the type Used to prevent multiple
-- Object_Size clauses for a given entity.
-- Has_Per_Object_Constraint (Flag154)
--- Defined in E_Component entities, true if the subtype of the
--- component has a per object constraint. Per object constraints result
--- from the following situations:
+-- Defined in E_Component entities. Set if the subtype of the component
+-- has a per object constraint. Per object constraints result from the
+-- following situations :
--
-- 1. N_Attribute_Reference - when the prefix is the enclosing type and
-- the attribute is Access.
@@ -1770,27 +1774,27 @@
-- some ancestor is derived from a private type, making some components
-- invisible and aggregates illegal. Used to check the legality of
-- selected components and aggregates. The flag is set at the point of
--- derivation.
--- The legality of an aggregate of a type with a private ancestor must
--- be checked because it also depends on the visibility at the point the
--- aggregate is resolved. See sem_aggr.adb. This is part of AI05-0115.
+-- derivation. The legality of an aggregate of a type with a private
+-- ancestor must be checked because it also depends on the visibility
+-- at the point the aggregate is resolved. See sem_aggr.adb. This is
+-- part of AI05-0115.
-- Has_Private_Declaration (Flag155)
--- Defined in all entities. Returns True if it is the defining entity
--- of a private type declaration or its corresponding full declaration.
--- This flag is thus preserved when the full and the partial views are
--- exchanged, to indicate if a full type declaration is a completion.
--- Used for semantic checks in E.4(18) and elsewhere.
+-- Defined in all entities. Set if it is the defining entity of a private
+-- type declaration or its corresponding full declaration. This flag is
+-- thus preserved when the full and the partial views are exchanged, to
+-- indicate if a full type declaration is a completion. Used for semantic
+-- checks in E.4(18) and elsewhere.
-- Has_Qualified_Name (Flag161)
--- Defined in all entities. Set True if the name in the Chars field
--- has been replaced by its qualified name, as used for debug output.
--- See Exp_Dbug for a full description of qualification requirements.
--- For some entities, the name is the fully qualified name, but there
--- are exceptions. In particular, for local variables in procedures,
--- we do not include the procedure itself or higher scopes. See also
--- the flag Has_Fully_Qualified_Name, which is set if the name does
--- indeed include the fully qualified name.
+-- Defined in all entities. Set if the name in the Chars field has
+-- been replaced by its qualified name, as used for debug output. See
+-- Exp_Dbug for a full description of qualification requirements. For
+-- some entities, the name is the fully qualified name, but there are
+-- exceptions. In particular, for local variables in procedures, we
+-- do not include the procedure itself or higher scopes. See also the
+-- flag Has_Fully_Qualified_Name, which is set if the name does indeed
+-- include the fully qualified name.
-- Has_RACW (Flag214)
-- Defined in package spec entities. Set if the spec contains the
@@ -2168,7 +2172,7 @@
-- Set if the type or subtype is constrained.
-- Is_Constr_Subt_For_U_Nominal (Flag80)
--- Defined in all types and subtypes. Set true only for the constructed
+-- Defined in all types and subtypes. Set only for the constructed
-- subtype of an object whose nominal subtype is unconstrained. Note
-- that the constructed subtype itself will be constrained.
@@ -2225,9 +2229,9 @@
-- entity is associated with a dispatch table.
-- Is_Dispatching_Operation (Flag6)
--- Defined in all entities. Set true for procedures, functions,
--- generic procedures and generic functions if the corresponding
--- operation is dispatching.
+-- Defined in all entities. Set for procedures, functions, generic
+-- procedures, and generic functions if the corresponding operation
+-- is dispatching.
-- Is_Dynamic_Scope (synthesized)
-- Applies to all Entities. Returns True if the entity is a dynamic
@@ -2253,9 +2257,9 @@
-- entities and False for all other entity kinds.
-- Is_Entry_Formal (Flag52)
--- Defined in all entities. Set only for entry formals (which can
--- only be in, in-out or out parameters). This flag is used to speed
--- up the test for the need to replace references in Exp_Ch2.
+-- Defined in all entities. Set only for entry formals (which can only
+-- be in, in-out or out parameters). This flag is used to speed up the
+-- test for the need to replace references in Exp_Ch2.
-- Is_Exported (Flag99)
-- Defined in all entities. Set if the entity is exported. For now we
@@ -2338,7 +2342,7 @@
-- convention.
-- Is_Hidden (Flag57)
--- Defined in all entities. Set true for all entities declared in the
+-- Defined in all entities. Set for all entities declared in the
-- private part or body of a package. Also marks generic formals of a
-- formal package declared without a box. For library level entities,
-- this flag is set if the entity is not publicly visible. This flag
@@ -2348,7 +2352,7 @@
-- Private_Declaration in sem_ch7).
-- Is_Hidden_Open_Scope (Flag171)
--- Defined in all entities. Set true for a scope that contains the
+-- Defined in all entities. Set for a scope that contains the
-- instantiation of a child unit, and whose entities are not visible
-- during analysis of the instance.
@@ -2462,20 +2466,20 @@
-- to be defined) must be in the same scope as the type.
-- Is_Known_Non_Null (Flag37)
--- Defined in all entities. Relevant (and can be set True) only for
+-- Defined in all entities. Relevant (and can be set) only for
-- objects of an access type. It is set if the object is currently
-- known to have a non-null value (meaning that no access checks
-- are needed). The indication can for example come from assignment
-- of an access parameter or an allocator whose value is known non-null.
--
-- Note: this flag is set according to the sequential flow of the
--- program, watching the current value of the variable. However,
--- this processing can miss cases of changing the value of an aliased
--- or constant object, so even if this flag is set, it should not
--- be believed if the variable is aliased or volatile. It would
--- be a little neater to avoid the flag being set in the first
--- place in such cases, but that's trickier, and there is only
--- one place that tests the value anyway.
+-- program, watching the current value of the variable. However, this
+-- processing can miss cases of changing the value of an aliased or
+-- constant object, so even if this flag is set, it should not be
+-- believed if the variable is aliased or volatile. It would be a
+-- little neater to avoid the flag being set in the first place in
+-- such cases, but that's trickier, and there is only one place that
+-- tests the value anyway.
--
-- The flag is dynamically set and reset as semantic analysis and
-- expansion proceeds. Its value is meaningless once the tree is
@@ -2483,7 +2487,7 @@
-- Thus this flag has no meaning to the back end.
-- Is_Known_Null (Flag204)
--- Defined in all entities. Relevant (and can be set True) only for
+-- Defined in all entities. Relevant (and can be set ) only for
-- objects of an access type. It is set if the object is currently known
-- to have a null value (meaning that a dereference will surely raise
-- constraint error exception). The indication can come from an
@@ -2841,7 +2845,7 @@
-- Wide_Wide_Character).
-- Is_Statically_Allocated (Flag28)
--- Defined in all entities. This can only be set True for exception,
+-- Defined in all entities. This can only be set for exception,
-- variable, constant, and type/subtype entities. If the flag is set,
-- then the variable or constant must be allocated statically rather
-- than on the local stack frame. For exceptions, the meaning is that
@@ -2951,7 +2955,7 @@
-- or Export_Valued_Procedure pragma applies to the procedure entity.
-- Is_Visible_Formal (Flag206)
--- Defined in all entities. Set True for instances of the formals of a
+-- Defined in all entities. Set for instances of the formals of a
-- formal package. Indicates that the entity must be made visible in the
-- body of the instance, to reproduce the visibility of the generic.
-- This simplifies visibility settings in instance bodies.
@@ -3058,10 +3062,10 @@
-- Value attributes for the enumeration type in question.
-- Low_Bound_Tested (Flag205)
--- Defined in all entities. Currently this can only be set True for
--- formal parameter entries of a standard unconstrained one-dimensional
--- array or string type. Indicates that an explicit test of the low bound
--- of the formal appeared in the code, e.g. in a pragma Assert. If this
+-- Defined in all entities. Currently this can only be set for formal
+-- parameter entries of a standard unconstrained one-dimensional array
+-- or string type. Indicates that an explicit test of the low bound of
+-- the formal appeared in the code, e.g. in a pragma Assert. If this
-- flag is set, warnings about assuming the index low bound to be one
-- are suppressed.
@@ -3252,8 +3256,8 @@
-- the defining entity in the original declaration.
-- Nonzero_Is_True (Flag162) [base type only]
--- Defined in enumeration types. True if any non-zero value is to be
--- interpreted as true. Currently this is set true for derived Boolean
+-- Defined in enumeration types. Set if any non-zero value is to be
+-- interpreted as true. Currently this is set for derived Boolean
-- types which have a convention of C, C++ or Fortran.
-- No_Pool_Assigned (Flag131) [root type only]
@@ -3796,8 +3800,8 @@
-- Static_Predicate (List25)
-- Defined in discrete types/subtypes with predicates (Has_Predicates
--- set True). Set if the type/subtype has a static predicate. Points to
--- a list of expression and N_Range nodes that represent the predicate
+-- set). Set if the type/subtype has a static predicate. Points to a
+-- list of expression and N_Range nodes that represent the predicate
-- in canonical form. The canonical form has entries sorted in ascending
-- order, with duplicates eliminated, and adjacent ranges coalesced, so
-- that there is always a gap in the values between successive entries.
@@ -5104,6 +5108,7 @@
-- E_Abstract_State
-- Refinement_Constituents (Elist8)
-- Refined_State (Node10)
+ -- Has_Null_Refinement (Flag263)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
@@ -6344,6 +6349,7 @@
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;
@@ -6957,6 +6963,7 @@
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);
@@ -7672,6 +7679,7 @@
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);
@@ -8132,6 +8140,7 @@
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);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203525)
+++ sem_prag.adb (working copy)
@@ -1600,11 +1600,14 @@
-- Start of processing for Analyze_Global_List
begin
+ if Nkind (List) = N_Null then
+ null;
+
-- Single global item declaration
- if Nkind_In (List, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
then
Analyze_Global_Item (List, Global_Mode);
@@ -1691,7 +1694,7 @@
-- Local variables
- List : Node_Id;
+ Items : Node_Id;
Subp_Decl : Node_Id;
Restore_Scope : Boolean := False;
@@ -1704,11 +1707,11 @@
Subp_Decl := Find_Related_Subprogram (N);
Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
- List := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Items := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-- There is nothing to be done for a null global list
- if Nkind (List) = N_Null then
+ if Nkind (Items) = N_Null then
null;
-- Analyze the various forms of global lists and items. Note that some
@@ -1726,7 +1729,7 @@
Install_Formals (Subp_Id);
end if;
- Analyze_Global_List (List);
+ Analyze_Global_List (Items);
if Restore_Scope then
End_Scope;
@@ -19358,6 +19361,10 @@
-- a state of mode Input, In_Out and Output respectively with a visible
-- refinement.
+ Has_Null_State : Boolean := False;
+ -- This flag is set when the corresponding Global aspect/pragma has at
+ -- least one state with a null refinement.
+
In_Constits : Elist_Id := No_Elist;
In_Out_Constits : Elist_Id := No_Elist;
Out_Constits : Elist_Id := No_Elist;
@@ -19512,7 +19519,7 @@
-- Ensure that one of the three coverage variants is satisfied
if Ekind (Item_Id) = E_Abstract_State
- and then Present (Refinement_Constituents (Item_Id))
+ and then not Has_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -19595,7 +19602,7 @@
-- is of mode Input.
if Ekind (Item_Id) = E_Abstract_State
- and then Present (Refinement_Constituents (Item_Id))
+ and then not Has_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -19665,7 +19672,7 @@
-- have mode Output.
if Ekind (Item_Id) = E_Abstract_State
- and then Present (Refinement_Constituents (Item_Id))
+ and then not Has_Null_Refinement (Item_Id)
then
Check_Constituent_Usage (Item_Id);
end if;
@@ -19881,11 +19888,14 @@
-- Start of processing for Check_Refined_Global_List
begin
+ if Nkind (List) = N_Null then
+ null;
+
-- Single global item declaration
- if Nkind_In (List, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
then
Check_Refined_Global_Item (List, Global_Mode);
@@ -19963,17 +19973,20 @@
begin
-- Signal that the global list contains at least one abstract
- -- state with a visible refinement.
+ -- state with a visible refinement. Note that the refinement
+ -- may be null in which case there are no constituents.
- if Ekind (Item_Id) = E_Abstract_State
- and then Present (Refinement_Constituents (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;
+ if Ekind (Item_Id) = E_Abstract_State then
+ if Has_Null_Refinement (Item_Id) then
+ Has_Null_State := True;
+ else
+ 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;
@@ -19995,11 +20008,14 @@
-- Start of processing for Process_Global_List
begin
+ if Nkind (List) = N_Null then
+ null;
+
-- Single global item declaration
- if Nkind_In (List, N_Expanded_Name,
- N_Identifier,
- N_Selected_Component)
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
then
Process_Global_Item (List, Mode);
@@ -20148,11 +20164,13 @@
-- The corresponding Global aspect/pragma must mention at least one
-- state with a visible refinement at the point Refined_Global is
- -- processed.
+ -- processed. States with null refinements warrant a Refined_Global
+ -- aspect/pragma.
if not Has_In_State
and then not Has_In_Out_State
and then not Has_Out_State
+ and then not Has_Null_State
then
Error_Msg_NE
("useless refinement, subprogram & does not mention abstract state "
@@ -20161,13 +20179,15 @@
end if;
-- The global refinement of inputs and outputs cannot be null when the
- -- corresponding Global aspect/pragma contains at least one item.
+ -- corresponding Global aspect/pragma contains at least one item except
+ -- in the case where we have states with null refinements.
if Nkind (List) = N_Null
and then
(Present (In_Items)
or else Present (In_Out_Items)
or else Present (Out_Items))
+ and then not Has_Null_State
then
Error_Msg_NE
("refinement cannot be null, subprogram & has global items",
@@ -20370,8 +20390,11 @@
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);
end if;
-- Non-null constituents
More information about the Gcc-patches
mailing list