+2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * atree.adb (Allocate_Initialize_Node): A newly created node is
+ no longer marked as Ghost at this level.
+ (Mark_New_Ghost_Node): New routine.
+ (New_Copy): Mark the copy as Ghost.
+ (New_Entity): Mark the entity as Ghost.
+ (New_Node): Mark the node as Ghost.
+ * einfo.adb (Is_Checked_Ghost_Entity): This attribute can now
+ apply to unanalyzed entities.
+ (Is_Ignored_Ghost_Entity): This attribute can now apply to unanalyzed
+ entities.
+ (Set_Is_Checked_Ghost_Entity): This attribute now
+ applies to all entities as well as unanalyzed entities.
+ (Set_Is_Ignored_Ghost_Entity): This attribute now applies to
+ all entities as well as unanalyzed entities.
+ * expander.adb Add with and use clauses for Ghost.
+ (Expand): Install and revert the Ghost region associated with the node
+ being expanded.
+ * exp_ch3.adb (Expand_Freeze_Array_Type): Remove all Ghost-related code.
+ (Expand_Freeze_Class_Wide_Type): Remoe all Ghost-related code.
+ (Expand_Freeze_Enumeration_Type): Remove all Ghost-related code.
+ (Expand_Freeze_Record_Type): Remove all Ghost-related code.
+ (Freeze_Type): Install and revert the Ghost region associated
+ with the type being frozen.
+ * exp_ch5.adb Remove with and use clauses for Ghost.
+ (Expand_N_Assignment_Statement): Remove all Ghost-related code.
+ * exp_ch6.adb Remove with and use clauses for Ghost.
+ (Expand_N_Procedure_Call_Statement): Remove all Ghost-relatd code.
+ (Expand_N_Subprogram_Body): Remove all Ghost-related code.
+ * exp_ch7.adb (Build_Invariant_Procedure_Body): Install and revert the
+ Ghost region of the working type.
+ (Build_Invariant_Procedure_Declaration): Install and revert
+ the Ghost region of the working type.
+ (Expand_N_Package_Body): Remove all Ghost-related code.
+ * exp_ch8.adb Remove with and use clauses for Ghost.
+ (Expand_N_Exception_Renaming_Declaration): Remove all Ghost-related
+ code.
+ (Expand_N_Object_Renaming_Declaration): Remove all Ghost-related code.
+ (Expand_N_Package_Renaming_Declaration): Remove all Ghost-related code.
+ (Expand_N_Subprogram_Renaming_Declaration): Remove all Ghost-related
+ code.
+ * exp_ch13.adb Remove with and use clauses for Ghost.
+ (Expand_N_Freeze_Entity): Remove all Ghost-related code.
+ * exp_disp.adb (Make_DT): Install and revert the Ghost region of
+ the tagged type. Move the generation of various entities within
+ the Ghost region of the type.
+ * exp_prag.adb Remove with and use clauses for Ghost.
+ (Expand_Pragma_Check): Remove all Ghost-related code.
+ (Expand_Pragma_Contract_Cases): Remove all Ghost-related code.
+ (Expand_Pragma_Initial_Condition): Remove all Ghost-related code.
+ (Expand_Pragma_Loop_Variant): Remove all Ghost-related code.
+ * exp_util.adb (Build_DIC_Procedure_Body): Install
+ and revert the Ghost region of the working types.
+ (Build_DIC_Procedure_Declaration): Install and revert the
+ Ghost region of the working type.
+ (Make_Invariant_Call): Install and revert the Ghost region of the
+ associated type.
+ (Make_Predicate_Call): Reimplemented. Install and revert the
+ Ghost region of the associated type.
+ * freeze.adb (Freeze_Entity): Install and revert the Ghost region
+ of the entity being frozen.
+ (New_Freeze_Node): Removed.
+ * ghost.adb Remove with and use clauses for Opt.
+ (Check_Ghost_Completion): Update the parameter profile
+ and all references to formal parameters.
+ (Ghost_Entity): Update the comment on usage.
+ (Install_Ghost_Mode): New routines.
+ (Is_Ghost_Assignment): New routine.
+ (Is_Ghost_Declaration): New routine.
+ (Is_Ghost_Pragma): New routine.
+ (Is_Ghost_Procedure_Call): New routine.
+ (Is_Ghost_Renaming): Removed.
+ (Is_OK_Declaration): Reimplemented.
+ (Is_OK_Pragma): Reimplemented.
+ (Is_OK_Statement): Reimplemented.
+ (Is_Subject_To_Ghost): Update the comment on usage.
+ (Mark_And_Set_Ghost_Assignment): New routine.
+ (Mark_And_Set_Ghost_Body): New routine.
+ (Mark_And_Set_Ghost_Completion): New routine.
+ (Mark_And_Set_Ghost_Declaration): New routine.
+ (Mark_And_Set_Ghost_Instantiation): New routine.
+ (Mark_And_Set_Ghost_Procedure_Call): New routine.
+ (Mark_Full_View_As_Ghost): Removed.
+ (Mark_Ghost_Declaration_Or_Body): New routine.
+ (Mark_Ghost_Pragma): New routine.
+ (Mark_Ghost_Renaming): New routine.
+ (Mark_Pragma_As_Ghost): Removed.
+ (Mark_Renaming_As_Ghost): Removed.
+ (Propagate_Ignored_Ghost_Code): Update the comment on usage.
+ (Prune_Node): Freeze nodes no longer need special pruning, they
+ are processed by the general ignored Ghost code mechanism.
+ (Restore_Ghost_Mode): New routine.
+ (Set_Ghost_Mode): Reimplemented.
+ (Set_Ghost_Mode_From_Entity): Removed.
+ * ghost.ads Add with and use clauses for Ghost.
+ (Check_Ghost_Completion): Update the parameter profile
+ along with the comment on usage.
+ (Install_Ghost_Mode): New routine.
+ (Is_Ghost_Assignment): New routine.
+ (Is_Ghost_Declaration): New routine.
+ (Is_Ghost_Pragma): New routine.
+ (Is_Ghost_Procedure_Call): New routine.
+ (Mark_And_Set_Ghost_Assignment): New routine.
+ (Mark_And_Set_Ghost_Body): New routine.
+ (Mark_And_Set_Ghost_Completion): New routine.
+ (Mark_And_Set_Ghost_Declaration): New routine.
+ (Mark_And_Set_Ghost_Instantiation): New routine.
+ (Mark_And_Set_Ghost_Procedure_Call): New routine.
+ (Mark_Full_View_As_Ghost): Removed.
+ (Mark_Ghost_Pragma): New routine.
+ (Mark_Ghost_Renaming): New routine.
+ (Mark_Pragma_As_Ghost): Removed.
+ (Mark_Renaming_As_Ghost): Removed.
+ (Restore_Ghost_Mode): New routine.
+ (Set_Ghost_Mode): Redefined.
+ (Set_Ghost_Mode_From_Entity): Removed.
+ * sem.adb (Analyze): Install and revert the Ghost region of the
+ node being analyzed.
+ (Do_Analyze): Change the way a clean Ghost
+ region is installed and reverted.
+ * sem_ch3.adb (Analyze_Full_Type_Declaration): Remove
+ all Ghost-related code.
+ (Analyze_Incomplete_Type_Decl): Remove all Ghost-related code.
+ (Analyze_Number_Declaration): Remove all Ghost-related code.
+ (Analyze_Object_Declaration): Install and revert the Ghost region of
+ a deferred object declaration's completion.
+ (Array_Type_Declaration): Remove all Ghost-related code.
+ (Build_Derived_Type): Update the comment on
+ the propagation of Ghost attributes from a parent to a derived type.
+ (Derive_Subprogram): Remove all Ghost-related code.
+ (Make_Class_Wide_Type): Remove all Ghost-related code.
+ (Make_Implicit_Base): Remove all Ghost-related code.
+ (Process_Full_View): Install and revert the Ghost region of
+ the partial view. There is no longer need to check the Ghost
+ completion here.
+ * sem_ch5.adb (Analyze_Assignment): Install and revert the Ghost
+ region of the left hand side.
+ * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Remove
+ all Ghost-related code.
+ (Analyze_Expression_Function): Remove all Ghost-related code.
+ (Analyze_Generic_Subprogram_Body): Remove all Ghost-related code.
+ (Analyze_Procedure_Call): Install and revert the Ghost region of
+ the procedure being called.
+ (Analyze_Subprogram_Body_Helper): Install and revert the Ghost
+ region of the spec or body.
+ (Analyze_Subprogram_Declaration): Remove all Ghost-related code.
+ (Build_Subprogram_Declaration): Remove all Ghost-related code.
+ (Find_Corresponding_Spec): Remove all Ghost-related code.
+ (Process_Formals): Remove all Ghost-related code.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Install and revert
+ the Ghost region of the spec.
+ (Analyze_Package_Declaration): Remove all Ghost-related code.
+ * sem_ch8.adb (Analyze_Exception_Renaming): Mark a renaming as
+ Ghost when it aliases a Ghost entity.
+ (Analyze_Generic_Renaming): Mark a renaming as Ghost when it aliases
+ a Ghost entity.
+ (Analyze_Object_Renaming): Mark a renaming as Ghost when
+ it aliases a Ghost entity.
+ (Analyze_Package_Renaming): Mark a renaming as Ghost when it aliases
+ a Ghost entity.
+ (Analyze_Subprogram_Renaming): Mark a renaming as Ghost when it
+ aliases a Ghost entity.
+ * sem_ch11.adb Remove with and use clauses for Ghost.
+ (Analyze_Exception_Declaration): Remove all Ghost-related code.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration): Remove all
+ Ghost-related code.
+ (Analyze_Generic_Subprogram_Declaration): Remove all Ghost-related
+ code.
+ (Analyze_Package_Instantiation): Install and revert the Ghost region
+ of the package instantiation.
+ (Analyze_Subprogram_Instantiation): Install
+ and revert the Ghost region of the subprogram instantiation.
+ (Instantiate_Package_Body): Code clean up. Install and revert the
+ Ghost region of the package body.
+ (Instantiate_Subprogram_Body): Code clean up. Install and revert the
+ Ghost region of the subprogram body.
+ * sem_ch13.adb (Build_Predicate_Functions): Install
+ and revert the Ghost region of the related type.
+ (Build_Predicate_Function_Declaration): Code clean up. Install
+ and rever the Ghost region of the related type.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
+ Install and revert the Ghost region of the pragma.
+ (Analyze_Initial_Condition_In_Decl_Part): Install and revert the
+ Ghost region of the pragma.
+ (Analyze_Pragma): Install and revert the Ghost region of various
+ pragmas. Mark a pragma as Ghost when it is related to a Ghost entity
+ or encloses a Ghost entity.
+ (Analyze_Pre_Post_Condition): Install and revert the Ghost
+ region of the pragma.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Install and revert the
+ Ghost region of the pragma.
+ * sem_res.adb (Resolve): Remove all Ghost-related code.
+ * sem_util.adb (Is_Declaration): Reimplemented.
+ (Is_Declaration_Other_Than_Renaming): New routine.
+ * sem_util.ads (Is_Declaration_Other_Than_Renaming): New routine.
+ * sinfo.adb (Is_Checked_Ghost_Pragma): New routine.
+ (Is_Ghost_Pragma): Removed.
+ (Is_Ignored_Ghost_Pragma): New routine.
+ (Set_Is_Checked_Ghost_Pragma): New routine.
+ (Set_Is_Ghost_Pragma): Removed.
+ (Set_Is_Ignored_Ghost_Pragma): New routine.
+ * sinfo.ads: Update the documentation on Ghost mode and
+ Ghost regions. New attributes Is_Checked_Ghost_Pragma
+ and Is_Ignored_Ghost_Pragma along with usages in nodes.
+ Remove attribute Is_Ghost_Pragma along with usages in nodes.
+ (Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
+ (Is_Ghost_Pragma): Removed along with pragma Inline.
+ (Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.
+ (Set_Is_Checked_Ghost_Pragma): New routine along with pragma Inline.
+ (Set_Is_Ghost_Pragma): Removed along with pragma Inline.
+ (Set_Is_Ignored_Ghost_Pragma): New routine along with pragma Inline.
+
2017-01-12 Tristan Gingold <gingold@adacore.com>
* s-mmap.ads, s-mmap.adb, s-mmosin-unix.ads, s-mmosin-unix.adb,
-- Local Subprograms --
-----------------------
- procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
- -- Fixup parent pointers for the syntactic children of Fix_Node after
- -- a copy, setting them to Fix_Node when they pointed to Ref_Node.
-
function Allocate_Initialize_Node
(Src : Node_Id;
With_Extension : Boolean) return Node_Id;
-- Allocate a new node or node extension. If Src is not empty, the
-- information for the newly-allocated node is copied from it.
+ procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
+ -- Fixup parent pointers for the syntactic children of Fix_Node after a
+ -- copy, setting them to Fix_Node when they pointed to Ref_Node.
+
+ procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id);
+ -- Mark arbitrary node or entity N as Ghost when it is created within a
+ -- Ghost region.
+
------------------------------
-- Allocate_Initialize_Node --
------------------------------
Node_Count := Node_Count + 1;
end if;
- -- Mark the node as ignored Ghost if it is created in an ignored Ghost
- -- region.
-
- if Ghost_Mode = Ignore then
- Set_Is_Ignored_Ghost_Node (New_Id);
- end if;
-
-- Clear Check_Actuals to False
Set_Check_Actuals (New_Id, False);
-----------------
procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is
-
procedure Fix_Parent (Field : Union_Id);
-- Fixup one parent pointer. Field is checked to see if it points to
-- a node, list, or element list that has a parent that points to
Orig_Nodes.Release;
end Lock;
+ -------------------------
+ -- Mark_New_Ghost_Node --
+ -------------------------
+
+ procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id) is
+ begin
+ -- The Ghost node is created within a Ghost region
+
+ if Ghost_Mode = Check then
+ if Nkind (N) in N_Entity then
+ Set_Is_Checked_Ghost_Entity (N);
+ end if;
+
+ elsif Ghost_Mode = Ignore then
+ if Nkind (N) in N_Entity then
+ Set_Is_Ignored_Ghost_Entity (N);
+ end if;
+
+ Set_Is_Ignored_Ghost_Node (N);
+ end if;
+ end Mark_New_Ghost_Node;
+
----------------------------
-- Mark_Rewrite_Insertion --
----------------------------
-- aspects if this is required for the particular situation.
Set_Has_Aspects (New_Id, False);
+
+ -- Mark the copy as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (New_Id);
end if;
return New_Id;
Nodes.Table (Ent).Sloc := New_Sloc;
pragma Debug (New_Node_Debugging_Output (Ent));
+ -- Mark the new entity as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (Ent);
+
return Ent;
end New_Entity;
Current_Error_Node := Nod;
end if;
+ -- Mark the new node as Ghost depending on the current Ghost region
+
+ Mark_New_Ghost_Node (Nod);
+
return Nod;
end New_Node;
function Is_Checked_Ghost_Entity (Id : E) return B is
begin
- pragma Assert (Nkind (Id) in N_Entity);
+ -- Allow this attribute to appear on non-analyzed entities
+
+ pragma Assert (Nkind (Id) in N_Entity
+ or else Ekind (Id) = E_Void);
return Flag277 (Id);
end Is_Checked_Ghost_Entity;
function Is_Ignored_Ghost_Entity (Id : E) return B is
begin
- pragma Assert (Nkind (Id) in N_Entity);
+ -- Allow this attribute to appear on non-analyzed entities
+
+ pragma Assert (Nkind (Id) in N_Entity
+ or else Ekind (Id) = E_Void);
return Flag278 (Id);
end Is_Ignored_Ghost_Entity;
procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is
begin
- pragma Assert (Is_Formal (Id)
- or else Is_Object (Id)
- or else Is_Package_Or_Generic_Package (Id)
- or else Is_Subprogram_Or_Generic_Subprogram (Id)
- or else Is_Type (Id)
- or else Ekind (Id) = E_Abstract_State
- or else Ekind (Id) = E_Component
- or else Ekind (Id) = E_Discriminant
- or else Ekind (Id) = E_Exception
- or else Ekind (Id) = E_Package_Body
- or else Ekind (Id) = E_Subprogram_Body
-
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on non-analyzed entities
+ pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
Set_Flag277 (Id, V);
end Set_Is_Checked_Ghost_Entity;
procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is
begin
- pragma Assert (Is_Formal (Id)
- or else Is_Object (Id)
- or else Is_Package_Or_Generic_Package (Id)
- or else Is_Subprogram_Or_Generic_Subprogram (Id)
- or else Is_Type (Id)
- or else Ekind (Id) = E_Abstract_State
- or else Ekind (Id) = E_Component
- or else Ekind (Id) = E_Discriminant
- or else Ekind (Id) = E_Exception
- or else Ekind (Id) = E_Package_Body
- or else Ekind (Id) = E_Subprogram_Body
-
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on non-analyzed entities
+ pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
Set_Flag278 (Id, V);
end Set_Is_Ignored_Ghost_Entity;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
-with Ghost; use Ghost;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
Insert_Action (N,
Make_Object_Declaration (Loc,
Defining_Identifier => Temp_Id,
- Object_Definition =>
- New_Occurrence_Of (Expr_Typ, Loc),
- Expression =>
- Relocate_Node (Expr)));
+ Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
+ Expression => Relocate_Node (Expr)));
New_Expr := New_Occurrence_Of (Temp_Id, Loc);
Set_Etype (New_Expr, Expr_Typ);
procedure Expand_N_Freeze_Entity (N : Node_Id) is
E : constant Entity_Id := Entity (N);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Decl : Node_Id;
Delete : Boolean := False;
E_Scope : Entity_Id;
In_Outer_Scope : Boolean;
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (E);
-
-- If there are delayed aspect specifications, we insert them just
-- before the freeze node. They are already analyzed so we don't need
-- to reanalyze them (they were analyzed before the type was frozen),
-- statement, insert them back into the tree now.
Explode_Initialization_Compound_Statement (E);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Only other items requiring any front end action are types and
-- subprograms.
elsif not Is_Type (E) and then not Is_Subprogram (E) then
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if No (E_Scope) then
Check_Error_Detected;
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- whether we are inside a (possibly nested) call to this procedure.
Inside_Freezing_Actions := Inside_Freezing_Actions - 1;
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Freeze_Entity;
-------------------------------------------
Base : constant Entity_Id := Base_Type (Typ);
Comp_Typ : constant Entity_Id := Component_Type (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
if not Is_Bit_Packed_Array (Typ) then
-- If the component contains tasks, so does the array type. This may
then
Build_Array_Init_Proc (Base, N);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Array_Type;
-----------------------------------
Typ : constant Entity_Id := Entity (N);
Root : constant Entity_Id := Root_Type (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_Freeze_Class_Wide_Type
begin
return;
end if;
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Create the body of TSS primitive Finalize_Address. This automatically
-- sets the TSS entry for the class-wide type.
Make_Finalize_Address_Body (Typ);
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Class_Wide_Type;
------------------------------------
Typ : constant Entity_Id := Entity (N);
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Arr : Entity_Id;
Ent : Entity_Id;
Fent : Entity_Id;
pragma Warnings (Off, Func);
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Various optimizations possible if given representation is contiguous
Is_Contiguous := True;
Set_Debug_Info_Off (Fent);
end if;
- Ghost_Mode := Save_Ghost_Mode;
-
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_Freeze_Enumeration_Type;
Typ : constant Node_Id := Entity (N);
Typ_Decl : constant Node_Id := Parent (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Comp : Entity_Id;
Comp_Typ : Entity_Id;
Predef_List : List_Id;
-- Start of processing for Expand_Freeze_Record_Type
begin
- -- Ensure that all freezing activities are properly flagged as Ghost
-
- Set_Ghost_Mode_From_Entity (Typ);
-
-- Build discriminant checking functions if not a derived type (for
-- derived types that are not tagged types, always use the discriminant
-- checking functions of the parent type). However, for untagged types
end loop;
end;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Freeze_Record_Type;
------------------------------------
-- Local variables
Def_Id : constant Entity_Id := Entity (N);
+ Mode : Ghost_Mode_Type;
Result : Boolean := False;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Freeze_Type
begin
-- now to ensure that any nodes generated during freezing are properly
-- marked as Ghost.
- Set_Ghost_Mode (N, Def_Id);
+ Set_Ghost_Mode (Def_Id, Mode);
-- Process any remote access-to-class-wide types designating the type
-- being frozen.
Build_Invariant_Procedure_Body (Def_Id);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return Result;
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return False;
end Freeze_Type;
with Exp_Pakd; use Exp_Pakd;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
Typ : constant Entity_Id := Underlying_Type (Etype (Lhs));
Exp : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The assignment statement is Ghost when the left hand side is Ghost.
- -- Set the mode now to ensure that any nodes generated during expansion
- -- are properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
-- Special case to check right away, if the Componentwise_Assignment
-- flag is set, this is a reanalysis from the expansion of the primitive
-- assignment procedure for a tagged type, and all we need to do is to
if Componentwise_Assignment (N) then
Expand_Assign_Record (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Rewrite (N, Call);
Analyze (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end;
loop
Set_Analyzed (Exp, False);
- if Nkind_In
- (Exp, N_Selected_Component, N_Indexed_Component)
+ if Nkind_In (Exp, N_Indexed_Component,
+ N_Selected_Component)
then
Exp := Prefix (Exp);
else
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
if not Crep then
Expand_Bit_Packed_Element_Set (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Change of representation case
-- expansion, since they would be missed in -gnatc mode ???
Error_Msg_N ("assignment not available on limited type", N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- it with all checks suppressed.
Analyze (N, Suppress => All_Checks);
- Ghost_Mode := Save_Ghost_Mode;
return;
end Tagged_Case;
end loop;
Expand_Assign_Array (N, Actual_Rhs);
- Ghost_Mode := Save_Ghost_Mode;
return;
end;
elsif Is_Record_Type (Typ) then
Expand_Assign_Record (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Scalar types. This is where we perform the processing related to the
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
-
exception
when RE_Not_Available =>
- Ghost_Mode := Save_Ghost_Mode;
return;
end Expand_N_Assignment_Statement;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
-with Ghost; use Ghost;
with Inline; use Inline;
with Lib; use Lib;
with Namet; use Namet;
---------------------------------------
procedure Expand_N_Procedure_Call_Statement (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The procedure call is Ghost when the name is Ghost. Set the mode now
- -- to ensure that any nodes generated during expansion are properly set
- -- as Ghost.
-
- Set_Ghost_Mode (N);
-
Expand_Call (N);
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Procedure_Call_Statement;
--------------------------------------
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Except_H : Node_Id;
L : List_Id;
Spec_Id : Entity_Id;
end if;
end if;
- -- The subprogram body is Ghost when it is stand alone and subject to
- -- pragma Ghost or the corresponding spec is Ghost. To accomodate both
- -- cases, set the mode now to ensure that any nodes generated during
- -- expansion are marked as Ghost.
-
- Set_Ghost_Mode (N, Spec_Id);
-
-- Set L to either the list of declarations if present, or to the list
-- of statements if no declarations are present. This is used to insert
-- new stuff at the start.
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (Make_Null_Statement (Loc))));
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
begin
if not Acts_As_Spec (N)
and then Nkind (Parent (Parent (Spec_Id))) /=
- N_Subprogram_Body_Stub
+ N_Subprogram_Body_Stub
then
null;
-- Set to encode entity names in package body before gigi is called
Qualify_Entity_Names (N);
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Body;
-----------------------------------
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Dummy : Entity_Id;
+ Mode : Ghost_Mode_Type;
Priv_Item : Node_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the invariant procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent types or interfaces, or be an array or record
-- type whose components have invariants.
-- inherited by implementing types.
if Is_Interface (Work_Typ) then
- return;
+ goto Leave;
end if;
-- Obtain both views of the type
-- Nothing to do because the processing of the underlying full
-- view already checked the invariants of the partial view.
- return;
+ goto Leave;
end if;
-- Create a declaration for the "partial" invariant procedure if it
-- Nothing to do if the invariant procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the invariant procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
-- Emulate the environment of the invariant procedure by installing
-- its scope and formal parameters. Note that this is not needed, but
-- having the scope of the invariant procedure installed helps with
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_Invariant_Procedure_Body;
-------------------------------------------
is
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
+ Mode : Ghost_Mode_Type;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Nam : Name_Id;
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the invariant procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent or interface types, or be an array or record
-- type whose components have invariants.
-- inherited by implementing types.
if Is_Interface (Work_Typ) then
- return;
+ goto Leave;
-- Nothing to do if the type already has a "partial" invariant procedure
elsif Partial_Invariant then
if Present (Partial_Invariant_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
-- Nothing to do if the type already has a "full" invariant procedure
elsif Present (Invariant_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the invariant procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
-- The caller requests the declaration of the "partial" invariant
-- procedure.
Set_Needs_Debug_Info (Proc_Id);
end if;
- -- Mark the invariant procedure explicitly as Ghost because it does not
- -- come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Proc_Id);
- end if;
-
-- Obtain all views of the input type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_Invariant_Procedure_Declaration;
---------------------
Spec_Id : constant Entity_Id := Corresponding_Spec (N);
Fin_Id : Entity_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
- -- The package body is Ghost when the corresponding spec is Ghost. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N, Spec_Id);
-
-- This is done only for non-generic packages
if Ekind (Spec_Id) = E_Package then
end;
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Body;
----------------------------------
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
-with Ghost; use Ghost;
with Namet; use Namet;
with Nmake; use Nmake;
with Nlists; use Nlists;
---------------------------------------------
procedure Expand_N_Exception_Renaming_Declaration (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Decl : Node_Id;
begin
- -- The exception renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Exception_Renaming_Declaration;
------------------------------------------
end if;
end Evaluation_Required;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_N_Object_Renaming_Declaration
begin
- -- The object renaming declaration is Ghost when it is subject to pragma
- -- Ghost or renames a Ghost entity. To accomodate both cases, set the
- -- mode now to ensure that any nodes generated during expansion are
- -- properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
-- Perform name evaluation if required
if Evaluation_Required (Nam) then
if Present (Decl) then
Insert_Action (N, Decl);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Object_Renaming_Declaration;
-------------------------------------------
-------------------------------------------
procedure Expand_N_Package_Renaming_Declaration (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Decl : Node_Id;
begin
- -- The package renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases,
- -- set the mode now to ensure that any nodes generated during expansion
- -- are properly marked as Ghost.
-
- Set_Ghost_Mode (N);
-
Decl := Debug_Renaming_Declaration (N);
if Present (Decl) then
Insert_Action (N, Decl);
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Package_Renaming_Declaration;
----------------------------------------------
-- Local variables
- Nam : constant Node_Id := Name (N);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Nam : constant Node_Id := Name (N);
-- Start of processing for Expand_N_Subprogram_Renaming_Declaration
begin
- -- The subprogram renaming declaration is Ghost when it is subject to
- -- pragma Ghost or renames a Ghost entity. To accomodate both cases, set
- -- the mode now to ensure that any nodes created during expansion are
- -- properly flagged as ignored Ghost.
-
- Set_Ghost_Mode (N);
-
-- When the prefix of the name is a function call, we must force the
-- call to be made by removing side effects from the call, since we
-- must only call the function once.
end if;
end;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Renaming_Declaration;
end Exp_Ch8;
-- Local variables
- Elab_Code : constant List_Id := New_List;
- Result : constant List_Id := New_List;
- Tname : constant Name_Id := Chars (Typ);
+ Elab_Code : constant List_Id := New_List;
+ Result : constant List_Id := New_List;
+ Tname : constant Name_Id := Chars (Typ);
+
+ -- The following name entries are used by Make_DT to generate a number
+ -- of entities related to a tagged type. These entities may be generated
+ -- in a scope other than that of the tagged type declaration, and if
+ -- the entities for two tagged types with the same name happen to be
+ -- generated in the same scope, we have to take care to use different
+ -- names. This is achieved by means of a unique serial number appended
+ -- to each generated entity name.
+
+ Name_DT : constant Name_Id :=
+ New_External_Name (Tname, 'T', Suffix_Index => -1);
+ Name_Exname : constant Name_Id :=
+ New_External_Name (Tname, 'E', Suffix_Index => -1);
+ Name_HT_Link : constant Name_Id :=
+ New_External_Name (Tname, 'H', Suffix_Index => -1);
+ Name_Predef_Prims : constant Name_Id :=
+ New_External_Name (Tname, 'R', Suffix_Index => -1);
+ Name_SSD : constant Name_Id :=
+ New_External_Name (Tname, 'S', Suffix_Index => -1);
+ Name_TSD : constant Name_Id :=
+ New_External_Name (Tname, 'B', Suffix_Index => -1);
+
AI : Elmt_Id;
AI_Tag_Elmt : Elmt_Id;
AI_Tag_Comp : Elmt_Id;
+ DT : Entity_Id;
DT_Aggr_List : List_Id;
DT_Constr_List : List_Id;
DT_Ptr : Entity_Id;
+ Exname : Entity_Id;
+ HT_Link : Entity_Id;
ITable : Node_Id;
I_Depth : Nat := 0;
Iface_Table_Node : Node_Id;
+ Mode : Ghost_Mode_Type;
Name_ITable : Name_Id;
Nb_Predef_Prims : Nat := 0;
Nb_Prim : Nat := 0;
New_Node : Node_Id;
Num_Ifaces : Nat := 0;
Parent_Typ : Entity_Id;
+ Predef_Prims : Entity_Id;
Prim : Entity_Id;
Prim_Elmt : Elmt_Id;
Prim_Ops_Aggr_List : List_Id;
+ SSD : Entity_Id;
Suffix_Index : Int;
Typ_Comps : Elist_Id;
Typ_Ifaces : Elist_Id;
+ TSD : Entity_Id;
TSD_Aggr_List : List_Id;
TSD_Tags_List : List_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
- -- The following name entries are used by Make_DT to generate a number
- -- of entities related to a tagged type. These entities may be generated
- -- in a scope other than that of the tagged type declaration, and if
- -- the entities for two tagged types with the same name happen to be
- -- generated in the same scope, we have to take care to use different
- -- names. This is achieved by means of a unique serial number appended
- -- to each generated entity name.
-
- Name_DT : constant Name_Id :=
- New_External_Name (Tname, 'T', Suffix_Index => -1);
- Name_Exname : constant Name_Id :=
- New_External_Name (Tname, 'E', Suffix_Index => -1);
- Name_HT_Link : constant Name_Id :=
- New_External_Name (Tname, 'H', Suffix_Index => -1);
- Name_Predef_Prims : constant Name_Id :=
- New_External_Name (Tname, 'R', Suffix_Index => -1);
- Name_SSD : constant Name_Id :=
- New_External_Name (Tname, 'S', Suffix_Index => -1);
- Name_TSD : constant Name_Id :=
- New_External_Name (Tname, 'B', Suffix_Index => -1);
-
- -- Entities built with above names
-
- DT : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_DT);
- Exname : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_Exname);
- HT_Link : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_HT_Link);
- Predef_Prims : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_Predef_Prims);
- SSD : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_SSD);
- TSD : constant Entity_Id :=
- Make_Defining_Identifier (Loc, Name_TSD);
-
-- Start of processing for Make_DT
begin
-- the mode now to ensure that any nodes generated during dispatch table
-- creation are properly marked as Ghost.
- Set_Ghost_Mode (Declaration_Node (Typ), Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Handle cases in which there is no need to build the dispatch table
or else No (Access_Disp_Table (Typ))
or else Is_CPP_Class (Typ)
then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
elsif not RTE_Available (RE_Tag) then
Append_To (Result,
Make_Object_Declaration (Loc,
- Defining_Identifier => Node (First_Elmt
- (Access_Disp_Table (Typ))),
+ Defining_Identifier =>
+ Node (First_Elmt (Access_Disp_Table (Typ))),
Object_Definition => New_Occurrence_Of (RTE (RE_Tag), Loc),
Constant_Present => True,
Expression =>
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- Ensure that the value of Max_Predef_Prims defined in a-tags is
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
else
if Max_Predef_Prims /= 9 then
Error_Msg_N ("run-time library configuration error", Typ);
Error_Msg_CRT ("tagged types", Typ);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
end if;
+ DT := Make_Defining_Identifier (Loc, Name_DT);
+ Exname := Make_Defining_Identifier (Loc, Name_Exname);
+ HT_Link := Make_Defining_Identifier (Loc, Name_HT_Link);
+ Predef_Prims := Make_Defining_Identifier (Loc, Name_Predef_Prims);
+ SSD := Make_Defining_Identifier (Loc, Name_SSD);
+ TSD := Make_Defining_Identifier (Loc, Name_TSD);
+
-- Initialize Parent_Typ handling private types
Parent_Typ := Etype (Typ);
Set_SCIL_Entity (New_Node, Typ);
Set_SCIL_Node (Last (Result), New_Node);
- goto Early_Exit_For_SCIL;
+ goto Leave_SCIL;
-- Gnat2scil has its own implementation of dispatch tables,
-- different than what is being implemented here. Generating
Set_SCIL_Entity (New_Node, Typ);
Set_SCIL_Node (Last (Result), New_Node);
- goto Early_Exit_For_SCIL;
+ goto Leave_SCIL;
-- Gnat2scil has its own implementation of dispatch tables,
-- different than what is being implemented here. Generating
end;
end if;
- <<Early_Exit_For_SCIL>>
+ <<Leave_SCIL>>
-- Register the tagged type in the call graph nodes table
Register_CG_Node (Typ);
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
+
return Result;
end Make_DT;
with Exp_Ch11; use Exp_Ch11;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
-with Ghost; use Ghost;
with Inline; use Inline;
with Namet; use Namet;
with Nlists; use Nlists;
-- Assert_Failure, so that coverage analysis tools can relate the
-- call to the failed check.
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
-- Nothing to do if pragma is ignored
return;
end if;
- -- Pragmas Assert, Assert_And_Cut, Assume, Check and Loop_Invariant are
- -- Ghost when they apply to a Ghost entity. Set the mode now to ensure
- -- that any nodes generated during expansion are properly flagged as
- -- Ghost.
-
- Set_Ghost_Mode (N);
-
- -- Since this check is active, we rewrite the pragma into a
- -- corresponding if statement, and then analyze the statement.
+ -- Since this check is active, rewrite the pragma into a corresponding
+ -- if statement, and then analyze the statement.
-- The normal case expansion transforms:
elsif Nam = Name_Assert then
Error_Msg_N ("?A?assertion will fail at run time", N);
else
-
Error_Msg_N ("?A?check will fail at run time", N);
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Check;
---------------------------------
Aggr : constant Node_Id :=
Expression (First (Pragma_Argument_Associations (CCs)));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Case_Guard : Node_Id;
CG_Checks : Node_Id;
CG_Stmts : List_Id;
return;
end if;
- -- The contract cases is Ghost when it applies to a Ghost entity. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly flagged as Ghost.
-
- Set_Ghost_Mode (CCs);
-
-- The expansion of contract cases is quite distributed as it produces
-- various statements to evaluate the case guards and consequences. To
-- preserve the original context, set the Is_Assertion_Expr flag. This
Append_To (Stmts, Conseq_Checks);
In_Assertion_Expr := In_Assertion_Expr - 1;
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Contract_Cases;
---------------------------------------
-------------------------------------
procedure Expand_Pragma_Initial_Condition (Spec_Or_Body : Node_Id) is
- Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
+ Loc : constant Source_Ptr := Sloc (Spec_Or_Body);
+
Check : Node_Id;
Expr : Node_Id;
Init_Cond : Node_Id;
List : List_Id;
Pack_Id : Entity_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
if Nkind (Spec_Or_Body) = N_Package_Body then
Pack_Id := Corresponding_Spec (Spec_Or_Body);
Init_Cond := Get_Pragma (Pack_Id, Pragma_Initial_Condition);
- -- The initial condition is Ghost when it applies to a Ghost entity. Set
- -- the mode now to ensure that any nodes generated during expansion are
- -- properly flagged as Ghost.
-
- Set_Ghost_Mode (Init_Cond);
-
-- The caller should check whether the package is subject to pragma
-- Initial_Condition.
-- runtime check as it will repeat the illegality.
if Error_Posted (Init_Cond) or else Error_Posted (Expr) then
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Append_To (List, Check);
Analyze (Check);
-
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Initial_Condition;
------------------------------------
-- Local variables
- Expr : constant Node_Id := Expression (Variant);
- Expr_Typ : constant Entity_Id := Etype (Expr);
+ Expr : constant Node_Id := Expression (Variant);
+ Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
Loop_Loc : constant Source_Ptr := Sloc (Loop_Stmt);
Curr_Id : Entity_Id;
end if;
end Process_Variant;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Expand_Pragma_Loop_Variant
begin
return;
end if;
- -- The loop variant is Ghost when it applies to a Ghost entity. Set
- -- the mode now to ensure that any nodes generated during expansion
- -- are properly flagged as Ghost.
-
- Set_Ghost_Mode (N);
-
-- The expansion of Loop_Variant is quite distributed as it produces
-- various statements to capture and compare the arguments. To preserve
-- the original context, set the Is_Assertion_Expr flag. This aids the
-- for documentation purposes. It will be ignored by the backend.
In_Assertion_Expr := In_Assertion_Expr - 1;
- Ghost_Mode := Save_Ghost_Mode;
end Expand_Pragma_Loop_Variant;
--------------------------------
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
+ Mode : Ghost_Mode_Type;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the DIC procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The working type must be either define a DIC pragma of its own or
-- inherit one from a parent type.
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
- return;
+ goto Leave;
end if;
-- The working type may lack a DIC procedure declaration. This may be
-- Nothing to do if the DIC procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the DIC procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
-- Emulate the environment of the DIC procedure by installing its scope
-- and formal parameters.
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_DIC_Procedure_Body;
-------------------------------------
procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is
Loc : constant Source_Ptr := Sloc (Typ);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
+ Mode : Ghost_Mode_Type;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Typ_Decl : Node_Id;
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
+ -- The working type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the DIC procedure is properly marked as Ghost.
+
+ Set_Ghost_Mode (Work_Typ, Mode);
+
-- The type must be either subject to a DIC pragma or inherit one from a
-- parent type.
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
- return;
+ goto Leave;
-- Nothing to do if the type already has a DIC procedure
elsif Present (DIC_Procedure (Work_Typ)) then
- return;
+ goto Leave;
end if;
- -- The working type may be subject to pragma Ghost. Set the mode now to
- -- ensure that the DIC procedure is properly marked as Ghost.
-
- Set_Ghost_Mode_From_Entity (Work_Typ);
-
Proc_Id :=
Make_Defining_Identifier (Loc,
Chars =>
Set_Needs_Debug_Info (Proc_Id);
end if;
- -- Mark the DIC procedure explicitly as Ghost because it does not come
- -- from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Proc_Id);
- end if;
-
-- Obtain all views of the input type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ);
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Build_DIC_Procedure_Declaration;
--------------------------
-------------------------
function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
- Loc : constant Source_Ptr := Sloc (Expr);
- Typ : constant Entity_Id := Base_Type (Etype (Expr));
+ Loc : constant Source_Ptr := Sloc (Expr);
+ Typ : constant Entity_Id := Base_Type (Etype (Expr));
+
Proc_Id : Entity_Id;
begin
Expr : Node_Id;
Mem : Boolean := False) return Node_Id
is
- Loc : constant Source_Ptr := Sloc (Expr);
- Call : Node_Id;
- PFM : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (Expr);
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Call : Node_Id;
+ Func_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
begin
pragma Assert (Present (Predicate_Function (Typ)));
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the call is properly marked as Ghost.
- Set_Ghost_Mode_From_Entity (Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Call special membership version if requested and available
- if Mem then
- PFM := Predicate_Function_M (Typ);
-
- if Present (PFM) then
- Call :=
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (PFM, Loc),
- Parameter_Associations => New_List (Relocate_Node (Expr)));
-
- Ghost_Mode := Save_Ghost_Mode;
- return Call;
- end if;
+ if Mem and then Present (Predicate_Function_M (Typ)) then
+ Func_Id := Predicate_Function_M (Typ);
+ else
+ Func_Id := Predicate_Function (Typ);
end if;
-- Case of calling normal predicate function
Call :=
Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Predicate_Function (Typ), Loc),
+ Name => New_Occurrence_Of (Func_Id, Loc),
Parameter_Associations => New_List (Relocate_Node (Expr)));
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
return Call;
end Make_Predicate_Call;
with Exp_Ch12; use Exp_Ch12;
with Exp_Ch13; use Exp_Ch13;
with Exp_Prag; use Exp_Prag;
+with Ghost; use Ghost;
with Opt; use Opt;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
------------
procedure Expand (N : Node_Id) is
+ Mode : Ghost_Mode_Type;
+
begin
-- If we were analyzing a default expression (or other spec expression)
-- the Full_Analysis flag must be off. If we are in expansion mode then
and then (Full_Analysis or else not Expander_Active)
and then not (Inside_A_Generic and then Expander_Active));
+ -- Establish the Ghost mode of the context to ensure that any generated
+ -- nodes during expansion are marked as Ghost.
+
+ Set_Ghost_Mode (N, Mode);
+
-- The GNATprove_Mode flag indicates that a light expansion for formal
-- verification should be used. This expansion is never done inside
-- generics, because otherwise, this breaks the name resolution
-- needed, and in general cannot be done correctly, in this mode, so
-- we are all done.
- return;
+ goto Leave;
-- There are three reasons for the Expander_Active flag to be false
Pop_Scope;
end if;
- return;
+ goto Leave;
else
begin
exception
when RE_Not_Available =>
- return;
+ goto Leave;
end;
-- Set result as analyzed and then do a possible transient wrap. The
Debug_A_Exit ("expanding ", N, " (done)");
end if;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Expand;
---------------------------
-- Determine whether an arbitrary entity is subject to Boolean aspect
-- Import and its value is specified as True.
- function New_Freeze_Node return Node_Id;
- -- Create a new freeze node for entity E
-
procedure Wrap_Imported_Subprogram (E : Entity_Id);
-- If E is an entity for an imported subprogram with pre/post-conditions
-- then this procedure will create a wrapper to ensure that proper run-
if Convention (Rec_Type) = Convention_C then
Error_Msg_N
- ("?x?discriminated record has no direct " &
- "equivalent in C",
- A2);
+ ("?x?discriminated record has no direct equivalent in "
+ & "C", A2);
else
Error_Msg_N
- ("?x?discriminated record has no direct " &
- "equivalent in C++",
- A2);
+ ("?x?discriminated record has no direct equivalent in "
+ & "C++", A2);
end if;
Error_Msg_NE
return False;
end Has_Boolean_Aspect_Import;
- ---------------------
- -- New_Freeze_Node --
- ---------------------
-
- function New_Freeze_Node return Node_Id is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
- Result : Node_Id;
-
- begin
- -- Handle the case where an ignored Ghost subprogram freezes the type
- -- of one of its formals. The type can either be non-Ghost or checked
- -- Ghost. Since the freeze node for the type is generated in the
- -- context of the subprogram, the node will be incorrectly flagged as
- -- ignored Ghost and erroneously removed from the tree.
-
- -- type Typ is ...;
- -- procedure Ignored_Ghost_Proc (Formal : Typ) with Ghost;
-
- -- Reset the Ghost mode to "none". This preserves the freeze node.
-
- if Ghost_Mode = Ignore
- and then not Is_Ignored_Ghost_Entity (E)
- and then not Is_Ignored_Ghost_Node (E)
- then
- Ghost_Mode := None;
- end if;
-
- Result := New_Node (N_Freeze_Entity, Loc);
-
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
- end New_Freeze_Node;
-
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Freeze_Entity
-- now to ensure that any nodes generated during freezing are properly
-- flagged as Ghost.
- Set_Ghost_Mode_From_Entity (E);
+ Set_Ghost_Mode (E, Mode);
-- We are going to test for various reasons why this entity need not be
-- frozen here, but in the case of an Itype that's defined within a
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
elsif Ekind (E) = E_Generic_Package then
Result := Freeze_Generic_Entities (E);
-
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- It is improper to freeze an external entity within a generic because
-- its freeze node will appear in a non-valid context. The entity will
Analyze_Aspects_At_Freeze_Point (E);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
-- the instance, the same applies to the subtype renaming the actual.
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
-- Do not freeze a global entity within an inner scope created during
-- expansion. A call to subprogram E within some internal procedure
then
exit;
else
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
end if;
end loop;
if No (S) then
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
end;
end if;
if not Is_Internal (E) and then Do_Freeze_Profile then
if not Freeze_Profile (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
end if;
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
-- Check for error of Type_Invariant'Class applied to an untagged
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- The equivalent type associated with a class-wide subtype needs
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of full view present
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of underlying full view present
Check_Debug_Info_Needed (E);
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
-- Case of no full view present. If entity is derived or subtype,
-- it is safe to freeze, correctness depends on the frozen status
else
Set_Is_Frozen (E, False);
- Ghost_Mode := Save_Ghost_Mode;
- return No_List;
+ Result := No_List;
+ goto Leave;
end if;
-- For access subprogram, freeze types of all formals, the return
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
- Ghost_Mode := Save_Ghost_Mode;
- return Result;
+ goto Leave;
end if;
-- Some special processing for non-generic types to complete
Set_Sloc (F_Node, Loc);
else
- F_Node := New_Freeze_Node;
+ F_Node := New_Node (N_Freeze_Entity, Loc);
Set_Freeze_Node (E, F_Node);
Set_Access_Types_To_Process (F_Node, No_Elist);
Set_TSS_Elist (F_Node, No_Elist);
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
return Result;
end Freeze_Entity;
with Namet; use Namet;
with Nlists; use Nlists;
with Nmake; use Nmake;
-with Opt; use Opt;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Disp; use Sem_Disp;
-----------------------
function Ghost_Entity (N : Node_Id) return Entity_Id;
- -- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
- -- a reference to a Ghost entity. Return Empty if there is no such entity.
+ -- Find the entity of a reference to a Ghost entity. Return Empty if there
+ -- is no such entity.
+
+ procedure Install_Ghost_Mode (Mode : Name_Id);
+ -- Install a specific Ghost mode denoted by Mode by setting global variable
+ -- Ghost_Mode.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
- -- Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
- -- declaration or body N is subject to aspect or pragma Ghost. Use this
- -- routine in cases where [source] pragma Ghost has not been analyzed yet,
- -- but the context needs to establish the "ghostness" of N.
+ -- Determine whether declaration or body N is subject to aspect or pragma
+ -- Ghost. This routine must be used in cases where pragma Ghost has not
+ -- been analyzed yet, but the context needs to establish the "ghostness"
+ -- of N.
+
+ procedure Mark_Ghost_Declaration_Or_Body
+ (N : Node_Id;
+ Mode : Name_Id);
+ -- Mark the defining entity of declaration or body N as Ghost depending on
+ -- mode Mode. Mark all formals parameters when N denotes a subprogram or a
+ -- body.
procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
- -- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
- -- Signal all enclosing scopes that they now contain ignored Ghost code.
- -- Add the compilation unit containing N to table Ignored_Ghost_Units for
- -- post processing.
+ -- Signal all enclosing scopes that they now contain at least one ignored
+ -- Ghost node denoted by N. Add the compilation unit containing N to table
+ -- Ignored_Ghost_Units for post processing.
----------------------------
-- Add_Ignored_Ghost_Unit --
----------------------------
procedure Check_Ghost_Completion
- (Partial_View : Entity_Id;
- Full_View : Entity_Id)
+ (Prev_Id : Entity_Id;
+ Compl_Id : Entity_Id)
is
Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
+ -- Nothing to do if one of the views is missing
+
+ if No (Prev_Id) or else No (Compl_Id) then
+ null;
+
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(14)).
- if Is_Checked_Ghost_Entity (Partial_View)
+ elsif Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
then
- Error_Msg_Sloc := Sloc (Full_View);
+ Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
- Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
- Error_Msg_N ("\& completed # with ghost policy `Ignore`",
- Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id);
+ Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);
- elsif Is_Ignored_Ghost_Entity (Partial_View)
+ elsif Is_Ignored_Ghost_Entity (Prev_Id)
and then Policy = Name_Check
then
- Error_Msg_Sloc := Sloc (Full_View);
+ Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
- Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
- Error_Msg_N ("\& completed # with ghost policy `Check`",
- Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id);
+ Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
end if;
end Check_Ghost_Completion;
function Is_OK_Declaration (Decl : Node_Id) return Boolean;
-- Determine whether node Decl is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Decl must either
- -- 1) Be subject to pragma Ghost
- -- 2) Rename a Ghost entity
+ --
+ -- * Define a Ghost entity
+ --
+ -- * Be subject to pragma Ghost
function Is_OK_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether node Prag is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Prag must either
- -- 1) Be an assertion expression pragma
- -- 2) Denote pragma Global, Depends, Initializes, Refined_Global,
- -- Refined_Depends or Refined_State
- -- 3) Specify an aspect of a Ghost entity
- -- 4) Contain a reference to a Ghost entity
+ --
+ -- * Be an assertion expression pragma
+ --
+ -- * Denote pragma Global, Depends, Initializes, Refined_Global,
+ -- Refined_Depends or Refined_State.
+ --
+ -- * Specify an aspect of a Ghost entity
+ --
+ -- * Contain a reference to a Ghost entity
function Is_OK_Statement (Stmt : Node_Id) return Boolean;
-- Determine whether node Stmt is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Stmt must either
- -- 1) Denote a call to a Ghost procedure
- -- 2) Denote an assignment statement whose target is Ghost
+ --
+ -- * Denote a procedure call to a Ghost procedure
+ --
+ -- * Denote an assignment statement whose target is Ghost
-----------------------
-- Is_OK_Declaration --
-- Determine whether node N appears in the profile of a subprogram
-- body.
- function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
- -- Determine whether node Ren_Decl denotes a renaming declaration
- -- with a Ghost name.
-
--------------------------------
-- In_Subprogram_Body_Profile --
--------------------------------
and then Nkind (Parent (Spec)) = N_Subprogram_Body;
end In_Subprogram_Body_Profile;
- -----------------------
- -- Is_Ghost_Renaming --
- -----------------------
-
- function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
- Nam_Id : Entity_Id;
-
- begin
- if Is_Renaming_Declaration (Ren_Decl) then
- Nam_Id := Ghost_Entity (Name (Ren_Decl));
-
- return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
- end if;
-
- return False;
- end Is_Ghost_Renaming;
-
-- Local variables
Subp_Decl : Node_Id;
-- Start of processing for Is_OK_Declaration
begin
- if Is_Declaration (Decl) then
-
- -- A renaming declaration is Ghost when it renames a Ghost
- -- entity.
-
- if Is_Ghost_Renaming (Decl) then
- return True;
-
- -- The declaration may not have been analyzed yet, determine
- -- whether it is subject to pragma Ghost.
-
- elsif Is_Subject_To_Ghost (Decl) then
- return True;
- end if;
+ if Is_Ghost_Declaration (Decl) then
+ return True;
-- Special cases
-- OK as long as the initial declaration is Ghost.
if Nkind (Subp_Decl) = N_Expression_Function then
- return Is_Subject_To_Ghost (Subp_Decl);
+ return Is_Ghost_Declaration (Subp_Decl);
end if;
end if;
-- Local variables
- Arg : Node_Id;
- Arg_Id : Entity_Id;
Prag_Id : Pragma_Id;
Prag_Nam : Name_Id;
Name_Refined_State)
then
return True;
-
- -- Otherwise a normal pragma is Ghost when it encloses a Ghost
- -- name (SPARK RM 6.9(3)).
-
- else
- Arg := First (Pragma_Argument_Associations (Prag));
- while Present (Arg) loop
- Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
-
- if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
- return True;
- end if;
-
- Next (Arg);
- end loop;
end if;
end if;
---------------------
function Is_OK_Statement (Stmt : Node_Id) return Boolean is
- Nam_Id : Entity_Id;
-
begin
- -- An assignment statement or a procedure call is Ghost when the
- -- name denotes a Ghost entity.
+ -- An assignment statement is Ghost when the target is a Ghost
+ -- entity.
- if Nkind_In (Stmt, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- Nam_Id := Ghost_Entity (Name (Stmt));
+ if Nkind (Stmt) = N_Assignment_Statement then
+ return Is_Ghost_Assignment (Stmt);
- return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
+ -- A procedure call is Ghost when it calls a Ghost procedure
+
+ elsif Nkind (Stmt) = N_Procedure_Call_Statement then
+ return Is_Ghost_Procedure_Call (Stmt);
-- Special cases
Ref : Node_Id;
begin
- -- When the reference extracts a subcomponent, recover the related
+ -- When the reference denotes a subcomponent, recover the related
-- object (SPARK RM 6.9(1)).
Ref := N;
Ignored_Ghost_Units.Init;
end Initialize;
+ ------------------------
+ -- Install_Ghost_Mode --
+ ------------------------
+
+ procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
+ begin
+ Ghost_Mode := Mode;
+ end Install_Ghost_Mode;
+
+ procedure Install_Ghost_Mode (Mode : Name_Id) is
+ begin
+ if Mode = Name_Check then
+ Ghost_Mode := Check;
+
+ elsif Mode = Name_Ignore then
+ Ghost_Mode := Ignore;
+
+ elsif Mode = Name_None then
+ Ghost_Mode := None;
+ end if;
+ end Install_Ghost_Mode;
+
+ -------------------------
+ -- Is_Ghost_Assignment --
+ -------------------------
+
+ function Is_Ghost_Assignment (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- An assignment statement is Ghost when its target denotes a Ghost
+ -- entity.
+
+ if Nkind (N) = N_Assignment_Statement then
+ Id := Ghost_Entity (Name (N));
+
+ return Present (Id) and then Is_Ghost_Entity (Id);
+ end if;
+
+ return False;
+ end Is_Ghost_Assignment;
+
+ --------------------------
+ -- Is_Ghost_Declaration --
+ --------------------------
+
+ function Is_Ghost_Declaration (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- A declaration is Ghost when it elaborates a Ghost entity or is
+ -- subject to pragma Ghost.
+
+ if Is_Declaration (N) then
+ Id := Defining_Entity (N);
+
+ return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N);
+ end if;
+
+ return False;
+ end Is_Ghost_Declaration;
+
+ ---------------------
+ -- Is_Ghost_Pragma --
+ ---------------------
+
+ function Is_Ghost_Pragma (N : Node_Id) return Boolean is
+ begin
+ return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N);
+ end Is_Ghost_Pragma;
+
+ -----------------------------
+ -- Is_Ghost_Procedure_Call --
+ -----------------------------
+
+ function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is
+ Id : Entity_Id;
+
+ begin
+ -- A procedure call is Ghost when it invokes a Ghost procedure
+
+ if Nkind (N) = N_Procedure_Call_Statement then
+ Id := Ghost_Entity (Name (N));
+
+ return Present (Id) and then Is_Ghost_Entity (Id);
+ end if;
+
+ return False;
+ end Is_Ghost_Procedure_Call;
+
-------------------------
-- Is_Subject_To_Ghost --
-------------------------
Ignored_Ghost_Units.Release;
end Lock;
+ -----------------------------------
+ -- Mark_And_Set_Ghost_Assignment --
+ -----------------------------------
+
+ procedure Mark_And_Set_Ghost_Assignment
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Id : Entity_Id;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- An assignment statement becomes Ghost when its target denotes a Ghost
+ -- object. Install the Ghost mode of the target.
+
+ Id := Ghost_Entity (Name (N));
+
+ if Present (Id) then
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end if;
+ end Mark_And_Set_Ghost_Assignment;
+
-----------------------------
- -- Mark_Full_View_As_Ghost --
+ -- Mark_And_Set_Ghost_Body --
-----------------------------
- procedure Mark_Full_View_As_Ghost
- (Priv_Typ : Entity_Id;
- Full_Typ : Entity_Id)
+ procedure Mark_And_Set_Ghost_Body
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
is
- Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+ Policy : Name_Id := No_Name;
begin
- if Is_Checked_Ghost_Entity (Priv_Typ) then
- Set_Is_Checked_Ghost_Entity (Full_Typ);
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- A body becomes Ghost when it is subject to aspect or pragma Ghost
- elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
- Set_Is_Ignored_Ghost_Entity (Full_Typ);
- Set_Is_Ignored_Ghost_Node (Full_Decl);
- Propagate_Ignored_Ghost_Code (Full_Decl);
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- A body declared within a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- Inherit the "ghostness" of the previous declaration when the body
+ -- acts as a completion.
+
+ elsif Present (Spec_Id) then
+ if Is_Checked_Ghost_Entity (Spec_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Spec_Id) then
+ Policy := Name_Ignore;
+ end if;
end if;
- end Mark_Full_View_As_Ghost;
- --------------------------
- -- Mark_Pragma_As_Ghost --
- --------------------------
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
+
+ Check_Ghost_Completion
+ (Prev_Id => Spec_Id,
+ Compl_Id => Body_Id);
+
+ -- Mark the body as its formals as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Body;
+
+ -----------------------------------
+ -- Mark_And_Set_Ghost_Completion --
+ -----------------------------------
- procedure Mark_Pragma_As_Ghost
- (Prag : Node_Id;
- Context_Id : Entity_Id)
+ procedure Mark_And_Set_Ghost_Completion
+ (N : Node_Id;
+ Prev_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
is
+ Compl_Id : constant Entity_Id := Defining_Entity (N);
+ Policy : Name_Id := No_Name;
+
begin
- if Is_Checked_Ghost_Entity (Context_Id) then
- Set_Is_Ghost_Pragma (Prag);
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- A completion elaborated in a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ if Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- The completion becomes Ghost when its initial declaration is also
+ -- Ghost.
+
+ elsif Is_Checked_Ghost_Entity (Prev_Id) then
+ Policy := Name_Check;
- elsif Is_Ignored_Ghost_Entity (Context_Id) then
- Set_Is_Ghost_Pragma (Prag);
- Set_Is_Ignored_Ghost_Node (Prag);
- Propagate_Ignored_Ghost_Code (Prag);
+ elsif Is_Ignored_Ghost_Entity (Prev_Id) then
+ Policy := Name_Ignore;
end if;
- end Mark_Pragma_As_Ghost;
- ----------------------------
- -- Mark_Renaming_As_Ghost --
- ----------------------------
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(14)).
+
+ Check_Ghost_Completion
+ (Prev_Id => Prev_Id,
+ Compl_Id => Compl_Id);
+
+ -- Mark the completion as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Completion;
- procedure Mark_Renaming_As_Ghost
- (Ren_Decl : Node_Id;
- Nam_Id : Entity_Id)
+ ------------------------------------
+ -- Mark_And_Set_Ghost_Declaration --
+ ------------------------------------
+
+ procedure Mark_And_Set_Ghost_Declaration
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
is
- Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
+ Par_Id : Entity_Id;
+ Policy : Name_Id := No_Name;
begin
- if Is_Checked_Ghost_Entity (Nam_Id) then
- Set_Is_Checked_Ghost_Entity (Ren_Id);
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- A declaration becomes Ghost when it is subject to aspect or pragma
+ -- Ghost.
+
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- A declaration elaborated in a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- A child package or subprogram declaration becomes Ghost when its
+ -- parent is Ghost (SPARK RM 6.9(2)).
- elsif Is_Ignored_Ghost_Entity (Nam_Id) then
- Set_Is_Ignored_Ghost_Entity (Ren_Id);
- Set_Is_Ignored_Ghost_Node (Ren_Decl);
- Propagate_Ignored_Ghost_Code (Ren_Decl);
+ elsif Nkind_In (N, N_Generic_Function_Renaming_Declaration,
+ N_Generic_Package_Declaration,
+ N_Generic_Package_Renaming_Declaration,
+ N_Generic_Procedure_Renaming_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Package_Declaration,
+ N_Package_Renaming_Declaration,
+ N_Subprogram_Declaration,
+ N_Subprogram_Renaming_Declaration)
+ and then Present (Parent_Spec (N))
+ then
+ Par_Id := Defining_Entity (Unit (Parent_Spec (N)));
+
+ if Is_Checked_Ghost_Entity (Par_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Par_Id) then
+ Policy := Name_Ignore;
+ end if;
+ end if;
+
+ -- Mark the declaration and its formals as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Declaration;
+
+ --------------------------------------
+ -- Mark_And_Set_Ghost_Instantiation --
+ --------------------------------------
+
+ procedure Mark_And_Set_Ghost_Instantiation
+ (N : Node_Id;
+ Gen_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Policy : Name_Id := No_Name;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- An instantiation becomes Ghost when it is subject to pragma Ghost
+
+ if Is_Subject_To_Ghost (N) then
+ Policy := Policy_In_Effect (Name_Ghost);
+
+ -- An instantiation declaration within a Ghost region is automatically
+ -- Ghost (SPARK RM 6.9(2)).
+
+ elsif Ghost_Mode = Check then
+ Policy := Name_Check;
+
+ elsif Ghost_Mode = Ignore then
+ Policy := Name_Ignore;
+
+ -- Inherit the "ghostness" of the generic unit
+
+ elsif Is_Checked_Ghost_Entity (Gen_Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Gen_Id) then
+ Policy := Name_Ignore;
+ end if;
+
+ -- Mark the instantiation as Ghost
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+
+ -- Install the appropriate Ghost mode
+
+ Install_Ghost_Mode (Policy);
+ end Mark_And_Set_Ghost_Instantiation;
+
+ ---------------------------------------
+ -- Mark_And_Set_Ghost_Procedure_Call --
+ ---------------------------------------
+
+ procedure Mark_And_Set_Ghost_Procedure_Call
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ Id : Entity_Id;
+
+ begin
+ -- Save the previous Ghost mode in effect
+
+ Mode := Ghost_Mode;
+
+ -- A procedure call becomes Ghost when the procedure being invoked is
+ -- Ghost. Install the Ghost mode of the procedure.
+
+ Id := Ghost_Entity (Name (N));
+
+ if Present (Id) then
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end if;
+ end Mark_And_Set_Ghost_Procedure_Call;
+
+ ------------------------------------
+ -- Mark_Ghost_Declaration_Or_Body --
+ ------------------------------------
+
+ procedure Mark_Ghost_Declaration_Or_Body
+ (N : Node_Id;
+ Mode : Name_Id)
+ is
+ Id : constant Entity_Id := Defining_Entity (N);
+
+ Mark_Formals : Boolean := False;
+ Param : Node_Id;
+ Param_Id : Entity_Id;
+
+ begin
+ -- Mark the related node and its entity
+
+ if Mode = Name_Check then
+ Mark_Formals := True;
+ Set_Is_Checked_Ghost_Entity (Id);
+
+ elsif Mode = Name_Ignore then
+ Mark_Formals := True;
+ Set_Is_Ignored_Ghost_Entity (Id);
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+
+ -- Mark all formal parameters when the related node denotes a subprogram
+ -- or a body. The traversal is performed via the specification because
+ -- the related subprogram or body may be unanalyzed.
+
+ -- ??? could extra formal parameters cause a Ghost leak?
+
+ if Mark_Formals
+ and then Nkind_In (N, N_Abstract_Subprogram_Declaration,
+ N_Formal_Abstract_Subprogram_Declaration,
+ N_Formal_Concrete_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub,
+ N_Subprogram_Declaration,
+ N_Subprogram_Renaming_Declaration)
+ then
+ Param := First (Parameter_Specifications (Specification (N)));
+ while Present (Param) loop
+ Param_Id := Defining_Entity (Param);
+
+ if Mode = Name_Check then
+ Set_Is_Checked_Ghost_Entity (Param_Id);
+
+ elsif Mode = Name_Ignore then
+ Set_Is_Ignored_Ghost_Entity (Param_Id);
+ end if;
+
+ Next (Param);
+ end loop;
+ end if;
+ end Mark_Ghost_Declaration_Or_Body;
+
+ -----------------------
+ -- Mark_Ghost_Pragma --
+ -----------------------
+
+ procedure Mark_Ghost_Pragma
+ (N : Node_Id;
+ Id : Entity_Id)
+ is
+ begin
+ -- A pragma becomes Ghost when it encloses a Ghost entity or relates to
+ -- a Ghost entity.
+
+ if Is_Checked_Ghost_Entity (Id) then
+ Set_Is_Checked_Ghost_Pragma (N);
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Set_Is_Ignored_Ghost_Pragma (N);
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end Mark_Ghost_Pragma;
+
+ -------------------------
+ -- Mark_Ghost_Renaming --
+ -------------------------
+
+ procedure Mark_Ghost_Renaming
+ (N : Node_Id;
+ Id : Entity_Id)
+ is
+ Policy : Name_Id := No_Name;
+
+ begin
+ -- A renaming becomes Ghost when it renames a Ghost entity
+
+ if Is_Checked_Ghost_Entity (Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Policy := Name_Ignore;
end if;
- end Mark_Renaming_As_Ghost;
+
+ Mark_Ghost_Declaration_Or_Body (N, Policy);
+ end Mark_Ghost_Renaming;
----------------------------------
-- Propagate_Ignored_Ghost_Code --
Scop : Entity_Id;
begin
- -- Traverse the parent chain looking for blocks, packages and
+ -- Traverse the parent chain looking for blocks, packages, and
-- subprograms or their respective bodies.
Nod := Parent (N);
Prune (N);
return Skip;
- -- A freeze node for an ignored ghost entity must be pruned as
- -- well, to prevent meaningless references in the back end.
-
- -- ??? the freeze node itself should be ignored ghost
-
- elsif Nkind (N) = N_Freeze_Entity
- and then Is_Ignored_Ghost_Entity (Entity (N))
- then
- Prune (N);
- return Skip;
-
-- Scoping constructs such as blocks, packages, subprograms and
-- bodies offer some flexibility with respect to pruning.
end loop;
end Remove_Ignored_Ghost_Code;
+ ------------------------
+ -- Restore_Ghost_Mode --
+ ------------------------
+
+ procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type) is
+ begin
+ Ghost_Mode := Mode;
+ end Restore_Ghost_Mode;
+
--------------------
-- Set_Ghost_Mode --
--------------------
- procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
- procedure Set_From_Entity (Ent_Id : Entity_Id);
- -- Set the value of global variable Ghost_Mode depending on the mode of
- -- entity Ent_Id.
-
- procedure Set_From_Policy;
- -- Set the value of global variable Ghost_Mode depending on the current
- -- Ghost policy in effect.
-
- ---------------------
- -- Set_From_Entity --
- ---------------------
-
- procedure Set_From_Entity (Ent_Id : Entity_Id) is
- begin
- Set_Ghost_Mode_From_Entity (Ent_Id);
-
- if Is_Ignored_Ghost_Entity (Ent_Id) then
- Set_Is_Ignored_Ghost_Node (N);
- Propagate_Ignored_Ghost_Code (N);
- end if;
- end Set_From_Entity;
+ procedure Set_Ghost_Mode
+ (N : Node_Or_Entity_Id;
+ Mode : out Ghost_Mode_Type)
+ is
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+ -- Install the Ghost mode of entity Id
- ---------------------
- -- Set_From_Policy --
- ---------------------
-
- procedure Set_From_Policy is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+ --------------------------------
+ -- Set_Ghost_Mode_From_Entity --
+ --------------------------------
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
begin
- if Policy = Name_Check then
- Ghost_Mode := Check;
-
- elsif Policy = Name_Ignore then
- Ghost_Mode := Ignore;
-
- Set_Is_Ignored_Ghost_Node (N);
- Propagate_Ignored_Ghost_Code (N);
+ if Is_Checked_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Check);
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Install_Ghost_Mode (Ignore);
+ else
+ Install_Ghost_Mode (None);
end if;
- end Set_From_Policy;
+ end Set_Ghost_Mode_From_Entity;
-- Local variables
- Nam_Id : Entity_Id;
+ Id : Entity_Id;
-- Start of processing for Set_Ghost_Mode
begin
- -- The input node denotes one of the many declaration kinds that may be
- -- subject to pragma Ghost.
-
- if Is_Declaration (N) then
- if Is_Subject_To_Ghost (N) then
- Set_From_Policy;
+ -- Save the previous Ghost mode in effect
- -- The declaration denotes the completion of a deferred constant,
- -- pragma Ghost appears on the partial declaration.
+ Mode := Ghost_Mode;
- elsif Nkind (N) = N_Object_Declaration
- and then Constant_Present (N)
- and then Present (Id)
- then
- Set_From_Entity (Id);
+ -- The Ghost mode of an assignment statement depends on the Ghost mode
+ -- of the target.
- -- The declaration denotes the full view of a private type, pragma
- -- Ghost appears on the partial declaration.
+ if Nkind (N) = N_Assignment_Statement then
+ Id := Ghost_Entity (Name (N));
- elsif Nkind (N) = N_Full_Type_Declaration
- and then Is_Private_Type (Defining_Entity (N))
- and then Present (Id)
- then
- Set_From_Entity (Id);
+ if Present (Id) then
+ Set_Ghost_Mode_From_Entity (Id);
end if;
- -- The input denotes an assignment or a procedure call. In this case
- -- the Ghost mode is dictated by the name of the construct.
+ -- The Ghost mode of a body or a declaration depends on the Ghost mode
+ -- of its defining entity.
- elsif Nkind_In (N, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- Nam_Id := Ghost_Entity (Name (N));
+ elsif Is_Body (N) or else Is_Declaration (N) then
+ Set_Ghost_Mode_From_Entity (Defining_Entity (N));
- if Present (Nam_Id) then
- Set_From_Entity (Nam_Id);
- end if;
+ -- The Ghost mode of an entity depends on the entity itself
- -- The input denotes a package or subprogram body
+ elsif Nkind (N) in N_Entity then
+ Set_Ghost_Mode_From_Entity (N);
- elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
- if (Present (Id) and then Is_Ghost_Entity (Id))
- or else Is_Subject_To_Ghost (N)
- then
- Set_From_Policy;
- end if;
+ -- The Ghost mode of a [generic] freeze node depends on the Ghost mode
+ -- of the entity being frozen.
+
+ elsif Nkind_In (N, N_Freeze_Entity, N_Freeze_Generic_Entity) then
+ Set_Ghost_Mode_From_Entity (Entity (N));
- -- The input denotes a pragma
+ -- The Ghost mode of a pragma depends on the associated entity. The
+ -- property is encoded in the pragma itself.
- elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
- if Is_Ignored_Ghost_Node (N) then
- Ghost_Mode := Ignore;
+ elsif Nkind (N) = N_Pragma then
+ if Is_Checked_Ghost_Pragma (N) then
+ Install_Ghost_Mode (Check);
+ elsif Is_Ignored_Ghost_Pragma (N) then
+ Install_Ghost_Mode (Ignore);
else
- Ghost_Mode := Check;
+ Install_Ghost_Mode (None);
end if;
- -- The input denotes a freeze node
+ -- The Ghost mode of a procedure call depends on the Ghost mode of the
+ -- procedure being invoked.
- elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
- Set_From_Entity (Id);
- end if;
- end Set_Ghost_Mode;
+ elsif Nkind (N) = N_Procedure_Call_Statement then
+ Id := Ghost_Entity (Name (N));
- --------------------------------
- -- Set_Ghost_Mode_From_Entity --
- --------------------------------
-
- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
- begin
- if Is_Checked_Ghost_Entity (Id) then
- Ghost_Mode := Check;
- elsif Is_Ignored_Ghost_Entity (Id) then
- Ghost_Mode := Ignore;
+ if Present (Id) then
+ Set_Ghost_Mode_From_Entity (Id);
+ end if;
end if;
- end Set_Ghost_Mode_From_Entity;
+ end Set_Ghost_Mode;
-------------------------
-- Set_Is_Ghost_Entity --
-- --
-- S p e c --
-- --
--- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2014-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- This package contains routines that deal with the static and runtime
-- semantics of Ghost entities.
+with Opt; use Opt;
with Types; use Types;
package Ghost is
-- post processing.
procedure Check_Ghost_Completion
- (Partial_View : Entity_Id;
- Full_View : Entity_Id);
- -- Verify that the Ghost policy of a full view or a completion is the same
- -- as the Ghost policy of the partial view. Emit an error if this is not
- -- the case.
-
- procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
+ (Prev_Id : Entity_Id;
+ Compl_Id : Entity_Id);
+ -- Verify that the Ghost policy of initial entity Prev_Id is compatible
+ -- with the Ghost policy of completing entity Compl_Id. Emit an error if
+ -- this is not the case.
+
+ procedure Check_Ghost_Context
+ (Ghost_Id : Entity_Id;
+ Ghost_Ref : Node_Id);
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
procedure Initialize;
-- Initialize internal tables
- procedure Lock;
- -- Lock internal tables before calling backend
+ procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
+ -- Set the value of global variable Ghost_Mode depending on the Ghost
+ -- policy denoted by Mode.
- procedure Mark_Full_View_As_Ghost
- (Priv_Typ : Entity_Id;
- Full_Typ : Entity_Id);
- -- Set all Ghost-related attributes of type Full_Typ depending on the Ghost
- -- mode of incomplete or private type Priv_Typ.
+ function Is_Ghost_Assignment (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes an assignment statement whose
+ -- target is a Ghost entity.
- procedure Mark_Pragma_As_Ghost
- (Prag : Node_Id;
- Context_Id : Entity_Id);
- -- Set all Ghost-related attributes of pragma Prag if its context denoted
- -- by Id is a Ghost entity.
+ function Is_Ghost_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a declaration which defines
+ -- a Ghost entity.
- procedure Mark_Renaming_As_Ghost
- (Ren_Decl : Node_Id;
- Nam_Id : Entity_Id);
- -- Set all Ghost-related attributes of renaming declaration Ren_Decl if its
- -- renamed name denoted by Nam_Id is a Ghost entity.
+ function Is_Ghost_Pragma (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a pragma which encloses a
+ -- Ghost entity or is associated with a Ghost entity.
- procedure Remove_Ignored_Ghost_Code;
- -- Remove all code marked as ignored Ghost from the trees of all qualifying
- -- units (SPARK RM 6.9(4)).
- --
- -- WARNING: this is a separate front end pass, care should be taken to keep
- -- it optimized.
+ function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a procedure call invoking a
+ -- Ghost procedure.
- procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty);
- -- Set the value of global variable Ghost_Mode depending on the following
- -- scenarios:
+ procedure Lock;
+ -- Lock internal tables before calling backend
+
+ procedure Mark_And_Set_Ghost_Assignment
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark assignment statement N as Ghost when:
+ --
+ -- * The left hand side denotes a Ghost entity
+ --
+ -- Install the Ghost mode of the assignment statement. Mode is the Ghost
+ -- mode in effect prior to processing the assignment. This routine starts
+ -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Body
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark package or subprogram body N as Ghost when:
+ --
+ -- * The body is subject to pragma Ghost
+ --
+ -- * The body completes a previous declaration whose spec denoted by
+ -- Spec_Id is a Ghost entity.
+ --
+ -- * The body appears within a Ghost region
--
- -- If N is a declaration, determine whether N is subject to pragma Ghost.
- -- If this is the case, the Ghost_Mode is set based on the current Ghost
- -- policy in effect. Special cases:
+ -- Install the Ghost mode of the body. Mode is the Ghost mode prior to
+ -- processing the body. This routine starts a Ghost region and must be
+ -- used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Completion
+ (N : Node_Id;
+ Prev_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark completion N of a deferred constant or private type [extension]
+ -- Ghost when:
--
- -- N is the completion of a deferred constant, the Ghost_Mode is set
- -- based on the mode of partial declaration entity denoted by Id.
+ -- * The entity of the previous declaration denoted by Prev_Id is Ghost
--
- -- N is the full view of a private type, the Ghost_Mode is set based
- -- on the mode of the partial declaration entity denoted by Id.
+ -- * The completion appears within a Ghost region
--
- -- If N is an assignment statement or a procedure call, the Ghost_Mode is
- -- set based on the mode of the name.
+ -- Install the Ghost mode of the completion. Mode is the Ghost mode prior
+ -- to processing the completion. This routine starts a Ghost region and
+ -- must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Declaration
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark declaration N as Ghost when:
--
- -- If N denotes a package or a subprogram body, the Ghost_Mode is set to
- -- the current Ghost policy in effect if the body is subject to Ghost or
- -- the corresponding spec denoted by Id is a Ghost entity.
+ -- * The declaration is subject to pragma Ghost
--
- -- If N is a pragma, the Ghost_Mode is set based on the mode of the
- -- pragma.
+ -- * The declaration denotes a child package or subprogram and the parent
+ -- is a Ghost unit.
--
- -- If N is a freeze node, the Global_Mode is set based on the mode of
- -- entity Id.
+ -- * The declaration appears within a Ghost region
--
- -- WARNING: the caller must save and restore the value of Ghost_Mode in a
- -- a stack-like fasion as this routine may override the existing value.
+ -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior
+ -- to processing the declaration. This routine starts a Ghost region and
+ -- must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Instantiation
+ (N : Node_Id;
+ Gen_Id : Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark instantiation N as Ghost when:
+ --
+ -- * The instantiation is subject to pragma Ghost
+ --
+ -- * The generic template denoted by Gen_Id is Ghost
+ --
+ -- * The instantiation appears within a Ghost region
+ --
+ -- Install the Ghost mode of the instantiation. Mode is the Ghost mode
+ -- prior to processing the instantiation. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_And_Set_Ghost_Procedure_Call
+ (N : Node_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Mark procedure call N as Ghost when:
+ --
+ -- * The procedure being invoked is a Ghost entity
+ --
+ -- Install the Ghost mode of the procedure call. Mode is the Ghost mode
+ -- prior to processing the procedure call. This routine starts a Ghost
+ -- region and must be used in conjunction with Restore_Ghost_Mode.
+
+ procedure Mark_Ghost_Pragma
+ (N : Node_Id;
+ Id : Entity_Id);
+ -- Mark pragma N as Ghost when:
+ --
+ -- * The pragma encloses Ghost entity Id
+ --
+ -- * The pragma is associated with Ghost entity Id
- procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
- -- Set the valye of global variable Ghost_Mode depending on the mode of
- -- entity Id.
+ procedure Mark_Ghost_Renaming
+ (N : Node_Id;
+ Id : Entity_Id);
+ -- Mark renaming declaration N as Ghost when:
--
- -- WARNING: the caller must save and restore the value of Ghost_Mode in a
- -- a stack-like fasion as this routine may override the existing value.
+ -- * Renamed entity Id denotes a Ghost entity
+
+ procedure Remove_Ignored_Ghost_Code;
+ -- Remove all code marked as ignored Ghost from the trees of all qualifying
+ -- units (SPARK RM 6.9(4)).
+ --
+ -- WARNING: this is a separate front end pass, care should be taken to keep
+ -- it optimized.
+
+ procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type);
+ -- Terminate a Ghost region by restoring the Ghost mode prior to the
+ -- region denoted by Mode. This routine must be used in conjunction
+ -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode.
+
+ procedure Set_Ghost_Mode
+ (N : Node_Or_Entity_Id;
+ Mode : out Ghost_Mode_Type);
+ -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior
+ -- to processing the node. This routine starts a Ghost region and must be
+ -- used in conjunction with Restore_Ghost_Mode.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current
-------------
procedure Analyze (N : Node_Id) is
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
begin
Debug_A_Entry ("analyzing ", N);
-- marked as Ghost.
if Is_Declaration (N) then
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Declaration (N, Mode);
+ Mode_Set := True;
end if;
-- Otherwise processing depends on the node kind
Expand_SPARK_Potential_Renaming (N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze;
-- Version with check(s) suppressed
-- Set up a clean environment before analyzing
- Ghost_Mode := None;
+ Install_Ghost_Mode (None);
Outer_Generic_Scope := Empty;
Scope_Suppress := Suppress_Options;
Scope_Stack.Table
Pop_Scope;
Restore_Scope_Stack (List);
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Save_Ghost_Mode);
Style_Max_Line_Length := Save_Max_Line;
end Do_Analyze;
with Checks; use Checks;
with Einfo; use Einfo;
with Errout; use Errout;
-with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
Set_Is_Statically_Allocated (Id);
Set_Is_Pure (Id, PF);
- -- An exception declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
Set_Ekind (Id, E_Generic_Package);
Set_Etype (Id, Standard_Void_Type);
- -- A generic package declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- Analyze aspects now, so that generated pragmas appear in the
-- declarations before building and analyzing the generic copy.
Set_Etype (Id, Standard_Void_Type);
end if;
- -- A generic subprogram declared within a Ghost region is rendered Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- For a library unit, we have reconstructed the entity for the unit,
-- and must reset it in the library tables. We also make sure that
-- Body_Required is set properly in the original compilation unit node.
-- Local declarations
+ Mode : Ghost_Mode_Type;
+
Vis_Prims_List : Elist_Id := No_Elist;
-- List of primitives made temporarily visible in the instantiation
-- to match the visibility of the formal type
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A package instantiation is Ghost when it is subject to pragma Ghost
+ -- or the generic template is Ghost. Set the mode now to ensure that
+ -- any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
+
-- Verify that it is the name of a generic package
-- A visibility glitch: if the instance is a child unit and the generic
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Restore_Ghost_Mode (Mode);
+
exception
when Instantiation_Error =>
if Parent_Installed then
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
Style_Check := Save_Style_Check;
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Package_Instantiation;
--------------------------
-- Local variables
+ Mode : Ghost_Mode_Type;
+
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
-- Save flag Ignore_Pragma_SPARK_Mode for restore on exit
Check_Generic_Child_Unit (Gen_Id, Parent_Installed);
Gen_Unit := Entity (Gen_Id);
+ -- A subprogram instantiation is Ghost when it is subject to pragma
+ -- Ghost or the generic template is Ghost. Set the mode now to ensure
+ -- that any nodes generated during analysis and expansion are marked as
+ -- Ghost.
+
+ Mark_And_Set_Ghost_Instantiation (N, Gen_Unit, Mode);
+
Generate_Reference (Gen_Unit, Gen_Id);
if Nkind (Gen_Id) = N_Identifier
if Etype (Gen_Unit) = Any_Type then
Restore_Env;
- return;
+ goto Leave;
end if;
-- Verify that it is a generic subprogram of the right kind, and that
Error_Msg_NE
("access parameter& is controlling,", N, Formal);
Error_Msg_NE
- ("\corresponding parameter of & must be "
- & "explicitly null-excluding", N, Gen_Id);
+ ("\corresponding parameter of & must be explicitly "
+ & "null-excluding", N, Gen_Id);
end if;
Next_Formal (Formal);
Analyze_Aspect_Specifications (N, Act_Decl_Id);
end if;
+ Restore_Ghost_Mode (Mode);
+
exception
when Instantiation_Error =>
if Parent_Installed then
Ignore_Pragma_SPARK_Mode := Save_IPSM;
SPARK_Mode := Save_SM;
SPARK_Mode_Pragma := Save_SMP;
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Subprogram_Instantiation;
-------------------------
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
+ Act_Spec : constant Node_Id := Specification (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
-
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Spec : constant Node_Id := Specification (Act_Decl);
- Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec);
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
Save_Style_Check : constant Boolean := Style_Check;
- Act_Body : Node_Id;
- Act_Body_Id : Entity_Id;
- Act_Body_Name : Node_Id;
- Gen_Body : Node_Id;
- Gen_Body_Id : Node_Id;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
-
- Parent_Installed : Boolean := False;
-
- Vis_Prims_List : Elist_Id := No_Elist;
- -- List of primitives made temporarily visible in the instantiation
- -- to match the visibility of the formal type
-
procedure Check_Initialized_Types;
-- In a generic package body, an entity of a generic private type may
-- appear uninitialized. This is suspicious, unless the actual is a
end loop;
end Check_Initialized_Types;
+ -- Local variables
+
+ Act_Body : Node_Id;
+ Act_Body_Id : Entity_Id;
+ Act_Body_Name : Node_Id;
+ Gen_Body : Node_Id;
+ Gen_Body_Id : Node_Id;
+ Mode : Ghost_Mode_Type;
+ Par_Ent : Entity_Id := Empty;
+ Par_Vis : Boolean := False;
+
+ Parent_Installed : Boolean := False;
+
+ Vis_Prims_List : Elist_Id := No_Elist;
+ -- List of primitives made temporarily visible in the instantiation
+ -- to match the visibility of the formal type.
+
-- Start of processing for Instantiate_Package_Body
begin
return;
end if;
+ -- The package being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id, Mode);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
if not Unit_Requires_Body (Defining_Entity (Gen_Decl))
and then Body_Optional
then
- return;
+ goto Leave;
else
Load_Parent_Of_Generic
(Inst_Node, Specification (Gen_Decl), Body_Optional);
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Instantiate_Package_Body;
---------------------------------
Body_Optional : Boolean := False)
is
Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Decl);
Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
Gen_Id : constant Node_Id := Name (Inst_Node);
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Act_Decl_Id : constant Entity_Id :=
- Defining_Unit_Name (Specification (Act_Decl));
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
Pack_Id : constant Entity_Id :=
Defining_Unit_Name (Parent (Act_Decl));
Act_Body_Id : Entity_Id;
Gen_Body : Node_Id;
Gen_Body_Id : Node_Id;
+ Mode : Ghost_Mode_Type;
Pack_Body : Node_Id;
Par_Ent : Entity_Id := Empty;
Par_Vis : Boolean := False;
return;
end if;
+ -- The subprogram being instantiated may be subject to pragma Ghost. Set
+ -- the mode now to ensure that any nodes generated during instantiation
+ -- are properly marked as Ghost.
+
+ Set_Ghost_Mode (Act_Decl_Id, Mode);
+
Expander_Mode_Save_And_Set (Body_Info.Expander_Status);
-- Re-establish the state of information on which checks are suppressed.
Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit));
Set_Convention (Act_Decl_Id, Convention (Gen_Unit));
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
-- For other cases, compile the body
if Expander_Active
and then Operating_Mode = Generate_Code
then
- Error_Msg_N
- ("missing proper body for instantiation", Gen_Body);
+ Error_Msg_N ("missing proper body for instantiation", Gen_Body);
end if;
Set_Has_Completion (Act_Decl_Id);
- return;
+ goto Leave;
end if;
Save_Env (Gen_Unit, Act_Decl_Id);
and then Nkind (Parent (Inst_Node)) /= N_Compilation_Unit
then
if Body_Optional then
- return;
+ goto Leave;
elsif Ekind (Act_Decl_Id) = E_Procedure then
Act_Body :=
Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name =>
- Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
- New_Copy_List
- (Parameter_Specifications (Parent (Act_Decl_Id)))),
-
- Declarations => Empty_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List (
- Make_Raise_Program_Error (Loc,
- Reason =>
- PE_Access_Before_Elaboration))));
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
+ Parameter_Specifications =>
+ New_Copy_List
+ (Parameter_Specifications (Parent (Act_Decl_Id)))),
+
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Make_Raise_Program_Error (Loc,
+ Reason => PE_Access_Before_Elaboration))));
else
Ret_Expr :=
Make_Subprogram_Body (Loc,
Specification =>
Make_Function_Specification (Loc,
- Defining_Unit_Name =>
+ Defining_Unit_Name =>
Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
- Parameter_Specifications =>
+ Parameter_Specifications =>
New_Copy_List
(Parameter_Specifications (Parent (Act_Decl_Id))),
Result_Definition =>
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements =>
- New_List
- (Make_Simple_Return_Statement (Loc, Ret_Expr))));
+ Statements => New_List (
+ Make_Simple_Return_Statement (Loc, Ret_Expr))));
end if;
Pack_Body :=
end if;
Expander_Mode_Restore;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Instantiate_Subprogram_Body;
----------------------
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Build_Predicate_Functions
-- The related type may be subject to pragma Ghost. Set the mode now to
-- ensure that the predicate functions are properly marked as Ghost.
- Set_Ghost_Mode_From_Entity (Typ);
+ Set_Ghost_Mode (Typ, Mode);
-- Prepare to construct predicate expression
FBody : Node_Id;
begin
-
-- The predicate function is shared between views of a type
if Is_Private_Type (Typ) and then Present (Full_View (Typ)) then
Set_Predicate_Function (Full_View (Typ), SId);
end if;
- -- Mark the predicate function explicitly as Ghost because it does
- -- not come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (SId);
- end if;
-
-- Build function body
Spec :=
Set_Predicate_Function_M (Full_View (Typ), SId);
end if;
- -- Mark the predicate function explicitly as Ghost because it
- -- does not come from source.
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (SId);
- end if;
-
Spec :=
Make_Function_Specification (Loc,
Defining_Unit_Name => SId,
end;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Build_Predicate_Functions;
------------------------------------------
is
Loc : constant Source_Ptr := Sloc (Typ);
- Object_Entity : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_Internal_Name ('I'));
-
- -- The formal parameter of the function
+ Func_Decl : Node_Id;
+ Func_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
+ Spec : Node_Id;
- SId : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Typ), "Predicate"));
+ begin
+ -- The related type may be subject to pragma Ghost. Set the mode now to
+ -- ensure that the predicate functions are properly marked as Ghost.
- -- The entity for the function spec
+ Set_Ghost_Mode (Typ, Mode);
- FDecl : Node_Id;
- Spec : Node_Id;
+ Func_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Typ), "Predicate"));
- begin
Spec :=
Make_Function_Specification (Loc,
- Defining_Unit_Name => SId,
+ Defining_Unit_Name => Func_Id,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
+ Defining_Identifier => Make_Temporary (Loc, 'I'),
Parameter_Type => New_Occurrence_Of (Typ, Loc))),
Result_Definition =>
New_Occurrence_Of (Standard_Boolean, Loc));
- FDecl := Make_Subprogram_Declaration (Loc, Specification => Spec);
+ Func_Decl := Make_Subprogram_Declaration (Loc, Specification => Spec);
- Set_Ekind (SId, E_Function);
- Set_Etype (SId, Standard_Boolean);
- Set_Is_Internal (SId);
- Set_Is_Predicate_Function (SId);
- Set_Predicate_Function (Typ, SId);
+ Set_Ekind (Func_Id, E_Function);
+ Set_Etype (Func_Id, Standard_Boolean);
+ Set_Is_Internal (Func_Id);
+ Set_Is_Predicate_Function (Func_Id);
+ Set_Predicate_Function (Typ, Func_Id);
- Insert_After (Parent (Typ), FDecl);
+ Insert_After (Parent (Typ), Func_Decl);
+ Analyze (Func_Decl);
- Analyze (FDecl);
+ Restore_Ghost_Mode (Mode);
- return FDecl;
+ return Func_Decl;
end Build_Predicate_Function_Declaration;
-----------------------------------------
if not Analyzed (T) then
Set_Analyzed (T);
- -- A type declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (T);
- end if;
-
case Nkind (Def) is
when N_Access_To_Subprogram_Definition =>
Access_Subprogram_Declaration (T, Def);
Set_Is_First_Subtype (T, True);
Set_Etype (T, T);
- -- An incomplete type declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (T);
- end if;
-
-- Ada 2005 (AI-326): Minimum decoration to give support to tagged
-- incomplete types.
Generate_Definition (Id);
Enter_Name (Id);
- -- A number declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- This is an optimization of a common case of an integer literal
if Nkind (E) = N_Integer_Literal then
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
- Related_Id : Entity_Id;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
+ Related_Id : Entity_Id;
-- Start of processing for Analyze_Object_Declaration
end if;
end if;
- -- The object declaration is Ghost when it is subject to pragma Ghost or
- -- completes a deferred Ghost constant. Set the mode now to ensure that
- -- any nodes generated during analysis and expansion are properly marked
- -- as Ghost.
+ if Present (Prev_Entity) then
+
+ -- The object declaration is Ghost when it completes a deferred Ghost
+ -- constant.
- Set_Ghost_Mode (N, Prev_Entity);
+ Mark_And_Set_Ghost_Completion (N, Prev_Entity, Mode);
+ Mode_Set := True;
- if Present (Prev_Entity) then
Constant_Redeclaration (Id, N, T);
Generate_Reference (Prev_Entity, Id, 'c');
and then Analyzed (N)
and then No (Expression (N))
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- If E is null and has been replaced by an N_Raise_Constraint_Error
Set_Ekind (Id, E_Variable);
end if;
- -- An object declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
-
- -- The Ghost policy in effect at the point of declaration
- -- and at the point of completion must match
- -- (SPARK RM 6.9(14)).
-
- if Present (Prev_Entity)
- and then Is_Ghost_Entity (Prev_Entity)
- then
- Check_Ghost_Completion (Prev_Entity, Id);
- end if;
- end if;
-
Rewrite (N,
Make_Object_Renaming_Declaration (Loc,
Defining_Identifier => Id,
Set_Renamed_Object (Id, E);
Freeze_Before (N, T);
Set_Is_Frozen (Id);
-
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
else
-- Ensure that the generated subtype has a unique external name
Init_Esize (Id);
Set_Optimize_Alignment_Flags (Id);
- -- An object declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None
- or else (Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity))
- then
- Set_Is_Ghost_Entity (Id);
-
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
-
- if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
- Check_Ghost_Completion (Prev_Entity, Id);
- end if;
- end if;
-
-- Deal with aliased case
if Aliased_Present (N) then
Check_No_Hidden_State (Id);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze_Object_Declaration;
---------------------------
procedure Array_Type_Declaration (T : in out Entity_Id; Def : Node_Id) is
Component_Def : constant Node_Id := Component_Definition (Def);
Component_Typ : constant Node_Id := Subtype_Indication (Component_Def);
+ P : constant Node_Id := Parent (Def);
Element_Type : Entity_Id;
Implicit_Base : Entity_Id;
Index : Node_Id;
- Related_Id : Entity_Id := Empty;
Nb_Index : Nat;
- P : constant Node_Id := Parent (Def);
Priv : Entity_Id;
+ Related_Id : Entity_Id := Empty;
begin
if Nkind (Def) = N_Constrained_Array_Definition then
then
declare
Loc : constant Source_Ptr := Sloc (Def);
- New_E : Entity_Id;
Decl : Entity_Id;
+ New_E : Entity_Id;
begin
New_E := Make_Temporary (Loc, 'T');
Propagate_Concurrent_Flags (Implicit_Base, Element_Type);
- -- Inherit the "ghostness" from the constrained array type
-
- if Ghost_Mode > None or else Is_Ghost_Entity (T) then
- Set_Is_Ghost_Entity (Implicit_Base);
- end if;
-
-- Unconstrained array case
else
Copy_Array_Base_Type_Attributes (Implicit_Base, Parent_Base);
Set_Has_Delayed_Freeze (Implicit_Base, True);
-
- -- Inherit the "ghostness" from the parent base type
-
- if Ghost_Mode > None or else Is_Ghost_Entity (Parent_Base) then
- Set_Is_Ghost_Entity (Implicit_Base);
- end if;
end Make_Implicit_Base;
-- Start of processing for Build_Derived_Array_Type
-- (anonymous) base type.
if Has_Predicates (Parent_Type)
- or else Has_Predicates (First_Subtype (Parent_Type))
+ or else Has_Predicates (First_Subtype (Parent_Type))
then
Set_Has_Predicates (Derived_Type);
end if;
Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type);
end if;
- -- Propagate the attributes related to pragma Ghost from the parent type
- -- to the derived type or type extension (SPARK RM 6.9(9)).
+ -- A derived type becomes Ghost when its parent type is also Ghost
+ -- (SPARK RM 6.9(9)). Note that the Ghost-related attributes are not
+ -- directly inherited because the Ghost policy in effect may differ.
if Is_Ghost_Entity (Parent_Type) then
Set_Is_Ghost_Entity (Derived_Type);
Set_Alias (New_Subp, Actual_Subp);
end if;
- -- Inherit the "ghostness" from the parent subprogram
-
- if Is_Ghost_Entity (Alias (New_Subp)) then
- Set_Is_Ghost_Entity (New_Subp);
- end if;
-
-- Derived subprograms of a tagged type must inherit the convention
-- of the parent subprogram (a requirement of AI-117). Derived
-- subprograms of untagged types simply get convention Ada by default.
-- The class-wide type of a class-wide type is itself (RM 3.9(14))
Set_Class_Wide_Type (CW_Type, CW_Type);
-
- -- Inherit the "ghostness" from the root tagged type
-
- if Ghost_Mode > None or else Is_Ghost_Entity (T) then
- Set_Is_Ghost_Entity (CW_Type);
- end if;
end Make_Class_Wide_Type;
----------------
Full_Indic : Node_Id;
Full_Parent : Entity_Id;
+ Mode : Ghost_Mode_Type;
Priv_Parent : Entity_Id;
-- Start of processing for Process_Full_View
begin
+ Mark_And_Set_Ghost_Completion (N, Priv_T, Mode);
+
-- First some sanity checks that must be done after semantic
-- decoration of the full view and thus cannot be placed with other
-- similar checks in Find_Type_Name
-- error situation [7.3(8)].
if Priv_Parent = Any_Type or else Full_Parent = Any_Type then
- return;
+ goto Leave;
-- Ada 2005 (AI-251): Interfaces in the full type can be given in
-- any order. Therefore we don't have to check that its parent must
Next_Elmt (Prim_Elmt);
end loop;
- return;
+ goto Leave;
end;
-- For non-concurrent types, transfer explicit primitives, but
Set_Has_Specified_Stream_Output (Full_T);
end if;
- if Is_Ghost_Entity (Priv_T) then
-
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Priv_T, Full_T);
-
- -- Propagate the attributes related to pragma Ghost from the private
- -- to the full view.
-
- Mark_Full_View_As_Ghost (Priv_T, Full_T);
- end if;
-
-- Propagate Default_Initial_Condition-related attributes from the
-- partial view to the full view and its base type.
Set_Predicate_Function (Full_T, Predicate_Function (Priv_T));
end if;
end if;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Process_Full_View;
-----------------------------------
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
-- Start of processing for Analyze_Assignment
-- Ghost entity. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Assignment (N, Mode);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
if PIt = No_Interp then
Error_Msg_N
- ("ambiguous left-hand side"
- & " in assignment", Lhs);
+ ("ambiguous left-hand side in "
+ & "assignment", Lhs);
exit;
else
Resolve (Prefix (Lhs), PIt.Typ);
Error_Msg_N
("no valid types for left-hand side for assignment", Lhs);
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
-- effect (AARM D.5.2 (5/2)).
if Locking_Policy /= 'C' then
- Error_Msg_N ("assignment to the attribute PRIORITY has " &
- "no effect??", Lhs);
- Error_Msg_N ("\since no Locking_Policy has been " &
- "specified??", Lhs);
+ Error_Msg_N
+ ("assignment to the attribute PRIORITY has no effect??",
+ Lhs);
+ Error_Msg_N
+ ("\since no Locking_Policy has been specified??", Lhs);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
end;
Diagnose_Non_Variable_Lhs (Lhs);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- Error of assigning to limited type. We do however allow this in
-- certain cases where the front end generates the assignments.
Explain_Limited_Type (T1, Lhs);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- A class-wide type may be a limited view. This illegal case is not
-- caught by previous checks.
- elsif Ekind (T1) = E_Class_Wide_Type
- and then From_Limited_With (T1)
- then
+ elsif Ekind (T1) = E_Class_Wide_Type and then From_Limited_With (T1) then
Error_Msg_NE ("invalid use of limited view of&", Lhs, T1);
- return;
+ goto Leave;
-- Enforce RM 3.9.3 (8): the target of an assignment operation cannot be
-- abstract. This is only checked when the assignment Comes_From_Source,
then
Error_Msg_N ("invalid use of incomplete type", Lhs);
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Now we can complete the resolution of the right hand side
if Rhs = Error then
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
T2 := Etype (Rhs);
if not Covers (T1, T2) then
Wrong_Type (Rhs, Etype (Lhs));
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Ada 2005 (AI-326): In case of explicit dereference of incomplete
if T1 = Any_Type or else T2 = Any_Type then
Kill_Lhs;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- If the rhs is class-wide or dynamically tagged, then require the lhs
-- to reset Is_True_Constant, and desirable for xref purposes.
Note_Possible_Modification (Lhs, Sure => True);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
-- If we know the right hand side is non-null, then we convert to the
-- target type, since we don't need a run time check in that case.
end;
Analyze_Dimension (N);
- Ghost_Mode := Save_Ghost_Mode;
+
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Analyze_Assignment;
-----------------------------
Set_Categorization_From_Scope (Subp_Id, Scop);
- -- An abstract subprogram declared within a Ghost region is rendered
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Subp_Id);
- end if;
-
if Ekind (Scope (Subp_Id)) = E_Protected_Type then
Error_Msg_N ("abstract subprogram not allowed in protected type", N);
Set_Is_Inlined (Defining_Entity (N));
- -- If the expression function is Ghost, mark its body entity as
- -- Ghost too. This avoids spurious errors on unanalyzed body entities
- -- of expression functions, which are not yet marked as ghost, yet
- -- identified as the Corresponding_Body of the ghost declaration.
-
- if Is_Ghost_Entity (Def_Id) then
- Set_Is_Ghost_Entity (Defining_Entity (New_Body));
- end if;
-
-- Establish the linkages between the spec and the body. These are
-- used when the expression function acts as the prefix of attribute
-- 'Access in order to freeze the original expression which has been
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Scope (Body_Id, Scope (Gen_Id));
- -- Inherit the "ghostness" of the generic spec. Note that this
- -- property is not directly inherited as the body may be subject
- -- to a different Ghost assertion policy.
-
- if Ghost_Mode > None or else Is_Ghost_Entity (Gen_Id) then
- Set_Is_Ghost_Entity (Body_Id);
-
- -- The Ghost policy in effect at the point of declaration and at
- -- the point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Gen_Id, Body_Id);
- end if;
-
Check_Fully_Conformant (Body_Id, Gen_Id, Body_Id);
if Nkind (N) = N_Subprogram_Body_Stub then
Loc : constant Source_Ptr := Sloc (N);
P : constant Node_Id := Name (N);
Actual : Node_Id;
+ Mode : Ghost_Mode_Type;
New_N : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Analyze_Procedure_Call
begin
-- Set the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N);
+ Mark_And_Set_Ghost_Procedure_Call (N, Mode);
-- Otherwise analyze the parameters
if Present (Actuals) then
Error_Msg_N
("no parameters allowed for this call", First (Actuals));
- return;
+ goto Leave;
end if;
Set_Etype (N, Standard_Void_Type);
and then Is_Record_Type (Etype (Entity (P)))
and then Remote_AST_I_Dereference (P)
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
elsif Is_Entity_Name (P)
and then Ekind (Entity (P)) /= E_Entry_Family
Error_Msg_N ("invalid procedure or entry call", N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ Restore_Ghost_Mode (Mode);
end Analyze_Procedure_Call;
------------------------------
------------------------------
procedure Analyze_Return_Statement (N : Node_Id) is
-
- pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
- N_Extended_Return_Statement));
+ pragma Assert (Nkind_In (N, N_Extended_Return_Statement,
+ N_Simple_Return_Statement));
Returns_Object : constant Boolean :=
Nkind (N) = N_Extended_Return_Statement
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
-- Ensure that the generated corresponding spec and original body
- -- share the same Ghost and SPARK_Mode attributes.
-
- Set_Is_Checked_Ghost_Entity
- (Body_Id, Is_Checked_Ghost_Entity (Spec_Id));
- Set_Is_Ignored_Ghost_Entity
- (Body_Id, Is_Ignored_Ghost_Entity (Spec_Id));
+ -- share the same SPARK_Mode attributes.
Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
Set_SPARK_Pragma_Inherited
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
+ Mode_Set : Boolean := False;
-- Start of processing for Analyze_Subprogram_Body_Helper
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
+
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id));
Check_Missing_Return;
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
- else
- -- Previous entity conflicts with subprogram name. Attempting to
- -- enter name will post error.
+ -- Otherwise a previous entity conflicts with the subprogram name.
+ -- Attempting to enter name will post error.
+ else
Enter_Name (Body_Id);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
-- analysis.
elsif Prev_Id = Body_Id and then Has_Completion (Body_Id) then
- Ghost_Mode := Save_Ghost_Mode;
return;
else
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
else
Spec_Id := Find_Corresponding_Spec (N);
-- Ghost. Set the mode now to ensure that any nodes generated
-- during analysis and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
-- In GNATprove mode, if the body has no previous spec, create
-- one so that the inlining machinery can operate properly.
-- If this is a duplicate body, no point in analyzing it
if Error_Posted (N) then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- A subprogram body should cause freezing of its own declaration,
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are properly marked as Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
+ Mode_Set := True;
end if;
end if;
-- function.
Set_Is_Immediately_Visible (Corresponding_Spec (N), False);
- return;
+ goto Leave;
end if;
-- If a separate spec is present, then deal with freezing issues
if Is_Abstract_Subprogram (Spec_Id) then
Error_Msg_N ("an abstract subprogram cannot have a body", N);
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
else
Set_Convention (Body_Id, Convention (Spec_Id));
Set_Has_Completion (Spec_Id);
- -- Inherit the "ghostness" of the subprogram spec. Note that this
- -- property is not directly inherited as the body may be subject
- -- to a different Ghost assertion policy.
-
- if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then
- Set_Is_Ghost_Entity (Body_Id);
-
- -- The Ghost policy in effect at the point of declaration and
- -- at the point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Spec_Id, Body_Id);
- end if;
-
if Is_Protected_Type (Scope (Spec_Id)) then
Prot_Typ := Scope (Spec_Id);
end if;
if not Conformant
and then not Mode_Conformant (Body_Id, Spec_Id)
then
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
end if;
New_Overloaded_Entity (Body_Id);
- -- A subprogram body declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Body_Id);
- end if;
-
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Acts_As_Spec (N);
Generate_Definition (Body_Id);
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
- return;
+ goto Leave;
end if;
-- Handle inlining
-- Check for variables that are never modified
declare
- E1, E2 : Entity_Id;
+ E1 : Entity_Id;
+ E2 : Entity_Id;
begin
-- If there is a separate spec, then transfer Never_Set_In_Source
Set_Directly_Designated_Type (Etype (Spec_Id), Desig_View);
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ <<Leave>>
+ if Mode_Set then
+ Restore_Ghost_Mode (Mode);
+ end if;
end Analyze_Subprogram_Body_Helper;
------------------------------------
Set_SPARK_Pragma_Inherited (Designator);
end if;
- -- A subprogram declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Designator);
- end if;
-
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
Set_Convention (Designator, Convention (E));
- if Is_Ghost_Entity (E) then
- Set_Is_Ghost_Entity (Designator);
- end if;
-
-- Skip past subprogram bodies and subprogram renamings that
-- may appear to have a matching spec, but that aren't fully
-- conformant with it. That can occur in cases where an
Set_Is_Primitive (S);
Check_Private_Overriding (B_Typ);
- -- The Ghost policy in effect at the point of declaration of
- -- a tagged type and a primitive operation must match
+ -- The Ghost policy in effect at the point of declaration
+ -- or a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
- -- The Ghost policy in effect at the point of declaration of
- -- a tagged type and a primitive operation must match
+ -- The Ghost policy in effect at the point of declaration
+ -- of a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
Set_Etype (Formal, Formal_Type);
- -- A formal parameter declared within a Ghost region is automatically
- -- Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Formal);
- end if;
-
-- Deal with default expression if present
Default := Expression (Param_Spec);
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Body_Id : Entity_Id;
HSS : Node_Id;
Last_Spec_Entity : Entity_Id;
+ Mode : Ghost_Mode_Type;
New_N : Node_Id;
Pack_Decl : Node_Id;
Spec_Id : Entity_Id;
-- the mode now to ensure that any nodes generated during analysis and
-- expansion are properly flagged as ignored Ghost.
- Set_Ghost_Mode (N, Spec_Id);
+ Mark_And_Set_Ghost_Body (N, Spec_Id, Mode);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Style.Check_Identifier (Body_Id, Spec_Id);
Set_SPARK_Aux_Pragma_Inherited (Body_Id);
end if;
- -- Inherit the "ghostness" of the package spec. Note that this property
- -- is not directly inherited as the body may be subject to a different
- -- Ghost assertion policy.
-
- if Ghost_Mode > None or else Is_Ghost_Entity (Spec_Id) then
- Set_Is_Ghost_Entity (Body_Id);
-
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
-
- Check_Ghost_Completion (Spec_Id, Body_Id);
- end if;
-
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
end if;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Analyze_Package_Body_Helper;
---------------------------------
procedure Analyze_Package_Declaration (N : Node_Id) is
Id : constant Node_Id := Defining_Entity (N);
- Par : constant Node_Id := Parent_Spec (N);
Is_Comp_Unit : constant Boolean :=
Nkind (Parent (N)) = N_Compilation_Unit;
Set_SPARK_Aux_Pragma_Inherited (Id);
end if;
- -- A package declared within a Ghost refion is automatically Ghost. A
- -- child package is Ghost when its parent is Ghost (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None
- or else (Present (Par)
- and then Is_Ghost_Entity (Defining_Entity (Unit (Par))))
- then
- Set_Is_Ghost_Entity (Id);
- end if;
-
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
New_Private_Type (N, Id, N);
Set_Depends_On_Private (Id);
- -- A type declared within a Ghost region is automatically Ghost
- -- (SPARK RM 6.9(2)).
-
- if Ghost_Mode > None then
- Set_Is_Ghost_Entity (Id);
- end if;
-
if Has_Aspects (N) then
Analyze_Aspect_Specifications (N, Id);
end if;
-- The exception renaming declaration may become Ghost if it renames
-- a Ghost entity.
- Mark_Renaming_As_Ghost (N, Entity (Nam));
+ Mark_Ghost_Renaming (N, Entity (Nam));
else
Error_Msg_N ("invalid exception name in renaming", Nam);
end if;
K : Entity_Kind)
is
New_P : constant Entity_Id := Defining_Entity (N);
- Old_P : Entity_Id;
-
Inst : Boolean := False;
- -- Prevent junk warning
+ Old_P : Entity_Id;
begin
if Name (N) = Error then
Set_Renamed_Object (New_P, Old_P);
end if;
+ -- The generic renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ Mark_Ghost_Renaming (N, Old_P);
+
Set_Is_Pure (New_P, Is_Pure (Old_P));
Set_Is_Preelaborated (New_P, Is_Preelaborated (Old_P));
Set_Etype (New_P, Etype (Old_P));
Set_Has_Completion (New_P);
- -- The generic renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Old_P);
-
if In_Open_Scopes (Old_P) then
Error_Msg_N ("within its scope, generic denotes its instance", N);
end if;
-- already-analyzed expression.
if Nkind (Nam) = N_Selected_Component and then Analyzed (Nam) then
- T := Etype (Nam);
+
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
+ T := Etype (Nam);
Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam);
if Present (Dec) then
T := Entity (Subtype_Mark (N));
Analyze (Nam);
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- Reject renamings of conversions unless the type is tagged, or
-- the conversion is implicit (which can occur for cases of anonymous
-- access types in Ada 2012).
-- Ada 2005 (AI-230/AI-254): Access renaming
else pragma Assert (Present (Access_Definition (N)));
- T := Access_Definition
- (Related_Nod => N,
- N => Access_Definition (N));
+ T :=
+ Access_Definition
+ (Related_Nod => N,
+ N => Access_Definition (N));
Analyze (Nam);
+ -- The object renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- Ada 2005 AI05-105: if the declaration has an anonymous access
-- type, the renamed object must also have an anonymous type, and
-- this is a name resolution rule. This was implicit in the last part
("\suggest using an initialized constant "
& "object instead?R?", Nam);
end if;
-
end case;
end if;
Set_Is_True_Constant (Id, True);
end if;
- -- The object renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- if Is_Entity_Name (Nam) then
- Mark_Renaming_As_Ghost (N, Entity (Nam));
- end if;
-
-- The entity of the renaming declaration needs to reflect whether the
-- renamed object is volatile. Is_Volatile is set if the renamed object
-- is volatile in the RM legality sense.
else
Error_Msg_Sloc := Sloc (Old_P);
Error_Msg_NE
- ("expect package name in renaming, found& declared#",
+ ("expect package name in renaming, found& declared#",
Name (N), Old_P);
end if;
Set_Renamed_Object (New_P, Old_P);
end if;
- Set_Has_Completion (New_P);
+ -- The package renaming declaration may become Ghost if it renames a
+ -- Ghost entity.
- Set_First_Entity (New_P, First_Entity (Old_P));
- Set_Last_Entity (New_P, Last_Entity (Old_P));
+ Mark_Ghost_Renaming (N, Old_P);
+
+ Set_Has_Completion (New_P);
+ Set_First_Entity (New_P, First_Entity (Old_P));
+ Set_Last_Entity (New_P, Last_Entity (Old_P));
Set_First_Private_Entity (New_P, First_Private_Entity (Old_P));
Check_Library_Unit_Renaming (N, Old_P);
Generate_Reference (Old_P, Name (N));
- -- The package renaming declaration may become Ghost if it renames a
- -- Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Old_P);
-
-- If the renaming is in the visible part of a package, then we set
-- Renamed_In_Spec for the renamed package, to prevent giving
-- warnings about no entities referenced. Such a warning would be
and then Expander_Active
then
declare
- Stream_Prim : Entity_Id;
Prefix_Type : constant Entity_Id := Entity (Prefix (Nam));
+ Stream_Prim : Entity_Id;
begin
-- The class-wide forms of the stream attributes are not
Find_Optional_Prim_Op (Prefix_Type, TSS_Stream_Write);
when others =>
Error_Msg_N
- ("attribute must be a primitive"
- & " dispatching operation", Nam);
+ ("attribute must be a primitive dispatching operation",
+ Nam);
return;
end case;
- -- If no operation was found, and the type is limited,
- -- the user should have defined one.
+ -- If no operation was found, and the type is limited, the user
+ -- should have defined one.
if No (Stream_Prim) then
if Is_Limited_Type (Prefix_Type) then
end if;
end if;
- -- Check whether this declaration corresponds to the instantiation
- -- of a formal subprogram.
+ -- Check whether this declaration corresponds to the instantiation of a
+ -- formal subprogram.
-- If this is an instantiation, the corresponding actual is frozen and
-- error messages can be made more precise. If this is a default
-- is an external axiomatization on the package.
if CW_Actual
- and then Box_Present (Inst_Node)
- and then not
+ and then Box_Present (Inst_Node)
+ and then not
(GNATprove_Mode
and then
Present (Containing_Package_With_Ext_Axioms (Formal_Spec)))
and then not Is_Overloaded (Nam)
then
Old_S := Entity (Nam);
+
+ -- The subprogram renaming declaration may become Ghost if it
+ -- renames a Ghost entity.
+
+ Mark_Ghost_Renaming (N, Old_S);
+
New_S := Analyze_Subprogram_Specification (Spec);
-- Operator case
- if Ekind (Entity (Nam)) = E_Operator then
+ if Ekind (Old_S) = E_Operator then
-- Box present
and then Hidden /= Old_S
then
Error_Msg_Sloc := Sloc (Hidden);
- Error_Msg_N ("default subprogram is resolved " &
- "in the generic declaration " &
- "(RM 12.6(17))??", N);
+ Error_Msg_N
+ ("default subprogram is resolved in the generic "
+ & "declaration (RM 12.6(17))??", N);
Error_Msg_NE ("\and will not use & #??", N, Hidden);
end if;
end;
else
Analyze (Nam);
+
+ -- The subprogram renaming declaration may become Ghost if it
+ -- renames a Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
New_S := Analyze_Subprogram_Specification (Spec);
end if;
Analyze (Nam);
+ -- The subprogram renaming declaration may become Ghost if it renames
+ -- a Ghost entity.
+
+ if Is_Entity_Name (Nam) then
+ Mark_Ghost_Renaming (N, Entity (Nam));
+ end if;
+
-- The renaming defines a new overloaded entity, which is analyzed
-- like a subprogram declaration.
Error_Msg_NE
("subprogram& overrides inherited operation",
N, Rename_Spec);
- elsif
- Style_Check and then not Must_Override (Specification (N))
+
+ elsif Style_Check
+ and then not Must_Override (Specification (N))
then
Style.Missing_Overriding (N, Rename_Spec);
end if;
Set_Is_Pure (New_S, Is_Pure (Entity (Nam)));
Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam)));
- -- The subprogram renaming declaration may become Ghost if it renames
- -- a Ghost entity.
-
- Mark_Renaming_As_Ghost (N, Entity (Nam));
-
-- Ada 2005 (AI-423): Check the consistency of null exclusions
-- between a subprogram and its correct renaming.
not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
then
Error_Msg_N
- ("renamed entity cannot be "
- & "subprogram that requires overriding (RM 8.5.4 (5.1))", N);
+ ("renamed entity cannot be subprogram that requires overriding "
+ & "(RM 8.5.4 (5.1))", N);
end if;
end if;
then
Error_Msg_N
("subprogram in renaming_as_body cannot be intrinsic",
- Name (N));
+ Name (N));
end if;
Set_Has_Completion (Rename_Spec);
then
Error_Msg_Node_2 := T1;
Error_Msg_NE
- ("default & on & is not directly visible",
- Nam, Nam);
+ ("default & on & is not directly visible", Nam, Nam);
end if;
end;
end if;
then
Error_Msg_N ("access parameter is controlling,", New_F);
Error_Msg_NE
- ("\corresponding parameter of& "
- & "must be explicitly null excluding", New_F, Old_S);
+ ("\corresponding parameter of& must be explicitly null "
+ & "excluding", New_F, Old_S);
end if;
Next_Formal (Old_F);
CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
CCase : Node_Id;
+ Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Contract_Cases_In_Decl_Part
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- Single and multiple contract cases must appear in aggregate form. If
-- this is not the case, then either the parser of the analysis of the
Error_Msg_N ("wrong syntax for constract cases", N);
end if;
- Ghost_Mode := Save_Ghost_Mode;
Set_Is_Analyzed_Pragma (N);
+ Restore_Ghost_Mode (Mode);
end Analyze_Contract_Cases_In_Decl_Part;
----------------------------------
Pack_Id : constant Entity_Id := Defining_Entity (Pack_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Pack_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Mode : Ghost_Mode_Type;
begin
-- Do not analyze the pragma multiple times
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- The expression is preanalyzed because it has not been moved to its
-- final place yet. A direct analysis may generate side effects and this
-- is not desired at this point.
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
- Ghost_Mode := Save_Ghost_Mode;
-
Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
end Analyze_Depends_Global;
Subp_Id := Defining_Entity (Subp_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Subp_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Pre_Post_Condition_In_Decl_Part.
Add_Contract_Item (N, Defining_Entity (Subp_Decl));
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Subp_Id);
-
-- Fully analyze the pragma when it appears inside an entry or
-- subprogram body because it cannot benefit from forward references.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
if Nam_In (Pname, Name_Refined_Depends, Name_Refined_Global) then
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost variable being
-- processed for error detection purposes.
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost name being
-- processed for error detection purposes.
return;
end if;
- E := Entity (E_Arg);
- Decl := Declaration_Node (E);
+ E := Entity (E_Arg);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Check duplicate before we chain ourselves
-- Now check appropriateness of the entity
+ Decl := Declaration_Node (E);
+
if Is_Type (E) then
if Rep_Item_Too_Early (E, N)
or else
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Def_Id);
+ Mark_Ghost_Pragma (N, Def_Id);
Kill_Size_Check_Code (Def_Id);
Note_Possible_Modification (Get_Pragma_Arg (Arg2), Sure => False);
end if;
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Subp);
+ Mark_Ghost_Pragma (N, Subp);
-- Capture the entity of the first Ghost subprogram being
-- processed for error detection purposes.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Handler);
+ Mark_Ghost_Pragma (N, Handler);
Set_Is_Interrupt_Handler (Handler);
pragma Assert (Ekind (Prot_Typ) = E_Protected_Type);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Enforce RM 11.5(7) which requires that for a pragma that
-- appears within a package spec, the named entity must be
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Pack_Id);
-- Analyze all these pragmas in the order outlined above
Analyze_If_Present (Pragma_SPARK_Mode);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
- Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-
States := Expression (Get_Argument (N, Pack_Id));
-- Multiple non-null abstract states appear as an aggregate
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Lib_Entity);
+ Mark_Ghost_Pragma (N, Lib_Entity);
-- This pragma should only apply to a RCI unit (RM E.2.3(23))
if Is_Entity_Name (Get_Pragma_Arg (Nam_Arg))
and then Present (Entity (Get_Pragma_Arg (Nam_Arg)))
then
- Mark_Pragma_As_Ghost (N, Entity (Get_Pragma_Arg (Nam_Arg)));
+ Mark_Ghost_Pragma (N, Entity (Get_Pragma_Arg (Nam_Arg)));
end if;
-- Not allowed in compiler units (bootstrap issues)
if Ekind (Obj_Id) = E_Variable then
- -- Chain the pragma on the contract for further processing by
- -- Analyze_External_Property_In_Decl_Part.
-
- Add_Contract_Item (N, Obj_Id);
-
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Id);
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_External_Property_In_Decl_Part.
+
+ Add_Contract_Item (N, Obj_Id);
-- Analyze the Boolean expression (if any)
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Nm);
+ Mark_Ghost_Pragma (N, Nm);
if not Is_Remote_Call_Interface (C_Ent)
and then not Is_Remote_Types (C_Ent)
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
Check_Duplicate_Pragma (E);
if Rep_Item_Too_Early (E, N)
Cname : Name_Id;
Eloc : Source_Ptr;
Expr : Node_Id;
+ Mode : Ghost_Mode_Type;
Str : Node_Id;
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
begin
-- Pragma Check is Ghost when it applies to a Ghost entity. Set
-- the mode now to ensure that any nodes generated during analysis
-- and expansion are marked as Ghost.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
- Ghost_Mode := Save_Ghost_Mode;
+ Restore_Ghost_Mode (Mode);
end Check;
--------------------------
return;
end if;
- -- Chain the pragma on the contract for completeness
-
- Add_Contract_Item (N, Obj_Id);
-
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Id);
+
+ -- Chain the pragma on the contract for completeness
+
+ Add_Contract_Item (N, Obj_Id);
-- Analyze the Boolean expression (if any)
Spec_Id := Unique_Defining_Entity (Subp_Decl);
- -- Chain the pragma on the contract for further processing by
- -- Analyze_Contract_Cases_In_Decl_Part.
-
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
-
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Spec_Id);
+ Mark_Ghost_Pragma (N, Spec_Id);
Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Contract_Cases_In_Decl_Part.
+
+ Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
-- Fully analyze the pragma when it appears inside an entry
-- or subprogram body because it cannot benefit from forward
-- references.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
end Convention;
---------------------------
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The pragma signals that the type defines its own DIC assertion
-- expression.
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Entity (Pool));
+ Mark_Ghost_Pragma (N, Entity (Pool));
else
Error_Pragma_Arg
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if (Is_First_Subtype (E)
and then
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- The expression must be analyzed in the special manner
-- described in "Handling of Default and Per-Object
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if Nkind_In (Unit (Cunit_Node), N_Package_Body,
N_Subprogram_Body)
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Def_Id);
+ Mark_Ghost_Pragma (N, Def_Id);
if Ekind (Def_Id) /= E_Constant then
Note_Possible_Modification
return;
end if;
+ -- Mark the pragma as Ghost if the related subprogram is also
+ -- Ghost. This also ensures that any expansion performed further
+ -- below will produce Ghost nodes.
+
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Defining_Entity (Subp_Decl));
Analyze_If_Present (Pragma_SPARK_Mode);
- -- Mark the pragma as Ghost if the related subprogram is also
- -- Ghost. This also ensures that any expansion performed further
- -- below will produce Ghost nodes.
-
- Spec_Id := Unique_Defining_Entity (Subp_Decl);
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- Examine the formals of the related subprogram
Formal := First_Formal (Spec_Id);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
Note_Possible_Modification
(Get_Pragma_Arg (Arg2), Sure => False);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- If it's an access-to-subprogram type (in particular, not a
-- subtype), set the flag on that type.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Check duplicate before we chain ourselves
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Initial_Condition_In_Decl_Part.
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Abstract_State);
Analyze_If_Present (Pragma_Initializes);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
end Initial_Condition;
------------------------
Pack_Id := Defining_Entity (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Pack_Id);
+ Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Initializes_In_Decl_Part.
Analyze_If_Present (Pragma_SPARK_Mode);
Analyze_If_Present (Pragma_Abstract_State);
-
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Pack_Id);
- Ensure_Aggregate_Form (Get_Argument (N, Pack_Id));
-
Analyze_If_Present (Pragma_Initial_Condition);
end Initializes;
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The pragma defines a type-specific invariant, the type is said
-- to have invariants of its "own".
-- the purposes of legality checks and removal of ignored
-- Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Subprograms
-- Ghost for the purposes of legality checks and
-- removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Capture the entity of the first Ghost subprogram
-- being processed for error detection purposes.
-- Ghost. This also ensures that any expansion performed further
-- below will produce Ghost nodes.
- Mark_Pragma_As_Ghost (N, Entry_Id);
+ Mark_Ghost_Pragma (N, Entry_Id);
-- Analyze the Integer expression
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Capture the entity of the first Ghost procedure being
-- processed for error detection purposes.
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
-- Entity name was given
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
if not Is_Array_Type (Typ) and then not Is_Record_Type (Typ) then
Error_Pragma ("pragma% must specify array or record type");
end if;
Item_Id := Defining_Entity (Stmt);
- Encap := Get_Pragma_Arg (Arg1);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Item_Id);
+ Mark_Ghost_Pragma (N, Item_Id);
-- Chain the pragma on the contract for further processing by
-- Analyze_Part_Of_In_Decl_Part or for completeness.
-- instantiation.
else
+ Encap := Get_Pragma_Arg (Arg1);
+
-- Detect any discrepancies between the placement of the
-- constant or package instantiation with respect to state
-- space and the encapsulating state.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- The pragma may come from an aspect on a private declaration,
-- even if the freeze point at which this is analyzed in the
end if;
Ent := Entity (Get_Pragma_Arg (Arg1));
- Decl := Parent (Ent);
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
-- Check for duplication before inserting in list of
-- representation items.
return;
end if;
+ Decl := Parent (Ent);
+
if Present (Expression (Decl)) then
Error_Pragma_Arg
("object for pragma% cannot have initialization", Arg1);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The remaining processing is simply to link the pragma on to
-- the rep item chain, for processing when the type is frozen.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- The remaining processing is simply to link the pragma on to
-- the rep item chain, for processing when the type is frozen.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
Check_Duplicate_Pragma (Ent);
-- This filters out pragmas inside generic parents that show up
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Ent);
+ Mark_Ghost_Pragma (N, Ent);
if not Debug_Flag_U then
Set_Is_Pure (Ent);
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Present (E) then
loop
Spec_Id := Corresponding_Spec (Pack_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Refined_State_In_Decl_Part.
Analyze_If_Present (Pragma_SPARK_Mode);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- State refinement is allowed only when the corresponding package
-- declaration has non-null pragma Abstract_State. Refinement not
-- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)).
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Nkind (Parent (E)) = N_Formal_Type_Declaration
and then Ekind (E) = E_General_Access_Type
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if K = N_Package_Declaration
or else K = N_Generic_Package_Declaration
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Cunit_Ent);
+ Mark_Ghost_Pragma (N, Cunit_Ent);
if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
N_Generic_Package_Declaration)
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
-- We require the pragma to apply to a type declared in a package
-- declaration, but not (immediately) within a package body.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Nam_Id);
+ Mark_Ghost_Pragma (N, Nam_Id);
Set_Debug_Info_Off (Nam_Id);
end Suppress_Debug_Info;
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if not Is_Type (E) and then Ekind (E) /= E_Variable then
Error_Pragma_Arg
Subp_Id := Defining_Entity (Subp_Decl);
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Subp_Id);
+
-- Chain the pragma on the contract for further processing by
-- Analyze_Test_Case_In_Decl_Part.
Add_Contract_Item (N, Subp_Id);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Subp_Id);
-
-- Preanalyze the original aspect argument "Name" for ASIS or for
-- a generic subprogram to properly capture global references.
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E);
+ Mark_Ghost_Pragma (N, E);
if Rep_Item_Too_Early (E, N)
or else
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Typ);
+ Mark_Ghost_Pragma (N, Typ);
if Typ = Any_Type
or else Rep_Item_Too_Early (Typ, N)
-- A pragma that applies to a Ghost entity becomes Ghost for the
-- purposes of legality checks and removal of ignored Ghost code.
- Mark_Pragma_As_Ghost (N, E_Id);
+ Mark_Ghost_Pragma (N, E_Id);
Set_Universal_Aliasing (Implementation_Base_Type (E_Id));
Record_Rep_Item (E_Id, N);
end Universal_Alias;
-- for the purposes of legality checks and removal of
-- ignored Ghost code.
- Mark_Pragma_As_Ghost (N, Arg_Id);
+ Mark_Ghost_Pragma (N, Arg_Id);
-- Capture the entity of the first Ghost type being
-- processed for error detection purposes.
return;
end if;
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Ghost_Pragma (N, Spec_Id);
+
-- Chain the pragma on the contract for completeness
Add_Contract_Item (N, Spec_Id);
Analyze_If_Present (Pragma_SPARK_Mode);
- -- A pragma that applies to a Ghost entity becomes Ghost for the
- -- purposes of legality checks and removal of ignored Ghost code.
-
- Mark_Pragma_As_Ghost (N, Spec_Id);
-
-- A volatile function cannot override a non-volatile function
-- (SPARK RM 7.1.2(15)). Overriding checks are usually performed
-- in New_Overloaded_Entity, however at that point the pragma has
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
Errors : Nat;
+ Mode : Ghost_Mode_Type;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
-- point of analysis may not necessarily be the same. Use the mode in
-- effect at the point of declaration.
- Set_Ghost_Mode (N);
+ Set_Ghost_Mode (N, Mode);
-- Ensure that the subprogram and its formals are visible when analyzing
-- the expression of the pragma.
-- subprogram subject to pragma Inline_Always.
Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
- Ghost_Mode := Save_Ghost_Mode;
-
Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Mode (Mode);
end Analyze_Pre_Post_Condition_In_Decl_Part;
------------------------------------------
return;
end Resolution_Failed;
- -- Local variables
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-- Start of processing for Resolve
begin
return;
end if;
- -- A declaration may be subject to pragma Ghost. Set the mode now to
- -- ensure that any nodes generated during analysis and expansion are
- -- marked as Ghost.
-
- if Is_Declaration (N) then
- Set_Ghost_Mode (N);
- end if;
-
-- Access attribute on remote subprogram cannot be used for a non-remote
-- access-to-subprogram type.
if Analyzed (N) then
Debug_A_Exit ("resolving ", N, " (done, already analyzed)");
Analyze_Dimension (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Any case of Any_Type as the Etype value means that we had a
elsif Etype (N) = Any_Type then
Debug_A_Exit ("resolving ", N, " (done, Etype = Any_Type)");
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
then
Resolve (N, Full_View (Typ));
Set_Etype (N, Typ);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Check for an aggregate. Sometimes we can get bogus aggregates
if Address_Integer_Convert_OK (Typ, Etype (N)) then
Rewrite (N, Unchecked_Convert_To (Typ, Relocate_Node (N)));
Analyze_And_Resolve (N, Typ);
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Under relaxed RM semantics silently replace occurrences of null
Error_Msg_Node_2 := Typ;
Error_Msg_NE
- ("no visible interpretation of& "
- & "matches expected type&", N, Subp_Name);
+ ("no visible interpretation of& matches expected type&",
+ N, Subp_Name);
end;
if All_Errors_Mode then
end if;
Resolution_Failed;
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Test if we have more than one interpretation for the context
elsif Ambiguous then
Resolution_Failed;
- Ghost_Mode := Save_Ghost_Mode;
return;
-- Only one intepretation
and then Present (Entity (N))
and then Ekind (Entity (N)) /= E_Operator
then
-
if not Is_Predefined_Op (Entity (N)) then
Rewrite_Operator_As_Call (N, Entity (N));
-- Rewrite_Renamed_Operator.
if Analyzed (N) then
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
end if;
end if;
case N_Subexpr'(Nkind (N)) is
-
when N_Aggregate => Resolve_Aggregate (N, Ctx_Type);
when N_Allocator => Resolve_Allocator (N, Ctx_Type);
if Nkind (N) not in N_Subexpr then
Debug_A_Exit ("resolving ", N, " (done)");
Expand (N);
- Ghost_Mode := Save_Ghost_Mode;
return;
end if;
Expand (N);
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Resolve;
-------------
--------------------
function Is_Declaration (N : Node_Id) return Boolean is
+ begin
+ return
+ Is_Declaration_Other_Than_Renaming (N)
+ or else Is_Renaming_Declaration (N);
+ end Is_Declaration;
+
+ ----------------------------------------
+ -- Is_Declaration_Other_Than_Renaming --
+ ----------------------------------------
+
+ function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is
begin
case Nkind (N) is
when N_Abstract_Subprogram_Declaration |
N_Exception_Declaration |
- N_Exception_Renaming_Declaration |
+ N_Expression_Function |
N_Full_Type_Declaration |
- N_Generic_Function_Renaming_Declaration |
N_Generic_Package_Declaration |
- N_Generic_Package_Renaming_Declaration |
- N_Generic_Procedure_Renaming_Declaration |
N_Generic_Subprogram_Declaration |
N_Number_Declaration |
N_Object_Declaration |
- N_Object_Renaming_Declaration |
N_Package_Declaration |
- N_Package_Renaming_Declaration |
N_Private_Extension_Declaration |
N_Private_Type_Declaration |
N_Subprogram_Declaration |
- N_Subprogram_Renaming_Declaration |
N_Subtype_Declaration =>
return True;
when others =>
return False;
end case;
- end Is_Declaration;
+ end Is_Declaration_Other_Than_Renaming;
--------------------------------
-- Is_Declared_Within_Variant --
function Is_Declaration (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes a declaration
+ function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a non-renaming declaration
+
function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean;
-- Returns True iff component Comp is declared within a variant part
return Flag11 (N);
end Is_Checked;
+ function Is_Checked_Ghost_Pragma
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ return Flag3 (N);
+ end Is_Checked_Ghost_Pragma;
+
function Is_Component_Left_Opnd
(N : Node_Id) return Boolean is
begin
return Flag2 (N);
end Is_Generic_Contract_Pragma;
- function Is_Ghost_Pragma
+ function Is_Ignored
(N : Node_Id) return Boolean is
begin
pragma Assert (False
+ or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- return Flag3 (N);
- end Is_Ghost_Pragma;
+ return Flag9 (N);
+ end Is_Ignored;
- function Is_Ignored
+ function Is_Ignored_Ghost_Pragma
(N : Node_Id) return Boolean is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- return Flag9 (N);
- end Is_Ignored;
+ return Flag8 (N);
+ end Is_Ignored_Ghost_Pragma;
function Is_In_Discriminant_Check
(N : Node_Id) return Boolean is
Set_Flag11 (N, Val);
end Set_Is_Checked;
+ procedure Set_Is_Checked_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Pragma);
+ Set_Flag3 (N, Val);
+ end Set_Is_Checked_Ghost_Pragma;
+
procedure Set_Is_Component_Left_Opnd
(N : Node_Id; Val : Boolean := True) is
begin
Set_Flag2 (N, Val);
end Set_Is_Generic_Contract_Pragma;
- procedure Set_Is_Ghost_Pragma
+ procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
+ or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- Set_Flag3 (N, Val);
- end Set_Is_Ghost_Pragma;
+ Set_Flag9 (N, Val);
+ end Set_Is_Ignored;
- procedure Set_Is_Ignored
+ procedure Set_Is_Ignored_Ghost_Pragma
(N : Node_Id; Val : Boolean := True) is
begin
pragma Assert (False
- or else NT (N).Nkind = N_Aspect_Specification
or else NT (N).Nkind = N_Pragma);
- Set_Flag9 (N, Val);
- end Set_Is_Ignored;
+ Set_Flag8 (N, Val);
+ end Set_Is_Ignored_Ghost_Pragma;
procedure Set_Is_In_Discriminant_Check
(N : Node_Id; Val : Boolean := True) is
-- Ghost Mode --
----------------
- -- When a declaration is subject to pragma Ghost, it establishes a Ghost
- -- region depending on the Ghost assertion policy in effect at the point
- -- of declaration. This region is temporal and starts right before the
- -- analysis of the Ghost declaration and ends after its expansion. The
- -- values of global variable Opt.Ghost_Mode are as follows:
+ -- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and
+ -- Ghost statements. The intent of the feature is to treat Ghost constructs
+ -- as non-existent when Ghost assertion policy Ignore is in effect.
+
+ -- The corresponding nodes which map to Ghost constructs are:
+
+ -- Ghost entities
+ -- Declaration nodes
+ -- N_Package_Body
+ -- N_Subprogram_Body
+
+ -- Ghost statements
+ -- N_Assignment_Statement
+ -- N_Procedure_Call_Statement
+ -- N_Pragma
+
+ -- In addition, the compiler treats instantiations as Ghost entities
+
+ -- To achieve the removal of ignored Ghost constructs, the compiler relies
+ -- on global variable Ghost_Mode and a mechanism called "Ghost regions".
+ -- The values of the global variable are as follows:
-- 1. Check - All static semantics as defined in SPARK RM 6.9 are in
- -- effect.
+ -- effect. The Ghost region has mode Check.
-- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI
- -- files, object files as well as the final executable.
+ -- files, object files, and the final executable. The Ghost region
+ -- has mode Ignore.
+
+ -- 3. None - No Ghost region is in effect
+
+ -- A Ghost region is a compiler operating mode, similar to Check_Syntax,
+ -- however a region is much more finely grained and depends on the policy
+ -- in effect. The region starts prior to the analysis of a Ghost construct
+ -- and ends immediately after its expansion. The region is established as
+ -- follows:
+
+ -- 1. Declarations - Prior to analysis, if the declaration is subject to
+ -- pragma Ghost.
+
+ -- 2. Renaming declarations - Same as 1) or when the renamed entity is
+ -- Ghost.
- -- To achieve the runtime semantics of "Ignore", the compiler marks each
- -- node created during an ignored Ghost region and signals all enclosing
- -- scopes that such a node resides within. The compilation unit where the
- -- node resides is also added to an auxiliary table for post processing.
+ -- 3. Completing declarations - Same as 1) or when the declaration is
+ -- partially analyzed and the declaration completes a Ghost entity.
+
+ -- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is
+ -- partially analyzed and completes a Ghost entity.
+
+ -- 5. N_Assignment_Statement - After the left hand side is analyzed and
+ -- references a Ghost entity.
+
+ -- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes
+ -- a Ghost procedure.
+
+ -- 7. N_Pragma - During analysis, when the related entity is Ghost or the
+ -- pragma encloses a Ghost entity.
+
+ -- 8. Instantiations - Save as 1) or when the instantiation is partially
+ -- analyzed and the generic template is Ghost.
+
+ -- Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine
+ -- Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled
+ -- similar to scopes for decoupled expansion such as the generation of
+ -- dispatch tables or the creation of a predicate function.
+
+ -- If the mode of a Ghost region is Ignore, any newly created nodes as well
+ -- as source entities are marked as ignored Ghost. In additon, the marking
+ -- process signals all enclosing scopes that an ignored Ghost node resides
+ -- within. The compilation unit where the node resides is also added to an
+ -- auxiliary table for post processing.
-- After the analysis and expansion of all compilation units takes place
-- as well as the instantiation of all inlined [generic] bodies, the GNAT
- -- driver initiates a separate pass which removes all ignored Ghost code
+ -- driver initiates a separate pass which removes all ignored Ghost nodes
-- from all units stored in the auxiliary table.
--------------------
-- be further modified (in some cases these flags are copied when a
-- pragma is rewritten).
+ -- Is_Checked_Ghost_Pragma (Flag3-Sem)
+ -- This flag is present in N_Pragma nodes. It is set when the pragma is
+ -- related to a checked Ghost entity or encloses a checked Ghost entity.
+ -- This flag has no relation to Is_Checked.
+
-- Is_Component_Left_Opnd (Flag13-Sem)
-- Is_Component_Right_Opnd (Flag14-Sem)
-- Present in concatenation nodes, to indicate that the corresponding
-- Refined_State
-- Test_Case
- -- Is_Ghost_Pragma (Flag3-Sem)
- -- This flag is present in N_Pragma nodes. It is set when the pragma is
- -- either declared within a Ghost construct or it applies to a Ghost
- -- construct.
-
-- Is_Ignored (Flag9-Sem)
-- A flag set in an N_Aspect_Specification or N_Pragma node if there was
-- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
-- aspect/pragma is fully analyzed and checked for other syntactic
-- and semantic errors, but it does not have any semantic effect.
+ -- Is_Ignored_Ghost_Pragma (Flag8-Sem)
+ -- This flag is present in N_Pragma nodes. It is set when the pragma is
+ -- related to an ignored Ghost entity or encloses ignored Ghost entity.
+ -- This flag has no relation to Is_Ignored.
+
-- Is_In_Discriminant_Check (Flag11-Sem)
-- This flag is present in a selected component, and is used to indicate
-- that the reference occurs within a discriminant check. The
-- Import_Interface_Present (Flag16-Sem)
-- Is_Analyzed_Pragma (Flag5-Sem)
-- Is_Checked (Flag11-Sem)
+ -- Is_Checked_Ghost_Pragma (Flag3-Sem)
-- Is_Delayed_Aspect (Flag14-Sem)
-- Is_Disabled (Flag15-Sem)
-- Is_Generic_Contract_Pragma (Flag2-Sem)
- -- Is_Ghost_Pragma (Flag3-Sem)
-- Is_Ignored (Flag9-Sem)
+ -- Is_Ignored_Ghost_Pragma (Flag8-Sem)
-- Is_Inherited_Pragma (Flag4-Sem)
-- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
-- Uneval_Old_Accept (Flag7-Sem)
function Is_Checked
(N : Node_Id) return Boolean; -- Flag11
+ function Is_Checked_Ghost_Pragma
+ (N : Node_Id) return Boolean; -- Flag3
+
function Is_Component_Left_Opnd
(N : Node_Id) return Boolean; -- Flag13
function Is_Generic_Contract_Pragma
(N : Node_Id) return Boolean; -- Flag2
- function Is_Ghost_Pragma
- (N : Node_Id) return Boolean; -- Flag3
-
function Is_Ignored
(N : Node_Id) return Boolean; -- Flag9
+ function Is_Ignored_Ghost_Pragma
+ (N : Node_Id) return Boolean; -- Flag8
+
function Is_In_Discriminant_Check
(N : Node_Id) return Boolean; -- Flag11
procedure Set_Is_Checked
(N : Node_Id; Val : Boolean := True); -- Flag11
+ procedure Set_Is_Checked_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True); -- Flag3
+
procedure Set_Is_Component_Left_Opnd
(N : Node_Id; Val : Boolean := True); -- Flag13
procedure Set_Is_Generic_Contract_Pragma
(N : Node_Id; Val : Boolean := True); -- Flag2
- procedure Set_Is_Ghost_Pragma
- (N : Node_Id; Val : Boolean := True); -- Flag3
-
procedure Set_Is_Ignored
(N : Node_Id; Val : Boolean := True); -- Flag9
+ procedure Set_Is_Ignored_Ghost_Pragma
+ (N : Node_Id; Val : Boolean := True); -- Flag8
+
procedure Set_Is_In_Discriminant_Check
(N : Node_Id; Val : Boolean := True); -- Flag11
pragma Inline (Is_Asynchronous_Call_Block);
pragma Inline (Is_Boolean_Aspect);
pragma Inline (Is_Checked);
+ pragma Inline (Is_Checked_Ghost_Pragma);
pragma Inline (Is_Component_Left_Opnd);
pragma Inline (Is_Component_Right_Opnd);
pragma Inline (Is_Controlling_Actual);
pragma Inline (Is_Finalization_Wrapper);
pragma Inline (Is_Folded_In_Parser);
pragma Inline (Is_Generic_Contract_Pragma);
- pragma Inline (Is_Ghost_Pragma);
pragma Inline (Is_Ignored);
+ pragma Inline (Is_Ignored_Ghost_Pragma);
pragma Inline (Is_In_Discriminant_Check);
pragma Inline (Is_Inherited_Pragma);
pragma Inline (Is_Machine_Number);
pragma Inline (Set_Is_Asynchronous_Call_Block);
pragma Inline (Set_Is_Boolean_Aspect);
pragma Inline (Set_Is_Checked);
+ pragma Inline (Set_Is_Checked_Ghost_Pragma);
pragma Inline (Set_Is_Component_Left_Opnd);
pragma Inline (Set_Is_Component_Right_Opnd);
pragma Inline (Set_Is_Controlling_Actual);
pragma Inline (Set_Is_Finalization_Wrapper);
pragma Inline (Set_Is_Folded_In_Parser);
pragma Inline (Set_Is_Generic_Contract_Pragma);
- pragma Inline (Set_Is_Ghost_Pragma);
pragma Inline (Set_Is_Ignored);
+ pragma Inline (Set_Is_Ignored_Ghost_Pragma);
pragma Inline (Set_Is_In_Discriminant_Check);
pragma Inline (Set_Is_Inherited_Pragma);
pragma Inline (Set_Is_Machine_Number);
projects / gcc.git / commitdiff