+2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb: Remove Integrity_Level from the node usage list.
+ (Has_Option): Update the implementation to match
+ the new terminology.
+ (Has_Property): Renamed to Has_Option.
+ (Integrity_Level): Removed.
+ (Is_External_State): New routine.
+ (Is_Input_Only_State): Use Has_Option to determine whether a state
+ is Input_Only. (Is_Input_State): Renamed to Is_Input_Only_State.
+ (Is_Output_Only_State): Use Has_Option to determine whether
+ a state is Output_Only.
+ (Is_Output_State): Renamed to
+ Is_Output_Only_State.
+ (Is_Volatile_State): Use Has_Option to determine whether a state is
+ volatile.
+ (Set_Integrity_Level): Removed.
+ (Write_Field8): Remove the entry for Integrity_Level.
+ * einfo.ads: Remove Integrity_Level along with its documentation
+ and usage in nodes. Rename Is_Input_State to Is_Input_Only_State.
+ Rename Is_Output_State to Is_Output_Only_State. Update the
+ documentation of Is_Volatile_State. Update the node structure of
+ E_Abstract_Entity.
+ (Integrity_Level): Removed along with pragma Inline.
+ (Is_External_State): New routine.
+ (Is_Input_State): Renamed to Is_Input_Only_State.
+ (Is_Output_State): Renamed to Is_Output_Only_State.
+ (Set_Integrity_Level): Removed along with pragma Inline.
+ * sem_prag.adb (Analyze_Pragma): Update the checks regarding
+ global items and abstract state modes. Update the implementation
+ of pragma Abstract_State to reflect the new rules and terminology.
+ * snames.ads-tmpl: Remove the predefined name for Integrity
+ level. Add new predefined names for Input_Only, Non_Volatile,
+ Output_Only and Part_Of.
+
+2013-10-10 Ed Schonberg <schonberg@adacore.com>
+
+ * lib-xref.adb (Generate_Reference): Do not generate a reference
+ within a _postcondition procedure: a proper source reference has
+ already been generated when pre- analyzing the original aspect
+ specification, and the use of a formal in a pre/postcondition
+ should not count as a proper use in a subprogram body.
+
+2013-10-10 Robert Dewar <dewar@adacore.com>
+
+ * sem_eval.adb (Why_Non_Static): Fix bomb for deferred constant
+ case
+
2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb: Add an entry for Aspect_Refined_Post in table
-- Associated_Node_For_Itype Node8
-- Dependent_Instances Elist8
-- Hiding_Loop_Variable Node8
- -- Integrity_Level Uint8
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
-- Postcondition_Proc Node8
-- Local subprograms --
-----------------------
- function Has_Property
- (State : Entity_Id;
- Prop_Nam : Name_Id) return Boolean;
- -- Determine whether abstract state State has a particular property denoted
- -- by the name Prop_Nam.
+ function Has_Option
+ (State : Entity_Id;
+ Opt_Nam : Name_Id) return Boolean;
+ -- Determine whether abstract state State has a particular option denoted
+ -- by the name Opt_Nam.
---------------
-- Float_Rep --
return F'Val (UI_To_Int (Uint10 (Base_Type (Id))));
end Float_Rep;
- ------------------
- -- Has_Property --
- ------------------
+ ----------------
+ -- Has_Option --
+ ----------------
- function Has_Property
- (State : Entity_Id;
- Prop_Nam : Name_Id) return Boolean
+ function Has_Option
+ (State : Entity_Id;
+ Opt_Nam : Name_Id) return Boolean
is
- Par : constant Node_Id := Parent (State);
- Prop : Node_Id;
+ Par : constant Node_Id := Parent (State);
+ Opt : Node_Id;
begin
pragma Assert (Ekind (State) = E_Abstract_State);
- -- States with properties appear as extension aggregates in the tree
+ -- States with options appear as extension aggregates in the tree
if Nkind (Par) = N_Extension_Aggregate then
- if Prop_Nam = Name_Integrity then
+ if Opt_Nam = Name_Part_Of then
return Present (Component_Associations (Par));
else
- Prop := First (Expressions (Par));
- while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
+ Opt := First (Expressions (Par));
+ while Present (Opt) loop
+ if Chars (Opt) = Opt_Nam then
return True;
end if;
- Next (Prop);
+ Next (Opt);
end loop;
end if;
end if;
return False;
- end Has_Property;
+ end Has_Option;
--------------------------------
-- Attribute Access Functions --
return Node28 (Id);
end Initialization_Statements;
- function Integrity_Level (Id : E) return U is
- begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- return Uint8 (Id);
- end Integrity_Level;
-
function Inner_Instances (Id : E) return L is
begin
return Elist23 (Id);
Set_Node28 (Id, V);
end Set_Initialization_Statements;
- procedure Set_Integrity_Level (Id : E; V : Uint) is
- begin
- pragma Assert (Ekind (Id) = E_Abstract_State);
- Set_Uint8 (Id, V);
- end Set_Integrity_Level;
-
procedure Set_Inner_Instances (Id : E; V : L) is
begin
Set_Elist23 (Id, V);
and then Is_Entity_Attribute_Name (Attribute_Name (N)));
end Is_Entity_Name;
+ -----------------------
+ -- Is_External_State --
+ -----------------------
+
+ function Is_External_State (Id : E) return B is
+ begin
+ return
+ Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_External);
+ end Is_External_State;
+
------------------
-- Is_Finalizer --
------------------
end if;
end Is_Ghost_Subprogram;
- --------------------
- -- Is_Input_State --
- --------------------
+ -------------------------
+ -- Is_Input_Only_State --
+ -------------------------
- function Is_Input_State (Id : E) return B is
+ function Is_Input_Only_State (Id : E) return B is
begin
return
- Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Input);
- end Is_Input_State;
+ Ekind (Id) = E_Abstract_State
+ and then Has_Option (Id, Name_Input_Only);
+ end Is_Input_Only_State;
-------------------
-- Is_Null_State --
-- Is_Output_State --
---------------------
- function Is_Output_State (Id : E) return B is
+ function Is_Output_Only_State (Id : E) return B is
begin
return
- Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Output);
- end Is_Output_State;
+ Ekind (Id) = E_Abstract_State
+ and then Has_Option (Id, Name_Output_Only);
+ end Is_Output_Only_State;
-----------------------------------
-- Is_Package_Or_Generic_Package --
begin
return
Ekind (Id) = E_Abstract_State
- and then Has_Property (Id, Name_Volatile);
+ and then Has_Option (Id, Name_Volatile);
end Is_Volatile_State;
------------------------
when E_Variable =>
Write_Str ("Hiding_Loop_Variable");
- when E_Abstract_State =>
- Write_Str ("Integrity_Level");
-
when Formal_Kind |
E_Function |
E_Subprogram_Body =>
-- instantiated within the given generic. Used to diagnose circular
-- instantiations.
--- Integrity_Level (Uint8)
--- Defined for E_Abstract_State entities. Contains the numerical value of
--- the integrity level state property. A value of Uint_0 designates a non
--- existent integrity.
-
-- Interface_Alias (Node25)
-- Defined in subprograms that cover a primitive operation of an abstract
-- interface type. Can be set only if the Is_Hidden flag is also set,
-- and variables, but that may well change later on. Exceptions can only
-- be exported in the OpenVMS and Java VM implementations of GNAT.
+-- Is_External_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- option External.
+
-- Is_Finalizer (synthesized)
-- Applies to all entities, true for procedures containing finalization
-- code to process local or library level objects.
-- inherited by their instances. It is also set on the body entities
-- of inlined subprograms. See also Has_Pragma_Inline.
--- Is_Input_State (synthesized)
+-- Is_Input_Only_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
--- property Input.
+-- option Input_Only.
-- Is_Instantiated (Flag126)
-- Defined in generic packages and generic subprograms. Set if the unit
-- Applies to all entities, true for ordinary fixed point types and
-- subtypes.
--- Is_Output_State (synthesized)
+-- Is_Output_Only_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
--- property Output.
+-- option Output_Only.
-- Is_Package_Or_Generic_Package (synthesized)
-- Applies to all entities. True for packages and generic packages.
-- Is_Volatile_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
--- property Volatile.
+-- option Volatile.
-- Is_Wrapper_Package (synthesized)
-- Defined in package entities. Indicates that the package has been
------------------------------------------
-- E_Abstract_State
- -- Integrity_Level (Uint8)
-- Refined_State (Node9)
- -- Is_Input_State (synth)
+ -- Is_External_State (synth)
+ -- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
- -- Is_Output_State (synth)
+ -- Is_Output_Only_State (synth)
-- Is_Volatile_State (synth)
-- E_Access_Protected_Subprogram_Type
function In_Private_Part (Id : E) return B;
function In_Use (Id : E) return B;
function Initialization_Statements (Id : E) return N;
- function Integrity_Level (Id : E) return U;
function Inner_Instances (Id : E) return L;
function Interface_Alias (Id : E) return E;
function Interface_Name (Id : E) return N;
function Is_Constant_Object (Id : E) return B;
function Is_Discriminal (Id : E) return B;
function Is_Dynamic_Scope (Id : E) return B;
+ function Is_External_State (Id : E) return B;
function Is_Finalizer (Id : E) return B;
function Is_Ghost_Entity (Id : E) return B;
function Is_Ghost_Subprogram (Id : E) return B;
- function Is_Input_State (Id : E) return B;
+ function Is_Input_Only_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
- function Is_Output_State (Id : E) return B;
+ function Is_Output_Only_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
function Is_Prival (Id : E) return B;
function Is_Protected_Component (Id : E) return B;
procedure Set_In_Private_Part (Id : E; V : B := True);
procedure Set_In_Use (Id : E; V : B := True);
procedure Set_Initialization_Statements (Id : E; V : N);
- procedure Set_Integrity_Level (Id : E; V : U);
procedure Set_Inner_Instances (Id : E; V : L);
procedure Set_Interface_Alias (Id : E; V : E);
procedure Set_Interface_Name (Id : E; V : N);
pragma Inline (In_Package_Body);
pragma Inline (In_Private_Part);
pragma Inline (In_Use);
- pragma Inline (Integrity_Level);
pragma Inline (Inner_Instances);
pragma Inline (Interface_Alias);
pragma Inline (Interface_Name);
pragma Inline (Set_In_Private_Part);
pragma Inline (Set_In_Use);
pragma Inline (Set_Inner_Instances);
- pragma Inline (Set_Integrity_Level);
pragma Inline (Set_Interface_Alias);
pragma Inline (Set_Interface_Name);
pragma Inline (Set_Interfaces);
Error_Msg_NE ("& is only defined in Ada 2012?y?", N, E);
end if;
+ -- Do not generate references if we are within a postcondition sub-
+ -- program, because the reference does not comes from source, and the
+ -- pre-analysis of the aspect has already created an entry for the ali
+ -- file at the proper source location.
+
+ if Chars (Current_Scope) = Name_uPostconditions then
+ return;
+ end if;
+
-- Never collect references if not in main source unit. However, we omit
-- this test if Typ is 'e' or 'k', since these entries are structural,
-- and it is useful to have them in units that reference packages as
then
Error_Msg_N ("\aggregate (#) is never static", N);
- elsif not Is_Static_Expression (CV) then
+ elsif No (CV) or else not Is_Static_Expression (CV) then
Error_Msg_NE
("\& is not a static constant (RM 4.9(5))", N, E);
end if;
-- valid choices. Perform mode- and usage-specific checks.
if Ekind (Item_Id) = E_Abstract_State
- and then Is_Volatile_State (Item_Id)
+ and then Is_External_State (Item_Id)
then
- -- A global item of mode In_Out or Output cannot denote a
- -- volatile Input state.
+ -- A global item of mode In_Out or Output cannot denote an
+ -- external Input_Only state.
- if Is_Input_State (Item_Id)
+ if Is_Input_Only_State (Item_Id)
and then Nam_In (Global_Mode, Name_In_Out, Name_Output)
then
Error_Msg_N
("global item of mode In_Out or Output cannot reference "
- & "Volatile Input state", Item);
+ & "External Input_Only state", Item);
- -- A global item of mode In_Out or Input cannot reference a
- -- volatile Output state.
+ -- A global item of mode In_Out or Input cannot reference an
+ -- external Output_Only state.
- elsif Is_Output_State (Item_Id)
+ elsif Is_Output_Only_State (Item_Id)
and then Nam_In (Global_Mode, Name_In_Out, Name_Input)
then
Error_Msg_N
("global item of mode In_Out or Input cannot reference "
- & "Volatile Output state", Item);
+ & "External Output_Only state", Item);
end if;
end if;
-- ABSTRACT_STATE_LIST ::=
-- null
- -- | STATE_NAME_WITH_PROPERTIES {, STATE_NAME_WITH_PROPERTIES}
+ -- | STATE_NAME_WITH_OPTIONS
+ -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS})
- -- STATE_NAME_WITH_PROPERTIES ::=
- -- STATE_NAME
- -- | (STATE_NAME with PROPERTY_LIST)
+ -- STATE_NAME_WITH_OPTIONS ::=
+ -- state_NAME
+ -- | (state_NAME with OPTION_LIST)
- -- PROPERTY_LIST ::= PROPERTY {, PROPERTY}
- -- PROPERTY ::= SIMPLE_PROPERTY | NAME_VALUE_PROPERTY
+ -- OPTION_LIST ::= OPTION {, OPTION}
- -- SIMPLE_PROPERTY ::= IDENTIFIER
- -- NAME_VALUE_PROPERTY ::= IDENTIFIER => EXPRESSION
+ -- OPTION ::= SIMPLE_OPTION | NAME_VALUE_OPTION
- -- STATE_NAME ::= DEFINING_IDENTIFIER
+ -- SIMPLE_OPTION ::=
+ -- External | Non_Volatile | Input_Only | Output_Only
+
+ -- NAME_VALUE_OPTION ::= Part_Of => abstract_state_NAME
when Pragma_Abstract_State => Abstract_State : declare
Pack_Id : Entity_Id;
----------------------------
procedure Analyze_Abstract_State (State : Node_Id) is
- procedure Check_Duplicate_Property
- (Prop : Node_Id;
+ procedure Check_Duplicate_Option
+ (Opt : Node_Id;
Status : in out Boolean);
- -- Flag Status denotes whether a particular property has been
+ -- Flag Status denotes whether a particular option has been
-- seen while processing a state. This routine verifies that
- -- Prop is not a duplicate property and sets the flag Status.
+ -- Opt is not a duplicate property and sets the flag Status.
- ------------------------------
- -- Check_Duplicate_Property --
- ------------------------------
+ ----------------------------
+ -- Check_Duplicate_Option --
+ ----------------------------
- procedure Check_Duplicate_Property
- (Prop : Node_Id;
+ procedure Check_Duplicate_Option
+ (Opt : Node_Id;
Status : in out Boolean)
is
begin
if Status then
- Error_Msg_N ("duplicate state property", Prop);
+ Error_Msg_N ("duplicate state option", Opt);
end if;
Status := True;
- end Check_Duplicate_Property;
+ end Check_Duplicate_Option;
-- Local variables
- Errors : constant Nat := Serious_Errors_Detected;
- Loc : constant Source_Ptr := Sloc (State);
- Assoc : Node_Id;
- Id : Entity_Id;
- Is_Null : Boolean := False;
- Level : Uint := Uint_0;
- Name : Name_Id;
- Prop : Node_Id;
+ Errors : constant Nat := Serious_Errors_Detected;
+ Loc : constant Source_Ptr := Sloc (State);
+ Assoc : Node_Id;
+ Id : Entity_Id;
+ Is_Null : Boolean := False;
+ Name : Name_Id;
+ Opt : Node_Id;
+ Par_State : Node_Id;
- -- Flags used to verify the consistency of properties
+ -- Flags used to verify the consistency of options
- Input_Seen : Boolean := False;
- Integrity_Seen : Boolean := False;
- Output_Seen : Boolean := False;
- Volatile_Seen : Boolean := False;
+ External_Seen : Boolean := False;
+ Input_Seen : Boolean := False;
+ Non_Volatile_Seen : Boolean := False;
+ Output_Seen : Boolean := False;
+ Part_Of_Seen : Boolean := False;
-- Start of processing for Analyze_Abstract_State
Name := Chars (State);
Non_Null_Seen := True;
- -- State declaration with various properties. This construct
+ -- State declaration with various options. This construct
-- appears as an extension aggregate in the tree.
elsif Nkind (State) = N_Extension_Aggregate then
Ancestor_Part (State));
end if;
- -- Process properties Input, Output and Volatile. Ensure
- -- that none of them appear more than once.
-
- Prop := First (Expressions (State));
- while Present (Prop) loop
- if Nkind (Prop) = N_Identifier then
- if Chars (Prop) = Name_Input then
- Check_Duplicate_Property (Prop, Input_Seen);
- elsif Chars (Prop) = Name_Output then
- Check_Duplicate_Property (Prop, Output_Seen);
- elsif Chars (Prop) = Name_Volatile then
- Check_Duplicate_Property (Prop, Volatile_Seen);
+ -- Process options External, Input_Only, Output_Only and
+ -- Volatile. Ensure that none of them appear more than once.
+
+ Opt := First (Expressions (State));
+ while Present (Opt) loop
+ if Nkind (Opt) = N_Identifier then
+ if Chars (Opt) = Name_External then
+ Check_Duplicate_Option (Opt, External_Seen);
+ elsif Chars (Opt) = Name_Input_Only then
+ Check_Duplicate_Option (Opt, Input_Seen);
+ elsif Chars (Opt) = Name_Output_Only then
+ Check_Duplicate_Option (Opt, Output_Seen);
+ elsif Chars (Opt) = Name_Non_Volatile then
+ Check_Duplicate_Option (Opt, Non_Volatile_Seen);
+
+ -- Ensure that the abstract state component of option
+ -- Part_Of has not been omitted.
+
+ elsif Chars (Opt) = Name_Part_Of then
+ Error_Msg_N
+ ("option Part_Of requires an abstract state",
+ Opt);
else
- Error_Msg_N ("invalid state property", Prop);
+ Error_Msg_N ("invalid state option", Opt);
end if;
else
- Error_Msg_N ("invalid state property", Prop);
+ Error_Msg_N ("invalid state option", Opt);
end if;
- Next (Prop);
+ Next (Opt);
end loop;
- -- Volatile requires exactly one Input or Output
+ -- External requires exactly one Input_Only or Output_Only
- if Volatile_Seen and then Input_Seen = Output_Seen then
+ if External_Seen and then Input_Seen = Output_Seen then
Error_Msg_N
- ("property Volatile requires exactly one Input or "
- & "Output", State);
+ ("option External requires exactly one option "
+ & "Input_Only or Output_Only", State);
end if;
- -- Either Input or Output require Volatile
+ -- Either Input_Only or Output_Only require External
if (Input_Seen or Output_Seen)
- and then not Volatile_Seen
+ and then not External_Seen
then
Error_Msg_N
- ("properties Input and Output require Volatile", State);
+ ("options Input_Only and Output_Only require option "
+ & "External", State);
end if;
- -- State property Integrity appears as a component
- -- association.
+ -- Option Part_Of appears as a component association
Assoc := First (Component_Associations (State));
while Present (Assoc) loop
- Prop := First (Choices (Assoc));
- while Present (Prop) loop
- if Nkind (Prop) = N_Identifier
- and then Chars (Prop) = Name_Integrity
+ Opt := First (Choices (Assoc));
+ while Present (Opt) loop
+ if Nkind (Opt) = N_Identifier
+ and then Chars (Opt) = Name_Part_Of
then
- Check_Duplicate_Property (Prop, Integrity_Seen);
+ Check_Duplicate_Option (Opt, Part_Of_Seen);
else
- Error_Msg_N ("invalid state property", Prop);
+ Error_Msg_N ("invalid state option", Opt);
end if;
- Next (Prop);
+ Next (Opt);
end loop;
- if Nkind (Expression (Assoc)) = N_Integer_Literal then
- Level := Intval (Expression (Assoc));
+ -- Part_Of must denote a parent state. Ensure that the
+ -- tree is not malformed by checking the expression of
+ -- the component association.
+
+ Par_State := Expression (Assoc);
+ pragma Assert (Present (Par_State));
+
+ Analyze (Par_State);
+
+ -- Part_Of specified a legal state
+
+ if Is_Entity_Name (Par_State)
+ and then Present (Entity (Par_State))
+ and then Ekind (Entity (Par_State)) = E_Abstract_State
+ then
+ null;
else
Error_Msg_N
- ("integrity level must be an integer literal",
- Expression (Assoc));
+ ("option Part_Of must denote an abstract state",
+ Par_State);
end if;
Next (Assoc);
Set_Parent (Id, State);
Set_Ekind (Id, E_Abstract_State);
Set_Etype (Id, Standard_Void_Type);
- Set_Integrity_Level (Id, Level);
Set_Refined_State (Id, Empty);
-- Every non-null state must be nameable and resolvable the
Name_In_Out : constant Name_Id := N + $;
Name_Increases : constant Name_Id := N + $;
Name_Info : constant Name_Id := N + $;
- Name_Integrity : constant Name_Id := N + $;
+ Name_Input_Only : constant Name_Id := N + $;
Name_Internal : constant Name_Id := N + $;
Name_Link_Name : constant Name_Id := N + $;
Name_Lowercase : constant Name_Id := N + $;
Name_No_Unroll : constant Name_Id := N + $;
Name_No_Vector : constant Name_Id := N + $;
Name_Nominal : constant Name_Id := N + $;
+ Name_Non_Volatile : constant Name_Id := N + $;
Name_On : constant Name_Id := N + $;
Name_Optional : constant Name_Id := N + $;
+ Name_Output_Only : constant Name_Id := N + $;
Name_Policy : constant Name_Id := N + $;
Name_Parameter_Types : constant Name_Id := N + $;
+ Name_Part_Of : constant Name_Id := N + $;
Name_Reason : constant Name_Id := N + $;
Name_Reference : constant Name_Id := N + $;
Name_Requires : constant Name_Id := N + $;
projects / thirdparty / gcc.git / commitdiff
