Aspect_Refined_Post, -- GNAT
Aspect_Refined_State, -- GNAT
Aspect_Relative_Deadline,
+ Aspect_Relaxed_Initialization, -- GNAT
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Secondary_Stack_Size, -- GNAT
Aspect_Simple_Storage_Pool, -- GNAT
Aspect_Persistent_BSS => True,
Aspect_Predicate => True,
Aspect_Pure_Function => True,
+ Aspect_Relaxed_Initialization => True,
Aspect_Remote_Access_Type => True,
Aspect_Scalar_Storage_Order => True,
Aspect_Secondary_Stack_Size => True,
Aspect_Refined_Post => Expression,
Aspect_Refined_State => Expression,
Aspect_Relative_Deadline => Expression,
+ Aspect_Relaxed_Initialization => Optional_Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Secondary_Stack_Size => Expression,
Aspect_Simple_Storage_Pool => Name,
Aspect_Refined_Post => False,
Aspect_Refined_State => False,
Aspect_Relative_Deadline => False,
+ Aspect_Relaxed_Initialization => False,
Aspect_Scalar_Storage_Order => True,
Aspect_Secondary_Stack_Size => True,
Aspect_Simple_Storage_Pool => True,
Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_State => Name_Refined_State,
Aspect_Relative_Deadline => Name_Relative_Deadline,
+ Aspect_Relaxed_Initialization => Name_Relaxed_Initialization,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
Aspect_Remote_Call_Interface => Name_Remote_Call_Interface,
Aspect_Remote_Types => Name_Remote_Types,
Aspect_Refined_Global => Never_Delay,
Aspect_Refined_Post => Never_Delay,
Aspect_Refined_State => Never_Delay,
+ Aspect_Relaxed_Initialization => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
and then Is_Protected_Type (Corresponding_Concurrent_Type (Id));
end Is_Protected_Record_Type;
+ -------------------------------------
+ -- Is_Relaxed_Initialization_State --
+ -------------------------------------
+
+ function Is_Relaxed_Initialization_State (Id : E) return B is
+ begin
+ -- To qualify, the abstract state must appear with simple option
+ -- "Relaxed_Initialization" (??? add reference to SPARK RM once the
+ -- Relaxed_Initialization aspect is described there).
+
+ return
+ Ekind (Id) = E_Abstract_State
+ and then Has_Option (Id, Name_Relaxed_Initialization);
+ end Is_Relaxed_Initialization_State;
+
--------------------------------
-- Is_Standard_Character_Type --
--------------------------------
-- Applies to all entities, true for record types and subtypes,
-- includes class-wide types and subtypes (which are also records).
+-- Is_Relaxed_Initialization_State (synthesized)
+-- Applies to all entities, true for abstract states that are subject to
+-- option Relaxed_Initialization.
+
-- Is_Remote_Call_Interface (Flag62)
-- Defined in all entities. Set in E_Package and E_Generic_Package
-- entities to which a pragma Remote_Call_Interface is applied, and
-- Has_Null_Visible_Refinement (synth)
-- Is_External_State (synth)
-- Is_Null_State (synth)
+ -- Is_Relaxed_Initialization_State (synth)
-- Is_Synchronized_State (synth)
-- Partial_Refinement_Constituents (synth)
function Is_Protected_Component (Id : E) return B;
function Is_Protected_Interface (Id : E) return B;
function Is_Protected_Record_Type (Id : E) return B;
+ function Is_Relaxed_Initialization_State (Id : E) return B;
function Is_Standard_Character_Type (Id : E) return B;
function Is_Standard_String_Type (Id : E) return B;
function Is_String_Type (Id : E) return B;
when Attribute_Img =>
Exp_Imgv.Expand_Image_Attribute (N);
+ -----------------
+ -- Initialized --
+ -----------------
+
+ -- For execution, we could either implement an approximation of this
+ -- aspect, or use Valid_Scalars as a first approximation. For now we do
+ -- the latter.
+
+ when Attribute_Initialized =>
+ Rewrite
+ (N,
+ Make_Attribute_Reference
+ (Sloc => Loc,
+ Prefix => Pref,
+ Attribute_Name => Name_Valid_Scalars,
+ Expressions => Exprs));
+
+ Analyze_And_Resolve (N);
+
-----------
-- Input --
-----------
then
null;
+ -- Attribute 'Result is allowed to appear in aspect
+ -- Relaxed_Initialization (??? add reference to SPARK RM once this
+ -- attribute is described there).
+
+ elsif Prag_Nam = Name_Relaxed_Initialization
+ and then Aname = Name_Result
+ then
+ null;
+
elsif Nam_In (Prag_Nam, Name_Post,
Name_Post_Class,
Name_Postcondition,
when Attribute_Img =>
Analyze_Image_Attribute (Standard_String);
+ -----------------
+ -- Initialized --
+ -----------------
+
+ when Attribute_Initialized =>
+ Check_E0;
+
+ if Comes_From_Source (N) then
+
+ -- A similar attribute Valid_Scalars can be prefixed with
+ -- references to both functions and objects, but this attribute
+ -- can be only prefixed with references to objects.
+
+ if not Is_Object_Reference (P) then
+ Error_Attr_P ("prefix of % attribute must be object");
+ end if;
+ end if;
+
+ Set_Etype (N, Standard_Boolean);
+
-----------
-- Input --
-----------
| Attribute_First_Bit
| Attribute_Img
| Attribute_Input
+ | Attribute_Initialized
| Attribute_Last_Bit
| Attribute_Library_Level
| Attribute_Maximum_Alignment
procedure Analyze_Aspect_Implicit_Dereference;
-- Perform analysis of the Implicit_Dereference aspects
+ procedure Analyze_Aspect_Relaxed_Initialization;
+ -- Perform analysis of aspect Relaxed_Initialization
+
procedure Make_Aitem_Pragma
(Pragma_Argument_Associations : List_Id;
Pragma_Name : Name_Id);
end Analyze_Aspect_Implicit_Dereference;
+ -------------------------------------------
+ -- Analyze_Aspect_Relaxed_Initialization --
+ -------------------------------------------
+
+ procedure Analyze_Aspect_Relaxed_Initialization is
+ procedure Analyze_Relaxed_Parameter
+ (Subp_Id : Entity_Id;
+ Param : Node_Id;
+ Seen : in out Elist_Id);
+ -- Analyze parameter that appears in the expression of the
+ -- aspect Relaxed_Initialization.
+
+ -------------------------------
+ -- Analyze_Relaxed_Parameter --
+ -------------------------------
+
+ procedure Analyze_Relaxed_Parameter
+ (Subp_Id : Entity_Id;
+ Param : Node_Id;
+ Seen : in out Elist_Id)
+ is
+ begin
+ -- The relaxed parameter is a formal parameter
+
+ if Nkind_In (Param, N_Identifier, N_Expanded_Name) then
+ Analyze (Param);
+
+ declare
+ Item : constant Entity_Id := Entity (Param);
+ begin
+ -- It must be a formal of the analyzed subprogram
+
+ if Scope (Item) = Subp_Id then
+
+ pragma Assert (Is_Formal (Item));
+
+ -- Detect duplicated items
+
+ if Contains (Seen, Item) then
+ Error_Msg_N ("duplicate aspect % item", Param);
+ else
+ Append_New_Elmt (Item, Seen);
+ end if;
+ else
+ Error_Msg_N ("illegal aspect % item", Param);
+ end if;
+ end;
+
+ -- The relaxed parameter is the function's Result attribute
+
+ elsif Is_Attribute_Result (Param) then
+ Analyze (Param);
+
+ declare
+ Pref : constant Node_Id := Prefix (Param);
+ begin
+ if Present (Pref)
+ and then
+ Nkind_In (Pref, N_Identifier, N_Expanded_Name)
+ and then
+ Entity (Pref) = Subp_Id
+ then
+ -- Detect duplicated items
+
+ if Contains (Seen, Subp_Id) then
+ Error_Msg_N ("duplicate aspect % item", Param);
+ else
+ Append_New_Elmt (Entity (Pref), Seen);
+ end if;
+
+ else
+ Error_Msg_N ("illegal aspect % item", Param);
+ end if;
+ end;
+ else
+ Error_Msg_N ("illegal aspect % item", Param);
+ end if;
+ end Analyze_Relaxed_Parameter;
+
+ -- Local variables
+
+ Seen : Elist_Id := No_Elist;
+ -- Items that appear in the relaxed initialization aspect
+ -- expression of a subprogram; for detecting duplicates.
+
+ -- Start of processing for Analyze_Aspect_Relaxed_Initialization
+
+ begin
+ -- Set name of the aspect for error messages
+ Error_Msg_Name_1 := Nam;
+
+ -- Annotation of a type; no aspect expression is allowed
+ -- ??? Once the exact rule for this aspect is ready, we will
+ -- likely reject concurrent types, etc., so let's keep the code
+ -- for types and variable separate.
+
+ if Is_First_Subtype (E) then
+ if Present (Expr) then
+ Error_Msg_N ("illegal aspect % expression", Expr);
+ end if;
+
+ -- Annotation of a variable; no aspect expression is allowed
+
+ elsif Ekind (E) = E_Variable then
+ if Present (Expr) then
+ Error_Msg_N ("illegal aspect % expression", Expr);
+ end if;
+
+ -- Annotation of a subprogram; aspect expression is required
+
+ elsif Is_Subprogram (E) then
+ if Present (Expr) then
+
+ -- Subprogram and its formal parameters must be visible
+ -- when analyzing the aspect expression.
+
+ pragma Assert (not In_Open_Scopes (E));
+
+ Push_Scope (E);
+
+ if Is_Generic_Subprogram (E) then
+ Install_Generic_Formals (E);
+ else
+ Install_Formals (E);
+ end if;
+
+ -- Aspect expression is either an aggregate with list of
+ -- parameters (and possibly the Result attribute for a
+ -- function).
+
+ if Nkind (Expr) = N_Aggregate then
+
+ -- Component associations are not allowed in the
+ -- aspect expression aggregate.
+
+ if Present (Component_Associations (Expr)) then
+ Error_Msg_N ("illegal aspect % expression", Expr);
+ else
+ declare
+ Param : Node_Id := First (Expressions (Expr));
+
+ begin
+ while Present (Param) loop
+ Analyze_Relaxed_Parameter (E, Param, Seen);
+ Next (Param);
+ end loop;
+ end;
+ end if;
+
+ -- Mark the aggregate expression itself as analyzed;
+ -- its subexpressions were marked when they themselves
+ -- were analyzed.
+
+ Set_Analyzed (Expr);
+
+ -- Otherwise, it is a single name of a subprogram
+ -- parameter (or possibly the Result attribute for
+ -- a function).
+
+ else
+ Analyze_Relaxed_Parameter (E, Expr, Seen);
+ end if;
+
+ End_Scope;
+ else
+ Error_Msg_N ("missing expression for aspect %", N);
+ end if;
+
+ else
+ Error_Msg_N ("inappropriate entity for aspect %", E);
+ end if;
+ end Analyze_Aspect_Relaxed_Initialization;
+
-----------------------
-- Make_Aitem_Pragma --
-----------------------
end;
end if;
+ -- Relaxed_Initialization
+
+ when Aspect_Relaxed_Initialization =>
+ Analyze_Aspect_Relaxed_Initialization;
+ goto Continue;
+
-- Secondary_Stack_Size
-- Aspect Secondary_Stack_Size needs to be converted into a
| Aspect_Refined_Global
| Aspect_Refined_Post
| Aspect_Refined_State
+ | Aspect_Relaxed_Initialization
| Aspect_SPARK_Mode
| Aspect_Test_Case
| Aspect_Unimplemented
if Present (L) then
Context := Parent (L);
- -- Certain contract annocations have forward visibility semantics and
+ -- Certain contract annotations have forward visibility semantics and
-- must be analyzed after all declarative items have been processed.
-- This timing ensures that entities referenced by such contracts are
-- visible.
-- SIMPLE_OPTION
-- | NAME_VALUE_OPTION
- -- SIMPLE_OPTION ::= Ghost | Synchronous
+ -- SIMPLE_OPTION ::= Ghost | Relaxed_Initialization | Synchronous
-- NAME_VALUE_OPTION ::=
-- Part_Of => ABSTRACT_STATE
is
-- Flags used to verify the consistency of options
- AR_Seen : Boolean := False;
- AW_Seen : Boolean := False;
- ER_Seen : Boolean := False;
- EW_Seen : Boolean := False;
- External_Seen : Boolean := False;
- Ghost_Seen : Boolean := False;
- Others_Seen : Boolean := False;
- Part_Of_Seen : Boolean := False;
- Synchronous_Seen : Boolean := False;
+ AR_Seen : Boolean := False;
+ AW_Seen : Boolean := False;
+ ER_Seen : Boolean := False;
+ EW_Seen : Boolean := False;
+ External_Seen : Boolean := False;
+ Ghost_Seen : Boolean := False;
+ Others_Seen : Boolean := False;
+ Part_Of_Seen : Boolean := False;
+ Relaxed_Initialization_Seen : Boolean := False;
+ Synchronous_Seen : Boolean := False;
-- Flags used to store the static value of all external states'
-- expressions.
Check_Duplicate_Option (Opt, Synchronous_Seen);
Check_Ghost_Synchronous;
+ -- Relaxed_Initialization
+
+ elsif Chars (Opt) = Name_Relaxed_Initialization then
+ Check_Duplicate_Option
+ (Opt, Relaxed_Initialization_Seen);
+
-- Option Part_Of without an encapsulating state is
-- illegal (SPARK RM 7.1.4(8)).
end if;
end Has_Private_Component;
+ --------------------------------
+ -- Has_Relaxed_Initialization --
+ --------------------------------
+
+ function Has_Relaxed_Initialization (E : Entity_Id) return Boolean is
+
+ function Denotes_Relaxed_Parameter
+ (Expr : Node_Id;
+ Param : Entity_Id)
+ return Boolean;
+ -- Returns True iff expression Expr denotes a formal parameter or
+ -- function Param (through its attribute Result).
+
+ -------------------------------
+ -- Denotes_Relaxed_Parameter --
+ -------------------------------
+
+ function Denotes_Relaxed_Parameter
+ (Expr : Node_Id;
+ Param : Entity_Id)
+ return Boolean
+ is
+ begin
+ if Nkind_In (Expr, N_Identifier, N_Expanded_Name) then
+ return Entity (Expr) = Param;
+ else
+ pragma Assert (Is_Attribute_Result (Expr));
+ return Entity (Prefix (Expr)) = Param;
+ end if;
+ end Denotes_Relaxed_Parameter;
+
+ -- Start of processing for Has_Relaxed_Initialization
+
+ begin
+ -- When analyzing, we checked all syntax legality rules for the aspect
+ -- Relaxed_Initialization, but didn't store the property anywhere (e.g.
+ -- as an Einfo flag). To query the property we look directly at the AST,
+ -- but now without any syntactic checks.
+
+ case Ekind (E) is
+ -- Abstract states have option Relaxed_Initialization
+
+ when E_Abstract_State =>
+ return Is_Relaxed_Initialization_State (E);
+
+ -- Variables have this aspect attached directly
+
+ when E_Variable =>
+ return Has_Aspect (E, Aspect_Relaxed_Initialization);
+
+ -- Types have this aspect attached directly (though we only allow it
+ -- to be specified for the first subtype).
+
+ when Type_Kind =>
+ pragma Assert (Is_First_Subtype (E));
+ return Has_Aspect (E, Aspect_Relaxed_Initialization);
+
+ -- Formal parameters and functions have the Relaxed_Initialization
+ -- aspect attached to the subprogram entity and must be listed in
+ -- the aspect expression.
+
+ when Formal_Kind
+ | E_Function
+ =>
+ declare
+ Subp_Id : Entity_Id;
+ Aspect_Expr : Node_Id;
+ Param_Expr : Node_Id;
+
+ begin
+ if Is_Formal (E) then
+ Subp_Id := Scope (E);
+ else
+ Subp_Id := E;
+ end if;
+
+ if Has_Aspect (Subp_Id, Aspect_Relaxed_Initialization) then
+ Aspect_Expr :=
+ Find_Value_Of_Aspect (E, Aspect_Relaxed_Initialization);
+
+ -- Aspect expression is either an aggregate, e.g.:
+ --
+ -- function F (X : Integer) return Integer
+ -- with Relaxed_Initialization => (X, F'Result);
+
+ if Nkind (Aspect_Expr) = N_Aggregate then
+
+ Param_Expr := First (Expressions (Aspect_Expr));
+
+ while Present (Param_Expr) loop
+ if Denotes_Relaxed_Parameter (Param_Expr, E) then
+ return True;
+ end if;
+
+ Next (Param_Expr);
+ end loop;
+
+ return False;
+
+ -- or it is a single identifier, e.g.:
+ --
+ -- function F (X : Integer) return Integer
+ -- with Relaxed_Initialization => X;
+
+ else
+ return Denotes_Relaxed_Parameter (Aspect_Expr, E);
+ end if;
+ else
+ return False;
+ end if;
+ end;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Has_Relaxed_Initialization;
+
----------------------
-- Has_Signed_Zeros --
----------------------
-- Check if a type has a (sub)component of a private type that has not
-- yet received a full declaration.
+ function Has_Relaxed_Initialization (E : Entity_Id) return Boolean;
+ -- Returns True iff entity E, which can be either a type, a variable, an
+ -- abstract state or a function, is subject to the Relaxed_Initialization
+ -- aspect.
+
function Has_Signed_Zeros (E : Entity_Id) return Boolean;
-- Determines if the floating-point type E supports signed zeros.
-- Returns False if E is not a floating-point type.
Name_Dimension_System : constant Name_Id := N + $;
Name_Disable_Controlled : constant Name_Id := N + $;
Name_Dynamic_Predicate : constant Name_Id := N + $;
+ Name_Relaxed_Initialization : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
Name_Synchronization : constant Name_Id := N + $;
Name_Unimplemented : constant Name_Id := N + $;
Name_Has_Tagged_Values : constant Name_Id := N + $; -- GNAT
Name_Identity : constant Name_Id := N + $;
Name_Implicit_Dereference : constant Name_Id := N + $; -- GNAT
+ Name_Initialized : constant Name_Id := N + $; -- GNAT
Name_Integer_Value : constant Name_Id := N + $; -- GNAT
Name_Invalid_Value : constant Name_Id := N + $; -- GNAT
Name_Iterator_Element : constant Name_Id := N + $; -- GNAT
Attribute_Has_Tagged_Values,
Attribute_Identity,
Attribute_Implicit_Dereference,
+ Attribute_Initialized,
Attribute_Integer_Value,
Attribute_Invalid_Value,
Attribute_Iterator_Element,
projects / gcc.git / commitdiff