+2013-04-12 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Alphabetize subprogram bodies in this unit. Add
+ an entry for Aspect_Ghost in the table of canonical aspects.
+ (Has_Aspect): New routine.
+ * aspects.ads: Add Aspect_Ghost to all relevant
+ tables. Alphabetize subprograms in this unit.
+ (Has_Aspect): New routine.
+ * einfo.adb: Add with and use clauses for Aspects.
+ (Is_Ghost_Function): New routine.
+ * einfo.ads: Add new synthesized attribute Is_Ghost_Function and
+ update the structure of the related nodes.
+ (Is_Ghost_Function): New routine.
+ * exp_ch4.adb (Find_Enclosing_Context): Use routine
+ Is_Body_Or_Package_Declaration to terminate a search.
+ (Is_Body_Or_Unit): Removed.
+ * exp_util.adb (Within_Case_Or_If_Expression): Use routine
+ Is_Body_Or_Package_Declaration to terminate a search.
+ * par-prag.adb: Add pragma Ghost to the list of pragmas that do
+ not need special processing by the parser.
+ * sem_attr.adb (Analyze_Access_Attribute): Detect an
+ illegal use of 'Access where the prefix is a ghost function.
+ (Analyze_Attribute): Use routine Is_Body_Or_Package_Declaration
+ to terminate a search. (Check_References_In_Prefix): Use routine
+ Is_Body_Or_Package_Declaration to terminate a search.
+ * sem_ch4.adb (Analyze_Call): Mark a function when it appears
+ inside an assertion expression. Verify the legality of a call
+ to a ghost function.
+ (Check_Ghost_Function_Call): New routine.
+ * sem_ch6.adb (Analyze_Function_Call): Code reformatting. Move
+ the setting of attribute In_Assertion_Expression to Analyze_Call.
+ (Check_Overriding_Indicator): Detect an illegal attempt to
+ override a function with a ghost function.
+ * sem_ch12.adb (Preanalyze_Actuals): Detect an illegal use of
+ a ghost function as a generic actual.
+ * sem_elab.adb (Check_Internal_Call_Continue): Update the call
+ to In_Assertion.
+ * sem_prag.adb: Add an entry for pragma Ghost in the table
+ of significant arguments.
+ (Analyze_Pragma): Do not analyze
+ an "others" case guard. Add processing for pragma Ghost. Use
+ Preanalyze_Assert_Expression when analyzing the expression of
+ pragmas Loop_Invariant and Loop_Variant.
+ * sem_util.adb (Get_Subprogram_Entity): Reimplemented.
+ (Is_Body_Or_Package_Declaration): New routine.
+ * sem_util.ads: Alphabetize subprotrams in this unit.
+ (Is_Body_Or_Package_Declaration): New routine.
+ * sinfo.adb (In_Assertion): Rename to In_Assertion_Expression.
+ (Set_In_Assertion): Rename to Set_In_Assertion_Expression.
+ * sinfo.ads: Rename flag In_Assertion to In_Assertion_Expression
+ to better reflect its use. Update all places that mention the flag.
+ (In_Assertion): Rename to In_Assertion_Expression. Update
+ related pragma Inline. (Set_In_Assertion): Rename to
+ Set_In_Assertion_Expression. Update related pragma Inline.
+ * snames.ads-tmpl: Add new predefined name Ghost. Add new pragma
+ id Pragma_Ghost.
+
2013-04-12 Arnaud Charlet <charlet@adacore.com>
* sem_prag.adb (Set_Imported): Do not generate error for multiple
end if;
end Aspect_Specifications;
- -------------------
- -- Get_Aspect_Id --
- -------------------
-
- function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
- begin
- return Aspect_Id_Hash_Table.Get (Name);
- end Get_Aspect_Id;
-
-----------------
-- Find_Aspect --
-----------------
return Empty;
end Find_Aspect;
+ -------------------
+ -- Get_Aspect_Id --
+ -------------------
+
+ function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
+ begin
+ return Aspect_Id_Hash_Table.Get (Name);
+ end Get_Aspect_Id;
+
+ ----------------
+ -- Has_Aspect --
+ ----------------
+
+ function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean is
+ Decl : constant Node_Id := Parent (Parent (Id));
+ Aspect : Node_Id;
+
+ begin
+ if Has_Aspects (Decl) then
+ Aspect := First (Aspect_Specifications (Decl));
+ while Present (Aspect) loop
+ if Get_Aspect_Id (Chars (Identifier (Aspect))) = A then
+ return True;
+ end if;
+
+ Next (Aspect);
+ end loop;
+ end if;
+
+ return False;
+ end Has_Aspect;
+
------------------
-- Move_Aspects --
------------------
Aspect_External_Name => Aspect_External_Name,
Aspect_External_Tag => Aspect_External_Tag,
Aspect_Favor_Top_Level => Aspect_Favor_Top_Level,
+ Aspect_Ghost => Aspect_Ghost,
Aspect_Global => Aspect_Global,
Aspect_Implicit_Dereference => Aspect_Implicit_Dereference,
Aspect_Import => Aspect_Import,
Aspect_Discard_Names,
Aspect_Export,
Aspect_Favor_Top_Level, -- GNAT
+ Aspect_Ghost, -- GNAT
Aspect_Independent,
Aspect_Independent_Components,
Aspect_Import,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
+ Aspect_Ghost => True,
Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Invariant => True,
Aspect_External_Tag => Name_External_Tag,
Aspect_Export => Name_Export,
Aspect_Favor_Top_Level => Name_Favor_Top_Level,
+ Aspect_Ghost => Name_Ghost,
Aspect_Global => Name_Global,
Aspect_Implicit_Dereference => Name_Implicit_Dereference,
Aspect_Import => Name_Import,
-- implemented internally with a hash table in the body, that provides
-- access to aspect specifications.
- function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
- -- Returns True if the node N is a declaration node that permits aspect
- -- specifications in the grammar. It is possible for other nodes to have
- -- aspect specifications as a result of Rewrite or Replace calls.
-
function Aspect_Specifications (N : Node_Id) return List_Id;
-- Given a node N, returns the list of N_Aspect_Specification nodes that
-- are attached to this declaration node. If the node is in the class of
-- Replace calls, and this function may be used to retrieve the aspect
-- specifications for the original rewritten node in such cases.
- procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
- -- The node N must be in the class of declaration nodes that permit aspect
- -- specifications and the Has_Aspects flag must be False on entry. L must
- -- be a non-empty list of N_Aspect_Specification nodes. This procedure sets
- -- the Has_Aspects flag to True, and makes an entry that can be retrieved
- -- by a subsequent Aspect_Specifications call. It is an error to call this
- -- procedure with a node that does not permit aspect specifications, or a
- -- node that has its Has_Aspects flag set True on entry, or with L being an
- -- empty list or No_List.
-
function Find_Aspect (Ent : Entity_Id; A : Aspect_Id) return Node_Id;
-- Find value of a given aspect from aspect list of entity
+ function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean;
+ -- Determine whether entity Id has aspect A
+
procedure Move_Aspects (From : Node_Id; To : Node_Id);
-- Moves aspects from 'From' node to 'To' node. Has_Aspects (To) must be
-- False on entry. If Has_Aspects (From) is False, the call has no effect.
-- Otherwise the aspects are moved and on return Has_Aspects (To) is True,
-- and Has_Aspects (From) is False.
+ function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
+ -- Returns True if the node N is a declaration node that permits aspect
+ -- specifications in the grammar. It is possible for other nodes to have
+ -- aspect specifications as a result of Rewrite or Replace calls.
+
function Same_Aspect (A1 : Aspect_Id; A2 : Aspect_Id) return Boolean;
-- Returns True if A1 and A2 are (essentially) the same aspect. This is not
-- a simple equality test because e.g. Post and Postcondition are the same.
-- This is used for detecting duplicate aspects.
- procedure Tree_Write;
- -- Writes contents of Aspect_Specifications hash table to the tree file
+ procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
+ -- The node N must be in the class of declaration nodes that permit aspect
+ -- specifications and the Has_Aspects flag must be False on entry. L must
+ -- be a non-empty list of N_Aspect_Specification nodes. This procedure sets
+ -- the Has_Aspects flag to True, and makes an entry that can be retrieved
+ -- by a subsequent Aspect_Specifications call. It is an error to call this
+ -- procedure with a node that does not permit aspect specifications, or a
+ -- node that has its Has_Aspects flag set True on entry, or with L being an
+ -- empty list or No_List.
procedure Tree_Read;
-- Reads contents of Aspect_Specifications hash table from the tree file
+ procedure Tree_Write;
+ -- Writes contents of Aspect_Specifications hash table to the tree file
+
end Aspects;
pragma Style_Checks (All_Checks);
-- Turn off subprogram ordering, not used for this unit
-with Atree; use Atree;
-with Namet; use Namet;
-with Nlists; use Nlists;
-with Output; use Output;
-with Sinfo; use Sinfo;
-with Stand; use Stand;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Output; use Output;
+with Sinfo; use Sinfo;
+with Stand; use Stand;
package body Einfo is
function Is_Finalizer (Id : E) return B is
begin
- return Ekind (Id) = E_Procedure
- and then Chars (Id) = Name_uFinalizer;
+ return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer;
end Is_Finalizer;
+ -----------------------
+ -- Is_Ghost_Function --
+ -----------------------
+
+ function Is_Ghost_Function (Id : E) return B is
+ Subp_Id : Entity_Id := Id;
+
+ begin
+ if Present (Subp_Id) and then Ekind (Subp_Id) = E_Function then
+
+ -- Handle renamings of functions
+
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Alias (Subp_Id);
+ end if;
+
+ return Has_Aspect (Subp_Id, Aspect_Ghost);
+ end if;
+
+ return False;
+ end Is_Ghost_Function;
+
--------------------
-- Is_Input_State --
--------------------
function Is_Null_State (Id : E) return B is
begin
return
- Ekind (Id) = E_Abstract_State
- and then Nkind (Parent (Id)) = N_Null;
+ Ekind (Id) = E_Abstract_State and then Nkind (Parent (Id)) = N_Null;
end Is_Null_State;
---------------------
function Is_Package_Or_Generic_Package (Id : E) return B is
begin
- return
- Ekind (Id) = E_Package
- or else
- Ekind (Id) = E_Generic_Package;
+ return Ekind_In (Id, E_Generic_Package, E_Package);
end Is_Package_Or_Generic_Package;
---------------
function Is_Protected_Component (Id : E) return B is
begin
- return Ekind (Id) = E_Component
- and then Is_Protected_Type (Scope (Id));
+ return Ekind (Id) = E_Component and then Is_Protected_Type (Scope (Id));
end Is_Protected_Component;
----------------------------
-- the same structure for constrained and unconstrained arrays, subtype
-- marks and discrete ranges are both represented by a subtype. This
-- function returns the tree node corresponding to an occurrence of the
--- first index (NOT the entity for the type). Subsequent indexes are
+-- first index (NOT the entity for the type). Subsequent indices are
-- obtained using Next_Index. Note that this field is defined for the
-- case of string literal subtypes, but is always Empty.
-- package, generic function, generic procedure), and False for all
-- other entities.
+-- Is_Ghost_Function (synthesized)
+-- Applies to all entities. Yields True for a function marked by aspect
+-- Ghost.
+
-- Is_Hidden (Flag57)
-- Defined in all entities. Set true for all entities declared in the
-- private part or body of a package. Also marks generic formals of a
-- Address_Clause (synth)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
+ -- Is_Ghost_Function (synth) (non-generic case only)
-- Last_Formal (synth)
-- Number_Formals (synth)
-- Scope_Depth (synth)
function Is_Discriminal (Id : E) return B;
function Is_Dynamic_Scope (Id : E) return B;
function Is_Finalizer (Id : E) return B;
+ function Is_Ghost_Function (Id : E) return B;
function Is_Input_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Output_State (Id : E) return B;
----------------------------
function Find_Enclosing_Context return Node_Id is
- function Is_Body_Or_Unit (N : Node_Id) return Boolean;
- -- Determine whether N denotes a body or unit declaration
-
- ---------------------
- -- Is_Body_Or_Unit --
- ---------------------
-
- function Is_Body_Or_Unit (N : Node_Id) return Boolean is
- begin
- return Nkind_In (N, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body);
- end Is_Body_Or_Unit;
-
- -- Local variables
-
Par : Node_Id;
Top : Node_Id;
- -- Start of processing for Find_Enclosing_Context
-
begin
-- The expression_with_actions is in a case/if expression and
-- the lifetime of any temporary controlled object is therefore
-- Prevent the search from going too far
- elsif Is_Body_Or_Unit (Par) then
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
-- Prevent the search from going too far
- elsif Is_Body_Or_Unit (Par) then
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
then
return Par;
- elsif Is_Body_Or_Unit (Par) then
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
exit;
end if;
-- Prevent the search from going too far
- elsif Nkind_In (Par, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Par) then
return False;
end if;
Pragma_Fast_Math |
Pragma_Finalize_Storage_Only |
Pragma_Float_Representation |
+ Pragma_Ghost |
Pragma_Global |
Pragma_Ident |
Pragma_Implementation_Defined |
if Has_Pragma_Inline_Always (Entity (P)) then
Error_Attr_P
("prefix of % attribute cannot be Inline_Always subprogram");
- end if;
- if Aname = Name_Unchecked_Access then
+ elsif Aname = Name_Unchecked_Access then
Error_Attr ("attribute% cannot be applied to a subprogram", P);
+
+ elsif Is_Ghost_Function (Entity (P)) then
+ Error_Attr_P
+ ("prefix of % attribute cannot be a ghost function");
end if;
-- Issue an error if the prefix denotes an eliminated subprogram
-- Prevent the search from going too far
- elsif Nkind_In (Stmt, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
-- Prevent the search from going too far
- elsif Nkind_In (Stmt, N_Entry_Body,
- N_Package_Body,
- N_Package_Declaration,
- N_Protected_Body,
- N_Subprogram_Body,
- N_Task_Body)
- then
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
exit;
end if;
and then
(Ekind (Btyp) = E_Access_Subprogram_Type
or else Is_Local_Anonymous_Access (Btyp))
-
and then Subprogram_Access_Level (Entity (P)) >
Type_Access_Level (Btyp)
then
-- in such a context.
if Attr_Id /= Attribute_Unchecked_Access
+ and then Ekind (Btyp) = E_General_Access_Type
and then
Object_Access_Level (P) > Deepest_Type_Access_Level (Btyp)
- and then Ekind (Btyp) = E_General_Access_Type
then
Accessibility_Message;
return;
Analyze (Act);
end if;
- if Errs /= Serious_Errors_Detected then
+ -- Ensure that a ghost function does not act as generic actual
+
+ if Is_Entity_Name (Act)
+ and then Is_Ghost_Function (Entity (Act))
+ then
+ Error_Msg_N
+ ("ghost function & cannot act as generic actual", Act);
+ Abandon_Instantiation (Act);
+
+ elsif Errs /= Serious_Errors_Detected then
-- Do a minimal analysis of the generic, to prevent spurious
-- warnings complaining about the generic being unreferenced,
-- Flag indicates whether an interpretation of the prefix is a
-- parameterless call that returns an access_to_subprogram.
+ procedure Check_Ghost_Function_Call;
+ -- Verify the legality of a call to a ghost function. Such calls can
+ -- appear only in assertion expressions except subtype predicates or
+ -- from within another ghost function.
+
procedure Check_Mixed_Parameter_And_Named_Associations;
-- Check that parameter and named associations are not mixed. This is
-- a restriction in SPARK mode.
procedure No_Interpretation;
-- Output error message when no valid interpretation exists
+ -------------------------------
+ -- Check_Ghost_Function_Call --
+ -------------------------------
+
+ procedure Check_Ghost_Function_Call is
+ S : Entity_Id;
+
+ begin
+ -- The ghost function appears inside an assertion expression
+
+ if In_Assertion_Expression (N) then
+ return;
+
+ else
+ S := Current_Scope;
+ while Present (S) and then S /= Standard_Standard loop
+
+ -- The call appears inside another ghost function
+
+ if Is_Ghost_Function (S) then
+ return;
+ end if;
+
+ S := Scope (S);
+ end loop;
+ end if;
+
+ Error_Msg_N
+ ("call to ghost function must appear in assertion expression or "
+ & "another ghost function", N);
+ end Check_Ghost_Function_Call;
+
--------------------------------------------------
-- Check_Mixed_Parameter_And_Named_Associations --
--------------------------------------------------
Check_Mixed_Parameter_And_Named_Associations;
end if;
+ -- Mark a function that appears inside an assertion expression
+
+ if Nkind (N) = N_Function_Call and then In_Assertion_Expr > 0 then
+ Set_In_Assertion_Expression (N);
+ end if;
+
-- Initialize the type of the result of the call to the error type,
-- which will be reset if the type is successfully resolved.
Set_Etype (Nam_Ent, Etype (N));
end if;
+ -- Overloaded call
+
else
-- An overloaded selected component must denote overloaded operations
-- of a concurrent type. The interpretations are attached to the
Get_Next_Interp (X, It);
end loop;
- -- If the name is the result of a function call, it can only
- -- be a call to a function returning an access to subprogram.
- -- Insert explicit dereference.
+ -- If the name is the result of a function call, it can only be a
+ -- call to a function returning an access to subprogram. Insert
+ -- explicit dereference.
if Nkind (Nam) = N_Function_Call then
Insert_Explicit_Dereference (Nam);
End_Interp_List;
end if;
+
+ -- A call to a ghost function is allowed only in assertion expressions,
+ -- excluding subtype predicates, or from within another ghost function.
+
+ if Is_Ghost_Function (Get_Subprogram_Entity (N)) then
+ Check_Ghost_Function_Call;
+ end if;
end Analyze_Call;
-----------------------------
----------------------------
procedure Analyze_Function_Call (N : Node_Id) is
- P : constant Node_Id := Name (N);
- Actuals : constant List_Id := Parameter_Associations (N);
- Actual : Node_Id;
+ Actuals : constant List_Id := Parameter_Associations (N);
+ Func_Nam : constant Node_Id := Name (N);
+ Actual : Node_Id;
+
+ -- Start of processing for Analyze_Function_Call
begin
- Analyze (P);
+ Analyze (Func_Nam);
-- A call of the form A.B (X) may be an Ada 2005 call, which is
-- rewritten as B (A, X). If the rewriting is successful, the call
-- has been analyzed and we just return.
- if Nkind (P) = N_Selected_Component
- and then Name (N) /= P
+ if Nkind (Func_Nam) = N_Selected_Component
+ and then Name (N) /= Func_Nam
and then Is_Rewrite_Substitution (N)
and then Present (Etype (N))
then
-- If error analyzing name, then set Any_Type as result type and return
- if Etype (P) = Any_Type then
+ if Etype (Func_Nam) = Any_Type then
Set_Etype (N, Any_Type);
return;
end if;
end if;
Analyze_Call (N);
-
- -- Mark function call if within assertion
-
- if In_Assertion_Expr /= 0 then
- Set_In_Assertion (N);
- end if;
end Analyze_Function_Call;
-----------------------------
-----------------------------
procedure Analyze_Function_Return (N : Node_Id) is
- Loc : constant Source_Ptr := Sloc (N);
- Stm_Entity : constant Entity_Id := Return_Statement_Entity (N);
- Scope_Id : constant Entity_Id := Return_Applies_To (Stm_Entity);
+ Loc : constant Source_Ptr := Sloc (N);
+ Stm_Entity : constant Entity_Id := Return_Statement_Entity (N);
+ Scope_Id : constant Entity_Id := Return_Applies_To (Stm_Entity);
R_Type : constant Entity_Id := Etype (Scope_Id);
-- Function result subtype
else
Set_Overridden_Operation (Subp, Overridden_Subp);
end if;
+
+ -- Ensure that a ghost function is not overriding another routine
+
+ elsif Is_Ghost_Function (Subp) then
+ Error_Msg_N ("ghost function & cannot be overriding", Subp);
end if;
end if;
-- in this case, due to the out of order handling in this case.
and then (Nkind (Original_Node (N)) /= N_Function_Call
- or else not In_Assertion (Original_Node (N)))
+ or else not In_Assertion_Expression (Original_Node (N)))
then
if Inst_Case then
Error_Msg_NE
-- Pre-analyze the guard and consequence expressions of a Contract_Cases
-- pragma/aspect aggregate expression.
+ ----------------------------
+ -- Analyze_Contract_Cases --
+ ----------------------------
+
procedure Analyze_Contract_Cases (Aggr : Node_Id) is
Case_Guard : Node_Id;
Conseq : Node_Id;
Post_Case : Node_Id;
+
begin
Post_Case := First (Component_Associations (Aggr));
while Present (Post_Case) loop
-- Preanalyze the boolean expression, we treat this as a spec
-- expression (i.e. similar to a default expression).
- Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+ if Nkind (Case_Guard) /= N_Others_Choice then
+ Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+ end if;
+
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
Next (Post_Case);
end loop;
end Analyze_Contract_Cases;
+ -- Start of processing for Analyze_CTC_In_Decl_Part
+
begin
-- Install formals and push subprogram spec onto scope stack so that we
-- can see the formals from the pragma.
- Install_Formals (S);
Push_Scope (S);
+ Install_Formals (S);
-- Preanalyze the boolean expressions, we treat these as spec
-- expressions (i.e. similar to a default expression).
end if;
end Float_Representation;
+ -----------
+ -- Ghost --
+ -----------
+
+ -- pragma GHOST (function_LOCAL_NAME);
+
+ when Pragma_Ghost => Ghost : declare
+ Subp : Node_Id;
+ Subp_Id : Entity_Id;
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+ Check_Arg_Is_Local_Name (Arg1);
+
+ -- Ensure the proper placement of the pragma. Ghost must be
+ -- associated with a subprogram declaration.
+
+ Subp := Parent (Corresponding_Aspect (N));
+
+ if Nkind (Subp) /= N_Subprogram_Declaration then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Id := Defining_Unit_Name (Specification (Subp));
+
+ if Ekind (Subp_Id) /= E_Function then
+ Error_Pragma ("pragma % must be applied to a function");
+ end if;
+ end Ghost;
+
------------
-- Global --
------------
return;
end if;
- Preanalyze_And_Resolve (Expression (Arg1), Any_Boolean);
+ Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
-- Transform pragma Loop_Invariant into equivalent pragma Check
-- Generate:
-- pragma Check (Loop_Invaraint, Arg1);
- -- Seems completely wrong to hijack pragma Check this way ???
-
Rewrite (N,
Make_Pragma (Loc,
Chars => Name_Check,
Error_Pragma_Arg ("wrong change modifier", Variant);
end if;
- Preanalyze_And_Resolve (Expression (Variant), Any_Discrete);
+ Preanalyze_Assert_Expression
+ (Expression (Variant), Any_Discrete);
Next (Variant);
end loop;
Pragma_Fast_Math => -1,
Pragma_Finalize_Storage_Only => 0,
Pragma_Float_Representation => 0,
+ Pragma_Ghost => 0,
Pragma_Global => -1,
Pragma_Ident => -1,
Pragma_Implementation_Defined => -1,
---------------------------
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id is
- Nam : Node_Id;
- Proc : Entity_Id;
+ Subp : Node_Id;
+ Subp_Id : Entity_Id;
begin
if Nkind (Nod) = N_Accept_Statement then
- Nam := Entry_Direct_Name (Nod);
+ Subp := Entry_Direct_Name (Nod);
+
+ elsif Nkind (Nod) = N_Slice then
+ Subp := Prefix (Nod);
+
+ else
+ Subp := Name (Nod);
+ end if;
+
+ -- Strip the subprogram call
+
+ loop
+ if Nkind_In (Subp, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component)
+ then
+ Subp := Prefix (Subp);
- -- For an entry call, the prefix of the call is a selected component.
- -- Need additional code for internal calls ???
+ elsif Nkind_In (Subp, N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ then
+ Subp := Expression (Subp);
- elsif Nkind (Nod) = N_Entry_Call_Statement then
- if Nkind (Name (Nod)) = N_Selected_Component then
- Nam := Entity (Selector_Name (Name (Nod)));
else
- Nam := Empty;
+ exit;
end if;
+ end loop;
- else
- Nam := Name (Nod);
- end if;
+ -- Extract the entity of the subprogram call
- if Nkind (Nam) = N_Explicit_Dereference then
- Proc := Etype (Prefix (Nam));
- elsif Is_Entity_Name (Nam) then
- Proc := Entity (Nam);
- else
- return Empty;
- end if;
+ if Is_Entity_Name (Subp) then
+ Subp_Id := Entity (Subp);
- if Is_Object (Proc) then
- Proc := Etype (Proc);
- end if;
+ if Ekind (Subp_Id) = E_Access_Subprogram_Type then
+ Subp_Id := Directly_Designated_Type (Subp_Id);
+ end if;
- if Ekind (Proc) = E_Access_Subprogram_Type then
- Proc := Directly_Designated_Type (Proc);
- end if;
+ if Is_Subprogram (Subp_Id) then
+ return Subp_Id;
+ else
+ return Empty;
+ end if;
+
+ -- The search did not find a construct that denotes a subprogram
- if not Is_Subprogram (Proc)
- and then Ekind (Proc) /= E_Subprogram_Type
- then
- return Empty;
else
- return Proc;
+ return Empty;
end if;
end Get_Subprogram_Entity;
end if;
end Is_Atomic_Object;
+ ------------------------------------
+ -- Is_Body_Or_Package_Declaration --
+ ------------------------------------
+
+ function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean is
+ begin
+ return Nkind_In (N, N_Entry_Body,
+ N_Package_Body,
+ N_Package_Declaration,
+ N_Protected_Body,
+ N_Subprogram_Body,
+ N_Task_Body);
+ end Is_Body_Or_Package_Declaration;
+
-----------------------
-- Is_Bounded_String --
-----------------------
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
+ procedure Check_Dynamically_Tagged_Expression
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Related_Nod : Node_Id);
+ -- Check wrong use of dynamically tagged expression
+
+ procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
+ -- Verify that the full declaration of type T has been seen. If not, place
+ -- error message on node N. Used in object declarations, type conversions
+ -- and qualified expressions.
+
procedure Check_Function_Writable_Actuals (N : Node_Id);
-- (Ada 2012): If the construct N has two or more direct constituents that
-- are names or expressions whose evaluation may occur in an arbitrary
-- remains in the Examiner (JB01-005). Note that the Examiner does not
-- count package declarations in later declarative items.
- procedure Check_Dynamically_Tagged_Expression
- (Expr : Node_Id;
- Typ : Entity_Id;
- Related_Nod : Node_Id);
- -- Check wrong use of dynamically tagged expression
-
- procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
- -- Verify that the full declaration of type T has been seen. If not, place
- -- error message on node N. Used in object declarations, type conversions
- -- and qualified expressions.
-
procedure Check_Nested_Access (Ent : Entity_Id);
-- Check whether Ent denotes an entity declared in an uplevel scope, which
-- is accessed inside a nested procedure, and set Has_Up_Level_Access flag
-- discriminant at the same position in this new type.
procedure Find_Overlaid_Entity
- (N : Node_Id;
+ (N : Node_Id;
Ent : out Entity_Id;
Off : out Boolean);
-- The node N should be an address representation clause. Determines if
-- Determines if the given node denotes an atomic object in the sense of
-- the legality checks described in RM C.6(12).
+ function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether node N denotes a body or a package declaration
+
function Is_Bounded_String (T : Entity_Id) return Boolean;
-- True if T is a bounded string type. Used to make sure "=" composes
-- properly for bounded string types.
-- S2. Otherwise, it is S itself.
function Object_Access_Level (Obj : Node_Id) return Uint;
- -- Return the accessibility level of the view of the object Obj.
- -- For convenience, qualified expressions applied to object names
- -- are also allowed as actuals for this function.
+ -- Return the accessibility level of the view of the object Obj. For
+ -- convenience, qualified expressions applied to object names are also
+ -- allowed as actuals for this function.
function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean;
-- Returns True if the names of both entities correspond with matching
return Flag16 (N);
end Import_Interface_Present;
- function In_Assertion
+ function In_Assertion_Expression
(N : Node_Id) return Boolean is
begin
pragma Assert (False
or else NT (N).Nkind = N_Function_Call);
return Flag4 (N);
- end In_Assertion;
+ end In_Assertion_Expression;
function In_Present
(N : Node_Id) return Boolean is
Set_Flag16 (N, Val);
end Set_Import_Interface_Present;
- procedure Set_In_Assertion
+ procedure Set_In_Assertion_Expression
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
or else NT (N).Nkind = N_Function_Call);
Set_Flag4 (N, Val);
- end Set_In_Assertion;
+ end Set_In_Assertion_Expression;
procedure Set_In_Present
(N : Node_Id; Val : Boolean := True) is
-- pragma of the other kind is also present. This is used to avoid
-- generating some unwanted error messages.
- -- In_Assertion (Flag4-Sem)
+ -- In_Assertion_Expression (Flag4-Sem)
-- This flag is present in N_Function_Call nodes. It is set if the
-- function is called from within an assertion expression. This is
-- used to avoid some bogus warnings about early elaboration.
-- actual parameter part)
-- First_Named_Actual (Node4-Sem)
-- Controlling_Argument (Node1-Sem) (set to Empty if not dispatching)
- -- In_Assertion (Flag4-Sem)
+ -- In_Assertion_Expression (Flag4-Sem)
-- Is_Expanded_Build_In_Place_Call (Flag11-Sem)
-- Do_Tag_Check (Flag13-Sem)
-- No_Elaboration_Check (Flag14-Sem)
function Import_Interface_Present
(N : Node_Id) return Boolean; -- Flag16
- function In_Assertion
+ function In_Assertion_Expression
(N : Node_Id) return Boolean; -- Flag4
function In_Present
procedure Set_Import_Interface_Present
(N : Node_Id; Val : Boolean := True); -- Flag16
- procedure Set_In_Assertion
+ procedure Set_In_Assertion_Expression
(N : Node_Id; Val : Boolean := True); -- Flag4
procedure Set_In_Present
pragma Inline (Interface_Present);
pragma Inline (Includes_Infinities);
pragma Inline (Import_Interface_Present);
- pragma Inline (In_Assertion);
+ pragma Inline (In_Assertion_Expression);
pragma Inline (In_Present);
pragma Inline (Inherited_Discriminant);
pragma Inline (Instance_Spec);
pragma Inline (Set_Interface_List);
pragma Inline (Set_Interface_Present);
pragma Inline (Set_Import_Interface_Present);
- pragma Inline (Set_In_Assertion);
+ pragma Inline (Set_In_Assertion_Expression);
pragma Inline (Set_In_Present);
pragma Inline (Set_Inherited_Discriminant);
pragma Inline (Set_Instance_Spec);
Name_Export_Valued_Procedure : constant Name_Id := N + $; -- GNAT
Name_External : constant Name_Id := N + $; -- GNAT
Name_Finalize_Storage_Only : constant Name_Id := N + $; -- GNAT
+ Name_Ghost : constant Name_Id := N + $; -- GNAT
Name_Global : constant Name_Id := N + $; -- GNAT
Name_Ident : constant Name_Id := N + $; -- VMS
Name_Implementation_Defined : constant Name_Id := N + $; -- GNAT
Pragma_Export_Valued_Procedure,
Pragma_External,
Pragma_Finalize_Storage_Only,
+ Pragma_Ghost,
Pragma_Global,
Pragma_Ident,
Pragma_Implementation_Defined,
projects / thirdparty / gcc.git / commitdiff
