===================================================================
@@ -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));
===================================================================
@@ -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. 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). 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 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 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. Set if the type as a representation
-- clause whose entries are successive integers.
-- Has_Controlling_Result (Flag98)
+-- 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 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 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 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 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 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 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. 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.
-- Has_Private_Declaration (Flag155)
+-- 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 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 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 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.
-- 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 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 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) 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.
--
-- 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 ) 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 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 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 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. 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). 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);
===================================================================
@@ -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