+2015-01-07 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * alloc.ads Alphabetize several declarations. Add constants
+ Ignored_Ghost_Units_Initial and Ignored_Ghost_Units_Increment.
+ * atree.adb Add with and use clauses for Opt.
+ (Allocate_Initialize_Node): Mark a node as ignored Ghost
+ if it is created in an ignored Ghost region.
+ (Ekind_In): New variant.
+ (Is_Ignored_Ghost_Node): New routine.
+ (Set_Is_Ignored_Ghost_Node): New routine.
+ * atree.adb Aplhabetize several subprograms declarations. Flag
+ Spare0 is now known as Is_Ignored_Ghost_Node.
+ (Ekind_In): New variant.
+ (Is_Ignored_Ghost_Node): New routine.
+ (Set_Is_Ignored_Ghost_Node): New routine.
+ * einfo.adb: Flag 279 is now known as Contains_Ignored_Ghost_Code.
+ (Contains_Ignored_Ghost_Code): New routine.
+ (Set_Contains_Ignored_Ghost_Code): New routine.
+ (Set_Is_Checked_Ghost_Entity, Set_Is_Ignored_Ghost_Entity):
+ It is now possible to set this property on an unanalyzed entity.
+ (Write_Entity_Flags): Output the status of flag
+ Contains_Ignored_Ghost_Code.
+ * einfo.ads New attribute Contains_Ignored_Ghost_Code along with
+ usage in nodes.
+ (Contains_Ignored_Ghost_Code): New routine
+ along with pragma Inline.
+ (Set_Contains_Ignored_Ghost_Code): New routine along with pragma Inline.
+ * exp_ch3.adb Add with and use clauses for Ghost.
+ (Freeze_Type): Capture/restore the value of Ghost_Mode on entry/exit.
+ Set the Ghost_Mode in effect.
+ (Restore_Globals): New routine.
+ * exp_ch7.adb (Process_Declarations): Do not process a context
+ that invoves an ignored Ghost entity.
+ * exp_dbug.adb (Qualify_All_Entity_Names): Skip an ignored Ghost
+ construct that has been rewritten as a null statement.
+ * exp_disp.adb Add with and use clauses for Ghost.
+ (Make_DT): Capture/restore the value of Ghost_Mode on entry/exit. Set
+ the Ghost_Mode in effect.
+ (Restore_Globals): New routine.
+ * exp_util.adb (Requires_Cleanup_Actions): An ignored Ghost entity
+ does not require any clean up. Add two missing cases that deal
+ with block statements.
+ * freeze.adb Add with and use clauses for Ghost.
+ (Freeze_Entity): Capture/restore the value of Ghost_Mode on entry/exit.
+ Set the Ghost_Mode in effect.
+ (Restore_Globals): New routine.
+ * frontend.adb Add with and use clauses for Ghost. Remove any
+ ignored Ghost code from all units that qualify.
+ * ghost.adb New unit.
+ * ghost.ads New unit.
+ * gnat1drv.adb Add with clause for Ghost. Initialize and lock
+ the table in package Ghost.
+ * lib.ads: Alphabetize several subprogram declarations.
+ * lib-xref.adb (Output_References): Do not generate reference
+ information for ignored Ghost entities.
+ * opt.ads Add new type Ghost_Mode_Type and new global variable
+ Ghost_Mode.
+ * rtsfind.adb (Load_RTU): Provide a clean environment when
+ loading a runtime unit.
+ * sem.adb (Analyze): Capture/restore the value of Ghost_Mode on
+ entry/exit as the node may set a different mode.
+ (Do_Analyze):
+ Capture/restore the value of Ghost_Mode on entry/exit as the
+ unit may be withed from a unit with a different Ghost mode.
+ * sem_ch3.adb Add with and use clauses for Ghost.
+ (Analyze_Full_Type_Declaration, Analyze_Incomplete_Type_Decl,
+ Analyze_Number_Declaration, Analyze_Private_Extension_Declaration,
+ Analyze_Subtype_Declaration): Set the Ghost_Mode in effect. Mark
+ the entity as Ghost when there is a Ghost_Mode in effect.
+ (Array_Type_Declaration): The implicit base type inherits the
+ "ghostness" from the array type.
+ (Derive_Subprogram): The
+ alias inherits the "ghostness" from the parent subprogram.
+ (Make_Implicit_Base): The implicit base type inherits the
+ "ghostness" from the parent type.
+ * sem_ch5.adb Add with and use clauses for Ghost.
+ (Analyze_Assignment): Set the Ghost_Mode in effect.
+ * sem_ch6.adb Add with and use clauses for Ghost.
+ (Analyze_Abstract_Subprogram_Declaration, Analyze_Procedure_Call,
+ Analyze_Subprogram_Body_Helper, Analyze_Subprogram_Declaration):
+ Set the Ghost_Mode in effect. Mark the entity as Ghost when
+ there is a Ghost_Mode in effect.
+ * sem_ch7.adb Add with and use clauses for Ghost.
+ (Analyze_Package_Body_Helper, Analyze_Package_Declaration,
+ Analyze_Private_Type_Declaration): Set the Ghost_Mode in
+ effect. Mark the entity as Ghost when there is a Ghost_Mode
+ in effect.
+ * sem_ch8.adb Add with and use clauses for Ghost.
+ (Analyze_Exception_Renaming, Analyze_Generic_Renaming,
+ Analyze_Object_Renaming, Analyze_Package_Renaming,
+ Analyze_Subprogram_Renaming): Set the Ghost_Mode in effect. Mark
+ the entity as Ghost when there is a Ghost_Mode in effect.
+ (Find_Type): Check the Ghost context of a type.
+ * sem_ch11.adb Add with and use clauses for Ghost.
+ (Analyze_Exception_Declaration): Set the Ghost_Mode in
+ effect. Mark the entity as Ghost when there is a Ghost_Mode
+ in effect.
+ * sem_ch12.adb Add with and use clauses for Ghost.
+ (Analyze_Generic_Package_Declaration,
+ Analyze_Generic_Subprogram_Declaration): Set the Ghost_Mode in effect.
+ Mark the entity as Ghost when there is a Ghost_Mode in effect.
+ * sem_prag.adb Add with and use clauses for Ghost.
+ (Analyze_Pragma): Ghost-related checks are triggered when there
+ is a Ghost mode in effect.
+ (Create_Abstract_State): Mark the
+ entity as Ghost when there is a Ghost_Mode in effect.
+ * sem_res.adb Add with and use clauses for Ghost.
+ (Check_Ghost_Context): Removed.
+ * sem_util.adb (Check_Ghost_Completion): Removed.
+ (Check_Ghost_Derivation): Removed.
+ (Incomplete_Or_Partial_View):
+ Add a guard in case the entity has not been analyzed yet
+ and does carry a scope.
+ (Is_Declaration): New routine.
+ (Is_Ghost_Entity): Removed.
+ (Is_Ghost_Statement_Or_Pragma):
+ Removed.
+ (Is_Subject_To_Ghost): Removed.
+ (Set_Is_Ghost_Entity):
+ Removed.
+ (Within_Ghost_Scope): Removed.
+ * sem_util.adb (Check_Ghost_Completion): Removed.
+ (Check_Ghost_Derivation): Removed.
+ (Is_Declaration): New routine.
+ (Is_Ghost_Entity): Removed.
+ (Is_Ghost_Statement_Or_Pragma): Removed.
+ (Is_Subject_To_Ghost): Removed.
+ (Set_Is_Ghost_Entity): Removed.
+ (Within_Ghost_Scope): Removed.
+ * sinfo.ads Add a section on Ghost mode.
+ * treepr.adb (Print_Header_Flag): New routine.
+ (Print_Node_Header): Factor out code. Output flag
+ Is_Ignored_Ghost_Node.
+ * gcc-interface/Make-lang.in: Add dependency for unit Ghost.
+
2015-01-06 Eric Botcazou <ebotcazou@adacore.com>
* freeze.adb (Freeze_Array_Type) <Complain_CS>: Remove always
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2014, 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- --
File_Name_Chars_Initial : constant := 10_000; -- Osint
File_Name_Chars_Increment : constant := 100;
- Inlined_Bodies_Initial : constant := 50; -- Inline
- Inlined_Bodies_Increment : constant := 200;
+ In_Out_Warnings_Initial : constant := 100; -- Sem_Warn
+ In_Out_Warnings_Increment : constant := 100;
+
+ Ignored_Ghost_Units_Initial : constant := 20; -- Sem_Util
+ Ignored_Ghost_Units_Increment : constant := 50;
Inlined_Initial : constant := 100; -- Inline
Inlined_Increment : constant := 100;
- In_Out_Warnings_Initial : constant := 100; -- Sem_Warn
- In_Out_Warnings_Increment : constant := 100;
+ Inlined_Bodies_Initial : constant := 50; -- Inline
+ Inlined_Bodies_Increment : constant := 200;
Interp_Map_Initial : constant := 200; -- Sem_Type
Interp_Map_Increment : constant := 100;
with Aspects; use Aspects;
with Debug; use Debug;
with Nlists; use Nlists;
+with Opt; use Opt;
with Output; use Output;
with Sinput; use Sinput;
with Tree_IO; use Tree_IO;
then
New_Id := Src;
- else
- -- We are allocating a new node, or extending a node
- -- other than Nodes.Last.
+ -- We are allocating a new node, or extending a node other than
+ -- Nodes.Last.
+ else
if Present (Src) then
Nodes.Append (Nodes.Table (Src));
Flags.Append (Flags.Table (Src));
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;
+
-- Specifically copy Paren_Count to deal with creating new table entry
-- if the parentheses count is at the maximum possible value already.
T = V8;
end Ekind_In;
+ function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind) return Boolean
+ is
+ begin
+ return T = V1 or else
+ T = V2 or else
+ T = V3 or else
+ T = V4 or else
+ T = V5 or else
+ T = V6 or else
+ T = V7 or else
+ T = V8 or else
+ T = V9;
+ end Ekind_In;
+
function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8);
end Ekind_In;
+ function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind) return Boolean
+ is
+ begin
+ return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8, V9);
+ end Ekind_In;
+
------------------------
-- Set_Reporting_Proc --
------------------------
Set_Error_Posted (Error, True);
end Initialize;
+ ---------------------------
+ -- Is_Ignored_Ghost_Node --
+ ---------------------------
+
+ function Is_Ignored_Ghost_Node (N : Node_Id) return Boolean is
+ begin
+ return Flags.Table (N).Is_Ignored_Ghost_Node;
+ end Is_Ignored_Ghost_Node;
+
--------------------------
-- Is_Rewrite_Insertion --
--------------------------
Nodes.Table (N).Has_Aspects := Val;
end Set_Has_Aspects;
+ -------------------------------
+ -- Set_Is_Ignored_Ghost_Node --
+ -------------------------------
+
+ procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True) is
+ begin
+ Flags.Table (N).Is_Ignored_Ghost_Node := Val;
+ end Set_Is_Ignored_Ghost_Node;
+
-----------------------
-- Set_Original_Node --
-----------------------
-- The following functions return the contents of the indicated field of
-- the node referenced by the argument, which is a Node_Id.
- function Nkind (N : Node_Id) return Node_Kind;
- pragma Inline (Nkind);
-
function Analyzed (N : Node_Id) return Boolean;
pragma Inline (Analyzed);
- function Has_Aspects (N : Node_Id) return Boolean;
- pragma Inline (Has_Aspects);
-
function Comes_From_Source (N : Node_Id) return Boolean;
pragma Inline (Comes_From_Source);
function Error_Posted (N : Node_Id) return Boolean;
pragma Inline (Error_Posted);
- function Sloc (N : Node_Id) return Source_Ptr;
- pragma Inline (Sloc);
+ function Has_Aspects (N : Node_Id) return Boolean;
+ pragma Inline (Has_Aspects);
- function Paren_Count (N : Node_Id) return Nat;
- pragma Inline (Paren_Count);
+ function Is_Ignored_Ghost_Node
+ (N : Node_Id) return Boolean;
+ pragma Inline (Is_Ignored_Ghost_Node);
- function Parent (N : Node_Id) return Node_Id;
- pragma Inline (Parent);
- -- Returns the parent of a node if the node is not a list member, or else
- -- the parent of the list containing the node if the node is a list member.
+ function Nkind (N : Node_Id) return Node_Kind;
+ pragma Inline (Nkind);
function No (N : Node_Id) return Boolean;
pragma Inline (No);
-- Tests given Id for equality with the Empty node. This allows notations
-- like "if No (Variant_Part)" as opposed to "if Variant_Part = Empty".
+ function Parent (N : Node_Id) return Node_Id;
+ pragma Inline (Parent);
+ -- Returns the parent of a node if the node is not a list member, or else
+ -- the parent of the list containing the node if the node is a list member.
+
+ function Paren_Count (N : Node_Id) return Nat;
+ pragma Inline (Paren_Count);
+
function Present (N : Node_Id) return Boolean;
pragma Inline (Present);
-- Tests given Id for inequality with the Empty node. This allows notations
-- like "if Present (Statement)" as opposed to "if Statement /= Empty".
+ function Sloc (N : Node_Id) return Source_Ptr;
+ pragma Inline (Sloc);
+
---------------------
-- Node_Kind Tests --
---------------------
V7 : Entity_Kind;
V8 : Entity_Kind) return Boolean;
+ function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind) return Boolean;
+
function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V7 : Entity_Kind;
V8 : Entity_Kind) return Boolean;
+ function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind;
+ V9 : Entity_Kind) return Boolean;
+
pragma Inline (Ekind_In);
-- Inline all above functions
-- to be set in the specified field. Note that Set_Nkind is in the next
-- section, since its use is restricted.
- procedure Set_Sloc (N : Node_Id; Val : Source_Ptr);
- pragma Inline (Set_Sloc);
-
- procedure Set_Paren_Count (N : Node_Id; Val : Nat);
- pragma Inline (Set_Paren_Count);
-
- procedure Set_Parent (N : Node_Id; Val : Node_Id);
- pragma Inline (Set_Parent);
-
- procedure Set_Analyzed (N : Node_Id; Val : Boolean := True);
+ procedure Set_Analyzed (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Analyzed);
- procedure Set_Error_Posted (N : Node_Id; Val : Boolean := True);
- pragma Inline (Set_Error_Posted);
-
procedure Set_Comes_From_Source (N : Node_Id; Val : Boolean);
pragma Inline (Set_Comes_From_Source);
- -- Note that this routine is very rarely used, since usually the
- -- default mechanism provided sets the right value, but in some
- -- unusual cases, the value needs to be reset (e.g. when a source
- -- node is copied, and the copy must not have Comes_From_Source set).
+ -- Note that this routine is very rarely used, since usually the default
+ -- mechanism provided sets the right value, but in some unusual cases, the
+ -- value needs to be reset (e.g. when a source node is copied, and the copy
+ -- must not have Comes_From_Source set).
+
+ procedure Set_Error_Posted (N : Node_Id; Val : Boolean := True);
+ pragma Inline (Set_Error_Posted);
procedure Set_Has_Aspects (N : Node_Id; Val : Boolean := True);
pragma Inline (Set_Has_Aspects);
+ procedure Set_Is_Ignored_Ghost_Node (N : Node_Id; Val : Boolean := True);
+ pragma Inline (Set_Is_Ignored_Ghost_Node);
+
procedure Set_Original_Node (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Original_Node);
-- Note that this routine is used only in very peculiar cases. In normal
-- cases, the Original_Node link is set by calls to Rewrite. We currently
- -- use it in ASIS mode to manually set the link from pragma expressions
- -- to their aspect original source expressions, so that the original source
+ -- use it in ASIS mode to manually set the link from pragma expressions to
+ -- their aspect original source expressions, so that the original source
-- expressions accessed by ASIS are also semantically analyzed.
+ procedure Set_Parent (N : Node_Id; Val : Node_Id);
+ pragma Inline (Set_Parent);
+
+ procedure Set_Paren_Count (N : Node_Id; Val : Nat);
+ pragma Inline (Set_Paren_Count);
+
+ procedure Set_Sloc (N : Node_Id; Val : Source_Ptr);
+ pragma Inline (Set_Sloc);
+
------------------------------
-- Entity Update Procedures --
------------------------------
Flag1 : Boolean;
Flag2 : Boolean;
Flag3 : Boolean;
- Spare0 : Boolean;
+
+ Is_Ignored_Ghost_Node : Boolean;
+ -- Flag denothing whether the node is subject to pragma Ghost with
+ -- policy Ignore. The name of the flag should be Flag4, however this
+ -- requires changing the names of all remaining 300+ flags.
+
Spare1 : Boolean;
Spare2 : Boolean;
Spare3 : Boolean;
-- No_Dynamic_Predicate_On_Actual Flag276
-- Is_Checked_Ghost_Entity Flag277
-- Is_Ignored_Ghost_Entity Flag278
+ -- Contains_Ignored_Ghost_Code Flag279
- -- (unused) Flag279
-- (unused) Flag280
-- (unused) Flag281
return Node18 (Id);
end Entry_Index_Constant;
+ function Contains_Ignored_Ghost_Code (Id : E) return B is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Block,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Package,
+ E_Generic_Procedure,
+ E_Package,
+ E_Package_Body,
+ E_Procedure,
+ E_Subprogram_Body));
+ return Flag279 (Id);
+ end Contains_Ignored_Ghost_Code;
+
function Contract (Id : E) return N is
begin
pragma Assert
Set_Node20 (Id, V);
end Set_Component_Type;
+ procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Block,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Package,
+ E_Generic_Procedure,
+ E_Package,
+ E_Package_Body,
+ E_Procedure,
+ E_Subprogram_Body));
+ Set_Flag279 (Id, V);
+ end Set_Contains_Ignored_Ghost_Code;
+
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
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);
+ or else Ekind (Id) = E_Subprogram_Body
+
+ -- Allow this attribute to appear on non-analyzed entities
+
+ or else Ekind (Id) = E_Void);
Set_Flag277 (Id, V);
end Set_Is_Checked_Ghost_Entity;
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);
+ or else Ekind (Id) = E_Subprogram_Body
+
+ -- Allow this attribute to appear on non-analyzed entities
+
+ or else Ekind (Id) = E_Void);
Set_Flag278 (Id, V);
end Set_Is_Ignored_Ghost_Entity;
W ("C_Pass_By_Copy", Flag125 (Id));
W ("Can_Never_Be_Null", Flag38 (Id));
W ("Checks_May_Be_Suppressed", Flag31 (Id));
+ W ("Contains_Ignored_Ghost_Code", Flag279 (Id));
W ("Debug_Info_Off", Flag166 (Id));
W ("Default_Expressions_Processed", Flag108 (Id));
W ("Delay_Cleanups", Flag114 (Id));
-- Component_Type (Node20) [implementation base type only]
-- Defined in array types and string types. References component type.
+-- Contains_Ignored_Ghost_Code (Flag279)
+-- Defined in blocks, packages and their bodies, subprograms and their
+-- bodies. Set if the entity contains any ignored Ghost code in the form
+-- of declaration, procedure call, assignment statement or pragma.
+
-- Corresponding_Concurrent_Type (Node18)
-- Defined in record types that are constructed by the expander to
-- represent task and protected types (Is_Concurrent_Record_Type flag
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
-- Entry_Cancel_Parameter (Node23)
+ -- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Has_Master_Entity (Flag21)
-- Has_Biased_Representation (Flag139)
-- Has_Completion (Flag26) (constants only)
-- Has_Independent_Components (Flag34)
- -- Has_Thunks (Flag228) (constants only)
-- Has_Size_Clause (Flag29)
+ -- Has_Thunks (Flag228) (constants only)
-- Has_Up_Level_Access (Flag215)
-- Has_Volatile_Components (Flag87)
-- Is_Atomic (Flag85)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
- -- Elaboration_Entity_Required (Flag174)
+ -- Contains_Ignored_Ghost_Code (Flag279)
-- Default_Expressions_Processed (Flag108)
-- Delay_Cleanups (Flag114)
-- Delay_Subprogram_Descriptors (Flag50)
-- Discard_Names (Flag88)
+ -- Elaboration_Entity_Required (Flag174)
-- Has_Anonymous_Master (Flag253)
-- Has_Completion (Flag26)
-- Has_Controlling_Result (Flag98)
-- Contract (Node34)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
+ -- Contains_Ignored_Ghost_Code (Flag279)
-- Discard_Names (Flag88)
-- Elaboration_Entity_Required (Flag174)
-- Elaborate_Body_Desirable (Flag210) (non-generic case only)
-- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
-- Contract (Node34)
+ -- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
+ -- Contains_Ignored_Ghost_Code (Flag279)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Elaboration_Entity_Required (Flag174)
-- Scope_Depth_Value (Uint22)
-- Extra_Formals (Node28)
-- SPARK_Pragma (Node32)
- -- SPARK_Pragma_Inherited (Flag265)
-- Contract (Node34)
+ -- Contains_Ignored_Ghost_Code (Flag279)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- E_Subprogram_Type
function Component_Clause (Id : E) return N;
function Component_Size (Id : E) return U;
function Component_Type (Id : E) return E;
+ function Contains_Ignored_Ghost_Code (Id : E) return B;
function Contract (Id : E) return N;
function Corresponding_Concurrent_Type (Id : E) return E;
function Corresponding_Discriminant (Id : E) return E;
procedure Set_Component_Clause (Id : E; V : N);
procedure Set_Component_Size (Id : E; V : U);
procedure Set_Component_Type (Id : E; V : E);
+ procedure Set_Contains_Ignored_Ghost_Code (Id : E; V : B := True);
procedure Set_Contract (Id : E; V : N);
procedure Set_Corresponding_Concurrent_Type (Id : E; V : E);
procedure Set_Corresponding_Discriminant (Id : E; V : E);
pragma Inline (Component_Clause);
pragma Inline (Component_Size);
pragma Inline (Component_Type);
+ pragma Inline (Contains_Ignored_Ghost_Code);
pragma Inline (Contract);
pragma Inline (Corresponding_Concurrent_Type);
pragma Inline (Corresponding_Discriminant);
pragma Inline (Set_Component_Clause);
pragma Inline (Set_Component_Size);
pragma Inline (Set_Component_Type);
+ pragma Inline (Set_Contains_Ignored_Ghost_Code);
pragma Inline (Set_Contract);
pragma Inline (Set_Corresponding_Concurrent_Type);
pragma Inline (Set_Corresponding_Discriminant);
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;
-- node using Append_Freeze_Actions.
function Freeze_Type (N : Node_Id) return Boolean is
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect in case the type being frozen
+ -- sets a different mode.
+
+ procedure Restore_Globals;
+ -- Restore the values of all saved global variables
+
+ ---------------------
+ -- Restore_Globals --
+ ---------------------
+
+ procedure Restore_Globals is
+ begin
+ Ghost_Mode := GM;
+ end Restore_Globals;
+
+ -- Local variables
+
Def_Id : constant Entity_Id := Entity (N);
RACW_Seen : Boolean := False;
Result : Boolean := False;
+ -- Start of processing for Freeze_Type
+
begin
+ -- The type being frozen may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- freezing are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode_For_Freeze (Def_Id, N);
+
-- Process associated access types needing special processing
if Present (Access_Types_To_Process (N)) then
end if;
Freeze_Stream_Operations (N, Def_Id);
+
+ Restore_Globals;
return Result;
exception
when RE_Not_Available =>
+ Restore_Globals;
return False;
end Freeze_Type;
if Nkind (Decl) = N_Full_Type_Declaration then
Typ := Defining_Identifier (Decl);
- if Is_Tagged_Type (Typ)
+ -- Ignored Ghost types do not need any cleanup actions because
+ -- they will not appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Typ) then
+ null;
+
+ elsif Is_Tagged_Type (Typ)
and then Is_Library_Level_Entity (Typ)
and then Convention (Typ) = Convention_Ada
and then Present (Access_Disp_Table (Typ))
and then RTE_Available (RE_Register_Tag)
- and then not No_Run_Time_Mode
and then not Is_Abstract_Type (Typ)
+ and then not No_Run_Time_Mode
then
Processing_Actions;
end if;
elsif Is_Processed_Transient (Obj_Id) then
null;
+ -- Ignored Ghost objects do not need any cleanup actions
+ -- because they will not appear in the final tree.
+
+ elsif Is_Ignored_Ghost_Entity (Obj_Id) then
+ null;
+
-- The object is of the form:
-- Obj : Typ [:= Expr];
if For_Package and then Finalize_Storage_Only (Obj_Typ) then
null;
+ -- Ignored Ghost object renamings do not need any cleanup
+ -- actions because they will not appear in the final tree.
+
+ elsif Is_Ignored_Ghost_Entity (Obj_Id) then
+ null;
+
-- Return object of a build-in-place function. This case is
-- recognized and marked by the expansion of an extended return
-- statement (see Expand_N_Extended_Return_Statement).
then
Typ := Entity (Decl);
- if (Is_Access_Type (Typ)
- and then not Is_Access_Subprogram_Type (Typ)
- and then Needs_Finalization
- (Available_View (Designated_Type (Typ))))
- or else (Is_Type (Typ) and then Needs_Finalization (Typ))
+ -- Freeze nodes for ignored Ghost types do not need cleanup
+ -- actions because they will never appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Typ) then
+ null;
+
+ elsif (Is_Access_Type (Typ)
+ and then not Is_Access_Subprogram_Type (Typ)
+ and then Needs_Finalization
+ (Available_View (Designated_Type (Typ))))
+ or else (Is_Type (Typ) and then Needs_Finalization (Typ))
then
Old_Counter_Val := Counter_Val;
-- Nested package declarations, avoid generics
elsif Nkind (Decl) = N_Package_Declaration then
- Spec := Specification (Decl);
- Pack_Id := Defining_Unit_Name (Spec);
+ Pack_Id := Defining_Entity (Decl);
+ Spec := Specification (Decl);
- if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then
- Pack_Id := Defining_Identifier (Pack_Id);
- end if;
+ -- Do not inspect an ignored Ghost package because all code
+ -- found within will not appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Pack_Id) then
+ null;
- if Ekind (Pack_Id) /= E_Generic_Package then
+ elsif Ekind (Pack_Id) /= E_Generic_Package then
Old_Counter_Val := Counter_Val;
Process_Declarations
(Private_Declarations (Spec), Preprocess);
-- Nested package bodies, avoid generics
elsif Nkind (Decl) = N_Package_Body then
- Spec := Corresponding_Spec (Decl);
- if Ekind (Spec) /= E_Generic_Package then
+ -- Do not inspect an ignored Ghost package body because all
+ -- code found within will not appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then
+ null;
+
+ elsif Ekind (Corresponding_Spec (Decl)) /=
+ E_Generic_Package
+ then
Old_Counter_Val := Counter_Val;
Process_Declarations (Declarations (Decl), Preprocess);
procedure Qualify_All_Entity_Names is
E : Entity_Id;
Ent : Entity_Id;
+ Nod : Node_Id;
begin
for J in Name_Qualify_Units.First .. Name_Qualify_Units.Last loop
- E := Defining_Entity (Name_Qualify_Units.Table (J));
+ Nod := Name_Qualify_Units.Table (J);
+
+ -- When a scoping construct is ignored Ghost, it is rewritten as
+ -- a null statement. Skip such constructs as they no longer carry
+ -- names.
+
+ if Nkind (Nod) = N_Null_Statement then
+ goto Continue;
+ end if;
+
+ E := Defining_Entity (Nod);
Reset_Buffers;
Qualify_Entity_Name (E);
exit when Ent = E;
end loop;
end if;
+
+ <<Continue>>
+ null;
end loop;
end Qualify_All_Entity_Names;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Itypes; use Itypes;
with Layout; use Layout;
with Nlists; use Nlists;
-- end;
function Make_DT (Typ : Entity_Id; N : Node_Id := Empty) return List_Id is
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect in case the tagged type sets a
+ -- different mode.
+
Loc : constant Source_Ptr := Sloc (Typ);
Max_Predef_Prims : constant Int :=
-- this secondary dispatch table by Make_Tags when its unique external
-- name was generated.
+ procedure Restore_Globals;
+ -- Restore the values of all saved global variables
+
------------------------------
-- Check_Premature_Freezing --
------------------------------
Append_Elmt (Iface_DT, DT_Decl);
end Make_Secondary_DT;
+ ---------------------
+ -- Restore_Globals --
+ ---------------------
+
+ procedure Restore_Globals is
+ begin
+ Ghost_Mode := GM;
+ end Restore_Globals;
+
-- Local variables
Elab_Code : constant List_Id := New_List;
begin
pragma Assert (Is_Frozen (Typ));
+ -- The tagged type for which the dispatch table is being build may be
+ -- subject to pragma Ghost with policy Ignore. Set the mode now to
+ -- ensure that any nodes generated during freezing are properly flagged
+ -- as ignored Ghost.
+
+ Set_Ghost_Mode_For_Freeze (Typ, Typ);
+
-- Handle cases in which there is no need to build the dispatch table
if Has_Dispatch_Table (Typ)
or else Convention (Typ) = Convention_CIL
or else Convention (Typ) = Convention_Java
then
+ Restore_Globals;
return Result;
elsif No_Run_Time_Mode then
Error_Msg_CRT ("tagged types", Typ);
+ Restore_Globals;
return Result;
elsif not RTE_Available (RE_Tag) then
Analyze_List (Result, Suppress => All_Checks);
Error_Msg_CRT ("tagged types", Typ);
+ Restore_Globals;
return Result;
end if;
if RTE_Available (RE_Interface_Data) then
if Max_Predef_Prims /= 15 then
Error_Msg_N ("run-time library configuration error", Typ);
+ Restore_Globals;
return Result;
end if;
else
if Max_Predef_Prims /= 9 then
Error_Msg_N ("run-time library configuration error", Typ);
Error_Msg_CRT ("tagged types", Typ);
+ Restore_Globals;
return Result;
end if;
end if;
Register_CG_Node (Typ);
+ Restore_Globals;
return Result;
end Make_DT;
if Nkind (Decl) = N_Full_Type_Declaration then
Typ := Defining_Identifier (Decl);
- if Is_Tagged_Type (Typ)
+ -- Ignored Ghost types do not need any cleanup actions because
+ -- they will not appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Typ) then
+ null;
+
+ elsif Is_Tagged_Type (Typ)
and then Is_Library_Level_Entity (Typ)
and then Convention (Typ) = Convention_Ada
and then Present (Access_Disp_Table (Typ))
and then RTE_Available (RE_Unregister_Tag)
- and then not No_Run_Time_Mode
and then not Is_Abstract_Type (Typ)
+ and then not No_Run_Time_Mode
then
return True;
end if;
elsif Is_Processed_Transient (Obj_Id) then
null;
+ -- Ignored Ghost objects do not need any cleanup actions because
+ -- they will not appear in the final tree.
+
+ elsif Is_Ignored_Ghost_Entity (Obj_Id) then
+ null;
+
-- The object is of the form:
-- Obj : Typ [:= Expr];
--
if Lib_Level and then Finalize_Storage_Only (Obj_Typ) then
null;
+ -- Ignored Ghost object renamings do not need any cleanup actions
+ -- because they will not appear in the final tree.
+
+ elsif Is_Ignored_Ghost_Entity (Obj_Id) then
+ null;
+
-- Return object of a build-in-place function. This case is
-- recognized and marked by the expansion of an extended return
-- statement (see Expand_N_Extended_Return_Statement).
then
Typ := Entity (Decl);
- if ((Is_Access_Type (Typ)
- and then not Is_Access_Subprogram_Type (Typ)
- and then Needs_Finalization
- (Available_View (Designated_Type (Typ))))
- or else (Is_Type (Typ) and then Needs_Finalization (Typ)))
+ -- Freeze nodes for ignored Ghost types do not need cleanup
+ -- actions because they will never appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Typ) then
+ null;
+
+ elsif ((Is_Access_Type (Typ)
+ and then not Is_Access_Subprogram_Type (Typ)
+ and then Needs_Finalization
+ (Available_View (Designated_Type (Typ))))
+ or else (Is_Type (Typ) and then Needs_Finalization (Typ)))
and then Requires_Cleanup_Actions
(Actions (Decl), Lib_Level, Nested_Constructs)
then
elsif Nested_Constructs
and then Nkind (Decl) = N_Package_Declaration
then
- Pack_Id := Defining_Unit_Name (Specification (Decl));
+ Pack_Id := Defining_Entity (Decl);
- if Nkind (Pack_Id) = N_Defining_Program_Unit_Name then
- Pack_Id := Defining_Identifier (Pack_Id);
- end if;
+ -- Do not inspect an ignored Ghost package because all code found
+ -- within will not appear in the final tree.
- if Ekind (Pack_Id) /= E_Generic_Package
- and then
- Requires_Cleanup_Actions (Specification (Decl), Lib_Level)
+ if Is_Ignored_Ghost_Entity (Pack_Id) then
+ null;
+
+ elsif Ekind (Pack_Id) /= E_Generic_Package
+ and then Requires_Cleanup_Actions
+ (Specification (Decl), Lib_Level)
then
return True;
end if;
-- Nested package bodies
elsif Nested_Constructs and then Nkind (Decl) = N_Package_Body then
- Pack_Id := Corresponding_Spec (Decl);
- if Ekind (Pack_Id) /= E_Generic_Package
+ -- Do not inspect an ignored Ghost package body because all code
+ -- found within will not appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Defining_Entity (Decl)) then
+ null;
+
+ elsif Ekind (Corresponding_Spec (Decl)) /= E_Generic_Package
and then Requires_Cleanup_Actions (Decl, Lib_Level)
then
return True;
end if;
+
+ elsif Nkind (Decl) = N_Block_Statement
+ and then
+
+ -- Handle a rare case caused by a controlled transient variable
+ -- created as part of a record init proc. The variable is wrapped
+ -- in a block, but the block is not associated with a transient
+ -- scope.
+
+ (Inside_Init_Proc
+
+ -- Handle the case where the original context has been wrapped in
+ -- a block to avoid interference between exception handlers and
+ -- At_End handlers. Treat the block as transparent and process its
+ -- contents.
+
+ or else Is_Finalization_Wrapper (Decl))
+ then
+ if Requires_Cleanup_Actions (Decl, Lib_Level) then
+ return True;
+ end if;
end if;
Next (Decl);
with Exp_Pakd; use Exp_Pakd;
with Exp_Util; use Exp_Util;
with Exp_Tss; use Exp_Tss;
+with Ghost; use Ghost;
with Layout; use Layout;
with Lib; use Lib;
with Namet; use Namet;
-------------------
function Freeze_Entity (E : Entity_Id; N : Node_Id) return List_Id is
- Loc : constant Source_Ptr := Sloc (N);
- Comp : Entity_Id;
- F_Node : Node_Id;
- Indx : Node_Id;
- Formal : Entity_Id;
- Atype : Entity_Id;
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect in case the entity being frozen
+ -- sets a different mode.
+
+ Loc : constant Source_Ptr := Sloc (N);
+ Atype : Entity_Id;
+ Comp : Entity_Id;
+ F_Node : Node_Id;
+ Formal : Entity_Id;
+ Indx : Node_Id;
Test_E : Entity_Id := E;
-- This could use a comment ???
-- call, but rather must go in the package holding the function, so that
-- the backend can process it in the proper context.
+ procedure Restore_Globals;
+ -- Restore the values of all saved global variables
+
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-
Append_List (Result, Decls);
end Late_Freeze_Subprogram;
+ ---------------------
+ -- Restore_Globals --
+ ---------------------
+
+ procedure Restore_Globals is
+ begin
+ Ghost_Mode := GM;
+ end Restore_Globals;
+
------------------------------
-- Wrap_Imported_Subprogram --
------------------------------
-- Start of processing for Freeze_Entity
begin
+ -- The entity being frozen may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- freezing are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode_For_Freeze (E, N);
+
-- 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
-- record, that test actually applies to the record.
-- Do not freeze if already frozen since we only need one freeze node
if Is_Frozen (E) then
+ Restore_Globals;
return No_List;
-- It is improper to freeze an external entity within a generic because
Analyze_Aspects_At_Freeze_Point (E);
end if;
+ Restore_Globals;
return No_List;
-- AI05-0213: A formal incomplete type does not freeze the actual. In
and then No (Full_View (Base_Type (E)))
and then Ada_Version >= Ada_2012
then
+ Restore_Globals;
return No_List;
-- Formal subprograms are never frozen
elsif Is_Formal_Subprogram (E) then
+ Restore_Globals;
return No_List;
-- Generic types are never frozen as they lack delayed semantic checks
elsif Is_Generic_Type (E) then
+ Restore_Globals;
return No_List;
-- Do not freeze a global entity within an inner scope created during
then
exit;
else
+ Restore_Globals;
return No_List;
end if;
end if;
end loop;
if No (S) then
+ Restore_Globals;
return No_List;
end if;
end;
elsif Ekind (E) = E_Generic_Package then
- return Freeze_Generic_Entities (E);
+ Result := Freeze_Generic_Entities (E);
+
+ Restore_Globals;
+ return Result;
end if;
-- Add checks to detect proper initialization of scalars that may appear
if not Is_Internal (E) then
if not Freeze_Profile (E) then
+ Restore_Globals;
return Result;
end if;
end if;
if Late_Freezing then
Late_Freeze_Subprogram (E);
+ Restore_Globals;
return No_List;
end if;
and then not Has_Delayed_Freeze (E))
then
Check_Compile_Time_Size (E);
+ Restore_Globals;
return No_List;
end if;
if not Is_Frozen (Root_Type (E)) then
Set_Is_Frozen (E, False);
+ Restore_Globals;
return Result;
end if;
and then not Present (Full_View (E))
then
Set_Is_Frozen (E, False);
+ Restore_Globals;
return Result;
-- Case of full view present
Set_RM_Size (E, RM_Size (Full_View (E)));
end if;
+ Restore_Globals;
return Result;
-- Case of underlying full view present
Check_Debug_Info_Needed (E);
+ Restore_Globals;
return Result;
-- Case of no full view present. If entity is derived or subtype,
else
Set_Is_Frozen (E, False);
+ Restore_Globals;
return No_List;
end if;
-- generic processing), so we never need freeze nodes for them.
if Is_Generic_Type (E) then
+ Restore_Globals;
return Result;
end if;
end if;
end if;
+ Restore_Globals;
return Result;
end Freeze_Entity;
with Exp_Dbug;
with Fmap;
with Fname.UF;
+with Ghost; use Ghost;
with Inline; use Inline;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
Analyze_Inlined_Bodies;
end if;
- -- Remove entities from program that do not have any
- -- execution time references.
+ -- Remove entities from program that do not have any execution
+ -- time references.
if Debug_Flag_UU then
Collect_Garbage_Entities;
end if;
Check_Elab_Calls;
+
+ -- Remove any ignored Ghost code as it must not appear in the
+ -- executable.
+
+ Remove_Ignored_Ghost_Code;
end if;
-- List library units if requested
ada/g-u3spch.o \
ada/get_spark_xrefs.o \
ada/get_targ.o \
+ ada/ghost.o \
ada/gnat.o \
ada/gnatvsn.o \
ada/hostparm.o \
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- G H O S T --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2014-2015, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+with Alloc; use Alloc;
+with Aspects; use Aspects;
+with Atree; use Atree;
+with Einfo; use Einfo;
+with Elists; use Elists;
+with Errout; use Errout;
+with Lib; use Lib;
+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_Eval; use Sem_Eval;
+with Sem_Res; use Sem_Res;
+with Sem_Util; use Sem_Util;
+with Sinfo; use Sinfo;
+with Snames; use Snames;
+with Table;
+
+package body Ghost is
+
+ -- The following table contains the N_Compilation_Unit node for a unit that
+ -- is either subject to pragma Ghost with policy Ignore or contains ignored
+ -- Ghost code. The table is used in the removal of ignored Ghost code from
+ -- units.
+
+ package Ignored_Ghost_Units is new Table.Table (
+ Table_Component_Type => Node_Id,
+ Table_Index_Type => Int,
+ Table_Low_Bound => 0,
+ Table_Initial => Alloc.Ignored_Ghost_Units_Initial,
+ Table_Increment => Alloc.Ignored_Ghost_Units_Increment,
+ Table_Name => "Ignored_Ghost_Units");
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
+ -- Subsidiary to Set_Ghost_Mode_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.
+
+ ----------------------------
+ -- Add_Ignored_Ghost_Unit --
+ ----------------------------
+
+ procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
+ begin
+ pragma Assert (Nkind (Unit) = N_Compilation_Unit);
+
+ -- Avoid duplicates in the table as pruning the same unit more than once
+ -- is wasteful. Since ignored Ghost code tends to be grouped up, check
+ -- the contents of the table in reverse.
+
+ for Index in reverse Ignored_Ghost_Units.First ..
+ Ignored_Ghost_Units.Last
+ loop
+ -- The unit is already present in the table, do not add it again
+
+ if Unit = Ignored_Ghost_Units.Table (Index) then
+ return;
+ end if;
+ end loop;
+
+ -- If we get here, then this is the first time the unit is being added
+
+ Ignored_Ghost_Units.Append (Unit);
+ end Add_Ignored_Ghost_Unit;
+
+ ----------------------------
+ -- Check_Ghost_Completion --
+ ----------------------------
+
+ procedure Check_Ghost_Completion
+ (Partial_View : Entity_Id;
+ Full_View : Entity_Id)
+ is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ -- The Ghost policy in effect at the point of declaration and at the
+ -- point of completion must match (SPARK RM 6.9(15)).
+
+ if Is_Checked_Ghost_Entity (Partial_View)
+ and then Policy = Name_Ignore
+ then
+ Error_Msg_Sloc := Sloc (Full_View);
+
+ 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);
+
+ elsif Is_Ignored_Ghost_Entity (Partial_View)
+ and then Policy = Name_Check
+ then
+ Error_Msg_Sloc := Sloc (Full_View);
+
+ 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);
+ end if;
+ end Check_Ghost_Completion;
+
+ -------------------------
+ -- Check_Ghost_Context --
+ -------------------------
+
+ procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
+ procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
+ -- Verify that the Ghost policy at the point of declaration of entity Id
+ -- matches the policy at the point of reference. If this is not the case
+ -- emit an error at Err_N.
+
+ function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
+ -- Determine whether node Context denotes a Ghost-friendly context where
+ -- a Ghost entity can safely reside.
+
+ -------------------------
+ -- Is_OK_Ghost_Context --
+ -------------------------
+
+ function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
+ function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
+ -- Determine whether node Decl is a Ghost declaration or appears
+ -- within a Ghost declaration.
+
+ function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
+ -- Determine whether statement or pragma N is Ghost or appears within
+ -- a Ghost statement or pragma. To qualify as such, N must either
+ -- 1) Occur within a ghost subprogram or package
+ -- 2) Denote a call to a ghost procedure
+ -- 3) Denote an assignment statement whose target is a ghost
+ -- variable.
+ -- 4) Denote a pragma that mentions a ghost entity
+
+ --------------------------
+ -- Is_Ghost_Declaration --
+ --------------------------
+
+ function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
+ Par : Node_Id;
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ begin
+ -- Climb the parent chain looking for an object declaration
+
+ Par := Decl;
+ while Present (Par) loop
+ if Is_Declaration (Par) then
+
+ -- A declaration is Ghost when it appears within a Ghost
+ -- package or subprogram.
+
+ if Ghost_Mode > None then
+ return True;
+
+ -- Otherwise the declaration may not have been analyzed yet,
+ -- determine whether it is subject to aspect/pragma Ghost.
+
+ else
+ return Is_Subject_To_Ghost (Par);
+ end if;
+
+ -- Special cases
+
+ -- A reference to a Ghost entity may appear as the default
+ -- expression of a formal parameter of a subprogram body. This
+ -- context must be treated as suitable because the relation
+ -- between the spec and the body has not been established and
+ -- the body is not marked as Ghost yet. The real check was
+ -- performed on the spec.
+
+ elsif Nkind (Par) = N_Parameter_Specification
+ and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
+ then
+ return True;
+
+ -- References to Ghost entities may be relocated in internally
+ -- generated bodies.
+
+ elsif Nkind (Par) = N_Subprogram_Body
+ and then not Comes_From_Source (Par)
+ then
+ Subp_Id := Corresponding_Spec (Par);
+
+ -- The original context is an expression function that has
+ -- been split into a spec and a body. The context is OK as
+ -- long as the the initial declaration is Ghost.
+
+ if Present (Subp_Id) then
+ Subp_Decl :=
+ Original_Node (Unit_Declaration_Node (Subp_Id));
+
+ if Nkind (Subp_Decl) = N_Expression_Function then
+ return Is_Subject_To_Ghost (Subp_Decl);
+ end if;
+ end if;
+
+ -- Otherwise this is either an internal body or an internal
+ -- completion. Both are OK because the real check was done
+ -- before expansion activities.
+
+ return True;
+ end if;
+
+ -- Prevent the search from going too far
+
+ if Is_Body_Or_Package_Declaration (Par) then
+ return False;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end Is_Ghost_Declaration;
+
+ ----------------------------------
+ -- Is_Ghost_Statement_Or_Pragma --
+ ----------------------------------
+
+ function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
+ function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
+ -- Determine whether an arbitrary node denotes a reference to a
+ -- Ghost entity.
+
+ -------------------------------
+ -- Is_Ghost_Entity_Reference --
+ -------------------------------
+
+ function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
+ Ref : Node_Id;
+
+ begin
+ Ref := N;
+
+ -- When the reference extracts a subcomponent, recover the
+ -- related object (SPARK RM 6.9(1)).
+
+ while Nkind_In (Ref, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component,
+ N_Slice)
+ loop
+ Ref := Prefix (Ref);
+ end loop;
+
+ return
+ Is_Entity_Name (Ref)
+ and then Present (Entity (Ref))
+ and then Is_Ghost_Entity (Entity (Ref));
+ end Is_Ghost_Entity_Reference;
+
+ -- Local variables
+
+ Arg : Node_Id;
+ Stmt : Node_Id;
+
+ -- Start of processing for Is_Ghost_Statement_Or_Pragma
+
+ begin
+ if Nkind (N) = N_Pragma then
+
+ -- A pragma is Ghost when it appears within a Ghost package or
+ -- subprogram.
+
+ if Ghost_Mode > None then
+ return True;
+ end if;
+
+ -- A pragma is Ghost when it mentions a Ghost entity
+
+ Arg := First (Pragma_Argument_Associations (N));
+ while Present (Arg) loop
+ if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
+ return True;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+
+ Stmt := N;
+ while Present (Stmt) loop
+ if Is_Statement (Stmt) then
+
+ -- A statement is Ghost when it appears within a Ghost
+ -- package or subprogram.
+
+ if Ghost_Mode > None then
+ return True;
+
+ -- An assignment statement or a procedure call is Ghost when
+ -- the name denotes a Ghost entity.
+
+ elsif Nkind_In (Stmt, N_Assignment_Statement,
+ N_Procedure_Call_Statement)
+ then
+ return Is_Ghost_Entity_Reference (Name (Stmt));
+ end if;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
+ return False;
+ end if;
+
+ Stmt := Parent (Stmt);
+ end loop;
+
+ return False;
+ end Is_Ghost_Statement_Or_Pragma;
+
+ -- Start of processing for Is_OK_Ghost_Context
+
+ begin
+ -- The Ghost entity appears within an assertion expression
+
+ if In_Assertion_Expr > 0 then
+ return True;
+
+ -- The Ghost entity is part of a declaration or its completion
+
+ elsif Is_Ghost_Declaration (Context) then
+ return True;
+
+ -- The Ghost entity is referenced within a Ghost statement
+
+ elsif Is_Ghost_Statement_Or_Pragma (Context) then
+ return True;
+
+ -- Routine Expand_Record_Extension creates a parent subtype without
+ -- inserting it into the tree. There is no good way of recognizing
+ -- this special case as there is no parent. Try to approximate the
+ -- context.
+
+ elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
+ return True;
+
+ else
+ return False;
+ end if;
+ end Is_OK_Ghost_Context;
+
+ ------------------------
+ -- Check_Ghost_Policy --
+ ------------------------
+
+ procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ -- The Ghost policy in effect a the point of declaration and at the
+ -- point of use must match (SPARK RM 6.9(14)).
+
+ if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
+ Error_Msg_Sloc := Sloc (Err_N);
+
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+
+ elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
+ Error_Msg_Sloc := Sloc (Err_N);
+
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+ end if;
+ end Check_Ghost_Policy;
+
+ -- Start of processing for Check_Ghost_Context
+
+ begin
+ -- Once it has been established that the reference to the Ghost entity
+ -- is within a suitable context, ensure that the policy at the point of
+ -- declaration and at the point of use match.
+
+ if Is_OK_Ghost_Context (Ghost_Ref) then
+ Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+
+ -- Otherwise the Ghost entity appears in a non-Ghost context and affects
+ -- its behavior or value.
+
+ else
+ Error_Msg_N
+ ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
+ Ghost_Ref);
+ end if;
+ end Check_Ghost_Context;
+
+ ----------------------------
+ -- Check_Ghost_Derivation --
+ ----------------------------
+
+ procedure Check_Ghost_Derivation (Typ : Entity_Id) is
+ Parent_Typ : constant Entity_Id := Etype (Typ);
+ Iface : Entity_Id;
+ Iface_Elmt : Elmt_Id;
+
+ begin
+ -- Allow untagged derivations from predefined types such as Integer as
+ -- those are not Ghost by definition.
+
+ if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
+ null;
+
+ -- The parent type of a Ghost type extension must be Ghost
+
+ elsif not Is_Ghost_Entity (Parent_Typ) then
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
+ return;
+ end if;
+
+ -- All progenitors (if any) must be Ghost as well
+
+ if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
+ Iface_Elmt := First_Elmt (Interfaces (Typ));
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
+
+ if not Is_Ghost_Entity (Iface) then
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
+ return;
+ end if;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end if;
+ end Check_Ghost_Derivation;
+
+ --------------------------------
+ -- Implements_Ghost_Interface --
+ --------------------------------
+
+ function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
+ Iface_Elmt : Elmt_Id;
+
+ begin
+ -- Traverse the list of interfaces looking for a Ghost interface
+
+ if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
+ Iface_Elmt := First_Elmt (Interfaces (Typ));
+ while Present (Iface_Elmt) loop
+ if Is_Ghost_Entity (Node (Iface_Elmt)) then
+ return True;
+ end if;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Implements_Ghost_Interface;
+
+ ----------------
+ -- Initialize --
+ ----------------
+
+ procedure Initialize is
+ begin
+ Ignored_Ghost_Units.Init;
+ end Initialize;
+
+ ---------------------
+ -- Is_Ghost_Entity --
+ ---------------------
+
+ function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
+ begin
+ return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
+ end Is_Ghost_Entity;
+
+ -------------------------
+ -- Is_Subject_To_Ghost --
+ -------------------------
+
+ function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
+ function Enables_Ghostness (Arg : Node_Id) return Boolean;
+ -- Determine whether aspect or pragma argument Arg enables "ghostness"
+
+ -----------------------
+ -- Enables_Ghostness --
+ -----------------------
+
+ function Enables_Ghostness (Arg : Node_Id) return Boolean is
+ Expr : Node_Id;
+
+ begin
+ Expr := Arg;
+
+ if Nkind (Expr) = N_Pragma_Argument_Association then
+ Expr := Get_Pragma_Arg (Expr);
+ end if;
+
+ -- Determine whether the expression of the aspect is static and
+ -- denotes True.
+
+ if Present (Expr) then
+ Preanalyze_And_Resolve (Expr);
+
+ return
+ Is_OK_Static_Expression (Expr)
+ and then Is_True (Expr_Value (Expr));
+
+ -- Otherwise Ghost defaults to True
+
+ else
+ return True;
+ end if;
+ end Enables_Ghostness;
+
+ -- Local variables
+
+ Id : constant Entity_Id := Defining_Entity (N);
+ Asp : Node_Id;
+ Decl : Node_Id;
+ Prev_Id : Entity_Id;
+
+ -- Start of processing for Is_Subject_To_Ghost
+
+ begin
+ -- The related entity of the declaration has not been analyzed yet, do
+ -- not inspect its attributes.
+
+ if Ekind (Id) = E_Void then
+ null;
+
+ elsif Is_Ghost_Entity (Id) then
+ return True;
+
+ -- The completion of a type or a constant is not fully analyzed when the
+ -- reference to the Ghost entity is resolved. Because the completion is
+ -- not marked as Ghost yet, inspect the partial view.
+
+ elsif Is_Record_Type (Id)
+ or else Ekind (Id) = E_Constant
+ or else (Nkind (N) = N_Object_Declaration
+ and then Constant_Present (N))
+ then
+ Prev_Id := Incomplete_Or_Partial_View (Id);
+
+ if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
+ return True;
+ end if;
+ end if;
+
+ -- Examine the aspect specifications (if any) looking for aspect Ghost
+
+ if Permits_Aspect_Specifications (N) then
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ if Chars (Identifier (Asp)) = Name_Ghost then
+ return Enables_Ghostness (Expression (Asp));
+ end if;
+
+ Next (Asp);
+ end loop;
+ end if;
+
+ Decl := Empty;
+
+ -- When the context is a [generic] package declaration, pragma Ghost
+ -- resides in the visible declarations.
+
+ if Nkind_In (N, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Decl := First (Visible_Declarations (Specification (N)));
+
+ -- When the context is a package or a subprogram body, pragma Ghost
+ -- resides in the declarative part.
+
+ elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
+ Decl := First (Declarations (N));
+
+ -- Otherwise pragma Ghost appears in the declarations following N
+
+ elsif Is_List_Member (N) then
+ Decl := Next (N);
+ end if;
+
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma
+ and then Pragma_Name (Decl) = Name_Ghost
+ then
+ return
+ Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
+
+ -- A source construct ends the region where pragma Ghost may appear,
+ -- stop the traversal.
+
+ elsif Comes_From_Source (Decl) then
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ return False;
+ end Is_Subject_To_Ghost;
+
+ ----------
+ -- Lock --
+ ----------
+
+ procedure Lock is
+ begin
+ Ignored_Ghost_Units.Locked := True;
+ Ignored_Ghost_Units.Release;
+ end Lock;
+
+ ----------------------------------
+ -- Propagate_Ignored_Ghost_Code --
+ ----------------------------------
+
+ procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
+ Nod : Node_Id;
+ Scop : Entity_Id;
+
+ begin
+ -- Traverse the parent chain looking for blocks, packages and
+ -- subprograms or their respective bodies.
+
+ Nod := Parent (N);
+ while Present (Nod) loop
+ Scop := Empty;
+
+ if Nkind (Nod) = N_Block_Statement then
+ Scop := Entity (Identifier (Nod));
+
+ elsif Nkind_In (Nod, N_Package_Body,
+ N_Package_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Declaration)
+ then
+ Scop := Defining_Entity (Nod);
+ end if;
+
+ -- The current node denotes a scoping construct
+
+ if Present (Scop) then
+
+ -- Stop the traversal when the scope already contains ignored
+ -- Ghost code as all enclosing scopes have already been marked.
+
+ if Contains_Ignored_Ghost_Code (Scop) then
+ exit;
+
+ -- Otherwise mark this scope and keep climbing
+
+ else
+ Set_Contains_Ignored_Ghost_Code (Scop);
+ end if;
+ end if;
+
+ Nod := Parent (Nod);
+ end loop;
+
+ -- The unit containing the ignored Ghost code must be post processed
+ -- before invoking the back end.
+
+ Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
+ end Propagate_Ignored_Ghost_Code;
+
+ -------------------------------
+ -- Remove_Ignored_Ghost_Code --
+ -------------------------------
+
+ procedure Remove_Ignored_Ghost_Code is
+ procedure Prune_Tree (Root : Node_Id);
+ -- Remove all code marked as ignored Ghost from the tree of denoted by
+ -- Root.
+
+ ----------------
+ -- Prune_Tree --
+ ----------------
+
+ procedure Prune_Tree (Root : Node_Id) is
+ procedure Prune (N : Node_Id);
+ -- Remove a given node from the tree by rewriting it into null
+
+ function Prune_Node (N : Node_Id) return Traverse_Result;
+ -- Determine whether node N denotes an ignored Ghost construct. If
+ -- this is the case, rewrite N as a null statement. See the body for
+ -- special cases.
+
+ -----------
+ -- Prune --
+ -----------
+
+ procedure Prune (N : Node_Id) is
+ begin
+ -- Destroy any aspects that may be associated with the node
+
+ if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
+ Remove_Aspects (N);
+ end if;
+
+ Rewrite (N, Make_Null_Statement (Sloc (N)));
+ end Prune;
+
+ ----------------
+ -- Prune_Node --
+ ----------------
+
+ function Prune_Node (N : Node_Id) return Traverse_Result is
+ Id : Entity_Id;
+
+ begin
+ -- The node is either declared as ignored Ghost or is a byproduct
+ -- of expansion. Destroy it and stop the traversal on this branch.
+
+ if Is_Ignored_Ghost_Node (N) then
+ Prune (N);
+ return Skip;
+
+ -- Scoping constructs such as blocks, packages, subprograms and
+ -- bodies offer some flexibility with respect to pruning.
+
+ elsif Nkind_In (N, N_Block_Statement,
+ N_Package_Body,
+ N_Package_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Declaration)
+ then
+ if Nkind (N) = N_Block_Statement then
+ Id := Entity (Identifier (N));
+ else
+ Id := Defining_Entity (N);
+ end if;
+
+ -- The scoping construct contains both living and ignored Ghost
+ -- code, let the traversal prune all relevant nodes.
+
+ if Contains_Ignored_Ghost_Code (Id) then
+ return OK;
+
+ -- Otherwise the construct contains only living code and should
+ -- not be pruned.
+
+ else
+ return Skip;
+ end if;
+
+ -- Otherwise keep searching for ignored Ghost nodes
+
+ else
+ return OK;
+ end if;
+ end Prune_Node;
+
+ procedure Prune_Nodes is new Traverse_Proc (Prune_Node);
+
+ -- Start of processing for Prune_Tree
+
+ begin
+ Prune_Nodes (Root);
+ end Prune_Tree;
+
+ -- Start of processing for Remove_Ignored_Ghost_Code
+
+ begin
+ for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
+ Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
+ end loop;
+ end Remove_Ignored_Ghost_Code;
+
+ --------------------
+ -- Set_Ghost_Mode --
+ --------------------
+
+ procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty) is
+ procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id);
+ -- Set the value of global variable Ghost_Mode depending on the mode of
+ -- entity Id.
+
+ procedure Set_Ghost_Mode_From_Policy;
+ -- Set the value of global variable Ghost_Mode depending on the current
+ -- Ghost policy in effect.
+
+ --------------------------------
+ -- 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;
+
+ Set_Is_Ignored_Ghost_Node (N);
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end Set_Ghost_Mode_From_Entity;
+
+ --------------------------------
+ -- Set_Ghost_Mode_From_Policy --
+ --------------------------------
+
+ procedure Set_Ghost_Mode_From_Policy is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ 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);
+ end if;
+ end Set_Ghost_Mode_From_Policy;
+
+ -- Local variables
+
+ Nam : Node_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_Ghost_Mode_From_Policy;
+
+ -- The declaration denotes the completion of a deferred constant,
+ -- pragma Ghost appears on the partial declaration.
+
+ elsif Nkind (N) = N_Object_Declaration
+ and then Constant_Present (N)
+ and then Present (Prev_Id)
+ then
+ Set_Ghost_Mode_From_Entity (Prev_Id);
+
+ -- The declaration denotes the full view of a private type, pragma
+ -- Ghost appears on the partial declaration.
+
+ elsif Nkind (N) = N_Full_Type_Declaration
+ and then Is_Private_Type (Defining_Entity (N))
+ and then Present (Prev_Id)
+ then
+ Set_Ghost_Mode_From_Entity (Prev_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.
+
+ elsif Nkind_In (N, N_Assignment_Statement,
+ N_Procedure_Call_Statement)
+ then
+ Nam := Name (N);
+
+ -- When the reference extracts a subcomponent, recover the related
+ -- object (SPARK RM 6.9(1)).
+
+ while Nkind_In (Nam, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component,
+ N_Slice)
+ loop
+ Nam := Prefix (Nam);
+ end loop;
+
+ if Is_Entity_Name (Nam)
+ and then Present (Entity (Nam))
+ then
+ Set_Ghost_Mode_From_Entity (Entity (Nam));
+ end if;
+
+ -- The input denotes a package or subprogram body
+
+ elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
+ if (Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id))
+ or else Is_Subject_To_Ghost (N)
+ then
+ Set_Ghost_Mode_From_Policy;
+ end if;
+ end if;
+ end Set_Ghost_Mode;
+
+ -------------------------------
+ -- Set_Ghost_Mode_For_Freeze --
+ -------------------------------
+
+ procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id) is
+ begin
+ if Is_Checked_Ghost_Entity (Id) then
+ Ghost_Mode := Check;
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Ghost_Mode := Ignore;
+
+ Propagate_Ignored_Ghost_Code (N);
+ end if;
+ end Set_Ghost_Mode_For_Freeze;
+
+ -------------------------
+ -- Set_Is_Ghost_Entity --
+ -------------------------
+
+ procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
+ Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+ begin
+ if Policy = Name_Check then
+ Set_Is_Checked_Ghost_Entity (Id);
+
+ elsif Policy = Name_Ignore then
+ Set_Is_Ignored_Ghost_Entity (Id);
+ end if;
+ end Set_Is_Ghost_Entity;
+
+end Ghost;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- G H O S T --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2014-2015, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+-- This package contains routines that deal with the static and runtime
+-- semantics of Ghost entities.
+
+with Types; use Types;
+
+package Ghost is
+
+ procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
+ -- Add a single ignored Ghost compilation unit to the internal table for
+ -- 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);
+ -- Determine whether node Ghost_Ref appears within a Ghost-friendly context
+ -- where Ghost entity Ghost_Id can safely reside.
+
+ procedure Check_Ghost_Derivation (Typ : Entity_Id);
+ -- Verify that the parent type and all progenitors of derived type or type
+ -- extension Typ are Ghost. If this is not the case, issue an error.
+
+ function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ implements at least one Ghost interface
+
+ procedure Initialize;
+ -- Initialize internal tables
+
+ function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
+ -- Determine whether entity Id is Ghost. To qualify as such, the entity
+ -- must be subject to pragma Ghost.
+
+ function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
+ -- Determine whether declarative node 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.
+
+ procedure Lock;
+ -- Lock internal tables before calling backend
+
+ procedure Remove_Ignored_Ghost_Code;
+ -- Remove all code marked as ignored Ghost from the trees of all qualifying
+ -- units.
+ --
+ -- WARNING: this is a separate front end pass, care should be taken to keep
+ -- it optimized.
+
+ procedure Set_Ghost_Mode (N : Node_Id; Prev_Id : Entity_Id := Empty);
+ -- Set the value of global variable Ghost_Mode depending on the following
+ -- scenarios:
+ --
+ -- 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:
+ --
+ -- N is the completion of a deferred constant, Prev_Id denotes the
+ -- entity of the partial declaration.
+ --
+ -- N is the full view of a private type, Prev_Id denotes the entity
+ -- of the partial declaration.
+ --
+ -- If N is an assignment statement or a procedure call, determine whether
+ -- the name of N denotes a reference to a Ghost entity. If this is the
+ -- case, the Global_Mode is set based on the mode of the name.
+ --
+ -- If N denotes a package or a subprogram body, determine whether the
+ -- corresponding spec Prev_Id is a Ghost entity or the body is subject
+ -- to pragma Ghost. If this is the case, the Global_Mode is set based on
+ -- the current Ghost policy in effect.
+ --
+ -- 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.
+
+ procedure Set_Ghost_Mode_For_Freeze (Id : Entity_Id; N : Node_Id);
+ -- Set the value of global variable Ghost_Mode depending on the mode of
+ -- entity Id. N denotes the context of the freeze.
+ --
+ -- 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.
+
+ procedure Set_Is_Ghost_Entity (Id : Entity_Id);
+ -- Set the relevant ghost attribute of entity Id depending on the current
+ -- Ghost assertion policy in effect.
+
+end Ghost;
with Fname; use Fname;
with Fname.UF; use Fname.UF;
with Frontend;
+with Ghost;
with Gnatvsn; use Gnatvsn;
with Inline;
with Lib; use Lib;
Lib.Xref.Initialize;
Scan_Compiler_Arguments;
Osint.Add_Default_Search_Dirs;
-
Atree.Initialize;
Nlists.Initialize;
Sinput.Initialize;
SCOs.Initialize;
Snames.Initialize;
Stringt.Initialize;
+ Ghost.Initialize;
Inline.Initialize;
Par_SCO.Initialize;
Sem_Ch8.Initialize;
Atree.Lock;
Elists.Lock;
Fname.UF.Lock;
+ Ghost.Lock;
Inline.Lock;
Lib.Lock;
+ Namet.Lock;
Nlists.Lock;
Sem.Lock;
Sinput.Lock;
- Namet.Lock;
Stringt.Lock;
-- Here we call the back end to generate the output code
J := 1;
while J <= Xrefs.Last loop
Ent := Xrefs.Table (J).Key.Ent;
+
+ -- Do not generate reference information for an ignored Ghost
+ -- entity because neither the entity nor its references will
+ -- appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Ent) then
+ goto Orphan_Continue;
+ end if;
+
Get_Type_Reference (Ent, Tref, L, R);
if Present (Tref)
end;
end if;
+ <<Orphan_Continue>>
J := J + 1;
end loop;
end Handle_Orphan_Type_References;
-- references, so we can sort them, and output them.
Output_Refs : declare
-
Nrefs : constant Nat := Xrefs.Last;
-- Number of references in table
begin
Ent := XE.Key.Ent;
+
+ -- Do not generate reference information for an ignored Ghost
+ -- entity because neither the entity nor its references will
+ -- appear in the final tree.
+
+ if Is_Ignored_Ghost_Entity (Ent) then
+ goto Continue;
+ end if;
+
Ctyp := Xref_Entity_Letters (Ekind (Ent));
-- Skip reference if it is the only reference to an entity,
-- do not have an entry for each possible field, since some of the fields
-- can only be set by specialized interfaces (defined below).
- function Version_Get (U : Unit_Number_Type) return Word_Hex_String;
- -- Returns the version as a string with 8 hex digits (upper case letters)
+ function Compilation_Switches_Last return Nat;
+ -- Return the count of stored compilation switches
- function Last_Unit return Unit_Number_Type;
- -- Unit number of last allocated unit
+ procedure Disable_Switch_Storing;
+ -- Disable registration of switches by Store_Compilation_Switch. Used to
+ -- avoid registering switches added automatically by the gcc driver at the
+ -- end of the command line.
- function Num_Units return Nat;
- -- Number of units currently in unit table
+ function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
+ -- Given two Sloc values for which In_Same_Extended_Unit is true, determine
+ -- if S1 appears before S2. Returns True if S1 appears before S2, and False
+ -- otherwise. The result is undefined if S1 and S2 are not in the same
+ -- extended unit. Note: this routine will not give reliable results if
+ -- called after Sprint has been called with -gnatD set.
- procedure Remove_Unit (U : Unit_Number_Type);
- -- Remove unit U from unit table. Currently this is effective only
- -- if U is the last unit currently stored in the unit table.
+ procedure Enable_Switch_Storing;
+ -- Enable registration of switches by Store_Compilation_Switch. Used to
+ -- avoid registering switches added automatically by the gcc driver at the
+ -- beginning of the command line.
function Entity_Is_In_Main_Unit (E : Entity_Id) return Boolean;
-- Returns True if the entity E is declared in the main unit, or, in
-- within generic instantiations return True if the instantiation is
-- itself "in the main unit" by this definition. Otherwise False.
+ function Exact_Source_Name (Loc : Source_Ptr) return String;
+ -- Return name of entity at location Loc exactly as written in the source.
+ -- this includes copying the wide character encodings exactly as they were
+ -- used in the source, so the caller must be aware of the possibility of
+ -- such encodings.
+
+ function Get_Compilation_Switch (N : Pos) return String_Ptr;
+ -- Return the Nth stored compilation switch, or null if less than N
+ -- switches have been stored. Used by ASIS and back ends written in Ada.
+
+ function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
+ -- Generic units must be separately compiled. Since we always use
+ -- macro substitution for generics, the resulting object file is a dummy
+ -- one with no code, but the ALI file has the normal form, and we need
+ -- this ALI file so that the binder can work out a correct order of
+ -- elaboration.
+ --
+ -- However, ancient versions of GNAT used to not generate code or ALI
+ -- files for generic units, and this would yield complex order of
+ -- elaboration issues. These were fixed in GNAT 3.10. The support for not
+ -- compiling language-defined library generics was retained nonetheless
+ -- to facilitate bootstrap. Specifically, it is convenient to have
+ -- the same list of files to be compiled for all stages. So, if the
+ -- bootstrap compiler does not generate code for a given file, then
+ -- the stage1 compiler (and binder) also must deal with the case of
+ -- that file not being compiled. The predicate Generic_May_Lack_ALI is
+ -- True for those generic units for which missing ALI files are allowed.
+
+ function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type;
+ -- Return unit number of the unit whose N_Compilation_Unit node is the
+ -- one passed as an argument. This must always succeed since the node
+ -- could not have been built without making a unit table entry.
+
+ function Get_Cunit_Entity_Unit_Number
+ (E : Entity_Id) return Unit_Number_Type;
+ -- Return unit number of the unit whose compilation unit spec entity is
+ -- the one passed as an argument. This must always succeed since the
+ -- entity could not have been built without making a unit table entry.
+
function Get_Source_Unit (N : Node_Or_Entity_Id) return Unit_Number_Type;
pragma Inline (Get_Source_Unit);
function Get_Source_Unit (S : Source_Ptr) return Unit_Number_Type;
-- template, so it returns the unit number containing the code that
-- corresponds to the node N, or the source location S.
- function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
- pragma Inline (In_Same_Source_Unit);
- -- Determines if the two nodes or entities N1 and N2 are in the same
- -- source unit, the criterion being that Get_Source_Unit yields the
- -- same value for each argument.
-
- function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
- pragma Inline (In_Same_Code_Unit);
- -- Determines if the two nodes or entities N1 and N2 are in the same
- -- code unit, the criterion being that Get_Code_Unit yields the same
- -- value for each argument.
-
- function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
- pragma Inline (In_Same_Extended_Unit);
- -- Determines if two nodes or entities N1 and N2 are in the same
- -- extended unit, where an extended unit is defined as a unit and all
- -- its subunits (considered recursively, i.e. subunits of subunits are
- -- included). Returns true if S1 and S2 are in the same extended unit
- -- and False otherwise.
-
- function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
- pragma Inline (In_Same_Extended_Unit);
- -- Determines if the two source locations S1 and S2 are in the same
- -- extended unit, where an extended unit is defined as a unit and all
- -- its subunits (considered recursively, i.e. subunits of subunits are
- -- included). Returns true if S1 and S2 are in the same extended unit
- -- and False otherwise.
-
function In_Extended_Main_Code_Unit
(N : Node_Or_Entity_Id) return Boolean;
-- Return True if the node is in the generated code of the extended main
function In_Predefined_Unit (S : Source_Ptr) return Boolean;
-- Same function as above but argument is a source pointer
- function Earlier_In_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
- -- Given two Sloc values for which In_Same_Extended_Unit is true, determine
- -- if S1 appears before S2. Returns True if S1 appears before S2, and False
- -- otherwise. The result is undefined if S1 and S2 are not in the same
- -- extended unit. Note: this routine will not give reliable results if
- -- called after Sprint has been called with -gnatD set.
-
- function Exact_Source_Name (Loc : Source_Ptr) return String;
- -- Return name of entity at location Loc exactly as written in the source.
- -- this includes copying the wide character encodings exactly as they were
- -- used in the source, so the caller must be aware of the possibility of
- -- such encodings.
-
- function Compilation_Switches_Last return Nat;
- -- Return the count of stored compilation switches
+ function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
+ pragma Inline (In_Same_Code_Unit);
+ -- Determines if the two nodes or entities N1 and N2 are in the same
+ -- code unit, the criterion being that Get_Code_Unit yields the same
+ -- value for each argument.
- function Get_Compilation_Switch (N : Pos) return String_Ptr;
- -- Return the Nth stored compilation switch, or null if less than N
- -- switches have been stored. Used by ASIS and back ends written in Ada.
+ function In_Same_Extended_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
+ pragma Inline (In_Same_Extended_Unit);
+ -- Determines if two nodes or entities N1 and N2 are in the same
+ -- extended unit, where an extended unit is defined as a unit and all
+ -- its subunits (considered recursively, i.e. subunits of subunits are
+ -- included). Returns true if S1 and S2 are in the same extended unit
+ -- and False otherwise.
- function Get_Cunit_Unit_Number (N : Node_Id) return Unit_Number_Type;
- -- Return unit number of the unit whose N_Compilation_Unit node is the
- -- one passed as an argument. This must always succeed since the node
- -- could not have been built without making a unit table entry.
+ function In_Same_Extended_Unit (S1, S2 : Source_Ptr) return Boolean;
+ pragma Inline (In_Same_Extended_Unit);
+ -- Determines if the two source locations S1 and S2 are in the same
+ -- extended unit, where an extended unit is defined as a unit and all
+ -- its subunits (considered recursively, i.e. subunits of subunits are
+ -- included). Returns true if S1 and S2 are in the same extended unit
+ -- and False otherwise.
- function Get_Cunit_Entity_Unit_Number
- (E : Entity_Id) return Unit_Number_Type;
- -- Return unit number of the unit whose compilation unit spec entity is
- -- the one passed as an argument. This must always succeed since the
- -- entity could not have been built without making a unit table entry.
+ function In_Same_Source_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
+ pragma Inline (In_Same_Source_Unit);
+ -- Determines if the two nodes or entities N1 and N2 are in the same
+ -- source unit, the criterion being that Get_Source_Unit yields the
+ -- same value for each argument.
function Increment_Serial_Number return Nat;
-- Increment Serial_Number field for current unit, and return the
-- incremented value.
- procedure Synchronize_Serial_Number;
- -- This function increments the Serial_Number field for the current unit
- -- but does not return the incremented value. This is used when there
- -- is a situation where one path of control increments a serial number
- -- (using Increment_Serial_Number), and the other path does not and it is
- -- important to keep the serial numbers synchronized in the two cases (e.g.
- -- when the references in a package and a client must be kept consistent).
+ procedure Initialize;
+ -- Initialize internal tables
+
+ function Is_Loaded (Uname : Unit_Name_Type) return Boolean;
+ -- Determines if unit with given name is already loaded, i.e. there is
+ -- already an entry in the file table with this unit name for which the
+ -- corresponding file was found and parsed. Note that the Fatal_Error flag
+ -- of this entry must be checked before proceeding with further processing.
+
+ function Last_Unit return Unit_Number_Type;
+ -- Unit number of last allocated unit
+
+ procedure List (File_Names_Only : Boolean := False);
+ -- Lists units in active library (i.e. generates output consisting of a
+ -- sorted listing of the units represented in File table, except for the
+ -- main unit). If File_Names_Only is set to True, then the list includes
+ -- only file names, and no other information. Otherwise the unit name and
+ -- time stamp are also output. File_Names_Only also restricts the list to
+ -- exclude any predefined files.
+
+ procedure Lock;
+ -- Lock internal tables before calling back end
+
+ function Num_Units return Nat;
+ -- Number of units currently in unit table
+
+ procedure Remove_Unit (U : Unit_Number_Type);
+ -- Remove unit U from unit table. Currently this is effective only if U is
+ -- the last unit currently stored in the unit table.
procedure Replace_Linker_Option_String
(S : String_Id;
-- which may influence the generated output file(s). Switch is the text of
-- the switch to store (except that -fRTS gets changed back to --RTS).
- procedure Enable_Switch_Storing;
- -- Enable registration of switches by Store_Compilation_Switch. Used to
- -- avoid registering switches added automatically by the gcc driver at the
- -- beginning of the command line.
-
- procedure Disable_Switch_Storing;
- -- Disable registration of switches by Store_Compilation_Switch. Used to
- -- avoid registering switches added automatically by the gcc driver at the
- -- end of the command line.
-
procedure Store_Linker_Option_String (S : String_Id);
-- This procedure is called to register the string from a pragma
-- Linker_Option. The argument is the Id of the string to register.
-- This procedure is called to register a pragma N for which a notes
-- entry is required.
- procedure Initialize;
- -- Initialize internal tables
-
- procedure Lock;
- -- Lock internal tables before calling back end
-
- procedure Unlock;
- -- Unlock internal tables, in cases where the back end needs to modify them
+ procedure Synchronize_Serial_Number;
+ -- This function increments the Serial_Number field for the current unit
+ -- but does not return the incremented value. This is used when there
+ -- is a situation where one path of control increments a serial number
+ -- (using Increment_Serial_Number), and the other path does not and it is
+ -- important to keep the serial numbers synchronized in the two cases (e.g.
+ -- when the references in a package and a client must be kept consistent).
procedure Tree_Read;
-- Initializes internal tables from current tree file using the relevant
-- Writes out internal tables to current tree file using the relevant
-- Table.Tree_Write routines.
- function Is_Loaded (Uname : Unit_Name_Type) return Boolean;
- -- Determines if unit with given name is already loaded, i.e. there is
- -- already an entry in the file table with this unit name for which the
- -- corresponding file was found and parsed. Note that the Fatal_Error flag
- -- of this entry must be checked before proceeding with further processing.
+ procedure Unlock;
+ -- Unlock internal tables, in cases where the back end needs to modify them
+
+ function Version_Get (U : Unit_Number_Type) return Word_Hex_String;
+ -- Returns the version as a string with 8 hex digits (upper case letters)
procedure Version_Referenced (S : String_Id);
-- This routine is called from Exp_Attr to register the use of a Version
-- or Body_Version attribute. The argument is the external name used to
-- access the version string.
- procedure List (File_Names_Only : Boolean := False);
- -- Lists units in active library (i.e. generates output consisting of a
- -- sorted listing of the units represented in File table, except for the
- -- main unit). If File_Names_Only is set to True, then the list includes
- -- only file names, and no other information. Otherwise the unit name and
- -- time stamp are also output. File_Names_Only also restricts the list to
- -- exclude any predefined files.
-
- function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
- -- Generic units must be separately compiled. Since we always use
- -- macro substitution for generics, the resulting object file is a dummy
- -- one with no code, but the ALI file has the normal form, and we need
- -- this ALI file so that the binder can work out a correct order of
- -- elaboration.
- --
- -- However, ancient versions of GNAT used to not generate code or ALI
- -- files for generic units, and this would yield complex order of
- -- elaboration issues. These were fixed in GNAT 3.10. The support for not
- -- compiling language-defined library generics was retained nonetheless
- -- to facilitate bootstrap. Specifically, it is convenient to have
- -- the same list of files to be compiled for all stages. So, if the
- -- bootstrap compiler does not generate code for a given file, then
- -- the stage1 compiler (and binder) also must deal with the case of
- -- that file not being compiled. The predicate Generic_May_Lack_ALI is
- -- True for those generic units for which missing ALI files are allowed.
-
procedure Write_Unit_Info
(Unit_Num : Unit_Number_Type;
Item : Node_Id;
-- True if the frontend finished its work and has called the backend to
-- process the tree and generate the object file.
+ type Ghost_Mode_Type is (None, Check, Ignore);
+ -- Possible legal modes that can be set by aspect/pragma Ghost as well as
+ -- value None, which indicates that no such aspect/pragma applies.
+
+ Ghost_Mode : Ghost_Mode_Type := None;
+ -- GNAT
+ -- Current Ghost mode setting
+
Global_Discard_Names : Boolean := False;
-- GNAT, GNATBIND
-- True if a pragma Discard_Names appeared as a configuration pragma for
end loop;
end Save_Private_Visibility;
+ -- Local variables
+
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect to ensure a clean environment
+ -- when analyzing the unit.
+
-- Start of processing for Load_RTU
begin
return;
end if;
+ -- Provide a clean environment for the unit
+
+ Ghost_Mode := None;
+
-- Note if secondary stack is used
if U_Id = System_Secondary_Stack then
if Use_Setting then
Set_Is_Potentially_Use_Visible (U.Entity, True);
end if;
+
+ -- Restore the original Ghost mode now that analysis has taken place
+
+ Ghost_Mode := GM;
end Load_RTU;
--------------------
-------------
procedure Analyze (N : Node_Id) is
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect in case the construct sets a
+ -- different mode.
+
begin
Debug_A_Entry ("analyzing ", N);
-- Otherwise processing depends on the node kind
case Nkind (N) is
-
when N_Abort_Statement =>
Analyze_Abort_Statement (N);
-- the call to analyze them is generated when the full list is
-- analyzed.
- when
- N_SCIL_Dispatch_Table_Tag_Init |
- N_SCIL_Dispatching_Call |
- N_SCIL_Membership_Test =>
+ when N_SCIL_Dispatch_Table_Tag_Init |
+ N_SCIL_Dispatching_Call |
+ N_SCIL_Membership_Test =>
null;
-- For the remaining node types, we generate compiler abort, because
-- node appears only in the context of a type declaration, and is
-- processed by the analyze routine for type declarations.
- when
- N_Abortable_Part |
- N_Access_Definition |
- N_Access_Function_Definition |
- N_Access_Procedure_Definition |
- N_Access_To_Object_Definition |
- N_Aspect_Specification |
- N_Case_Expression_Alternative |
- N_Case_Statement_Alternative |
- N_Compilation_Unit_Aux |
- N_Component_Association |
- N_Component_Clause |
- N_Component_Definition |
- N_Component_List |
- N_Constrained_Array_Definition |
- N_Contract |
- N_Decimal_Fixed_Point_Definition |
- N_Defining_Character_Literal |
- N_Defining_Identifier |
- N_Defining_Operator_Symbol |
- N_Defining_Program_Unit_Name |
- N_Delta_Constraint |
- N_Derived_Type_Definition |
- N_Designator |
- N_Digits_Constraint |
- N_Discriminant_Association |
- N_Discriminant_Specification |
- N_Elsif_Part |
- N_Entry_Call_Statement |
- N_Enumeration_Type_Definition |
- N_Exception_Handler |
- N_Floating_Point_Definition |
- N_Formal_Decimal_Fixed_Point_Definition |
- N_Formal_Derived_Type_Definition |
- N_Formal_Discrete_Type_Definition |
- N_Formal_Floating_Point_Definition |
- N_Formal_Modular_Type_Definition |
- N_Formal_Ordinary_Fixed_Point_Definition |
- N_Formal_Private_Type_Definition |
- N_Formal_Incomplete_Type_Definition |
- N_Formal_Signed_Integer_Type_Definition |
- N_Function_Specification |
- N_Generic_Association |
- N_Index_Or_Discriminant_Constraint |
- N_Iteration_Scheme |
- N_Mod_Clause |
- N_Modular_Type_Definition |
- N_Ordinary_Fixed_Point_Definition |
- N_Parameter_Specification |
- N_Pragma_Argument_Association |
- N_Procedure_Specification |
- N_Real_Range_Specification |
- N_Record_Definition |
- N_Signed_Integer_Type_Definition |
- N_Unconstrained_Array_Definition |
- N_Unused_At_Start |
- N_Unused_At_End |
- N_Variant =>
-
+ when N_Abortable_Part |
+ N_Access_Definition |
+ N_Access_Function_Definition |
+ N_Access_Procedure_Definition |
+ N_Access_To_Object_Definition |
+ N_Aspect_Specification |
+ N_Case_Expression_Alternative |
+ N_Case_Statement_Alternative |
+ N_Compilation_Unit_Aux |
+ N_Component_Association |
+ N_Component_Clause |
+ N_Component_Definition |
+ N_Component_List |
+ N_Constrained_Array_Definition |
+ N_Contract |
+ N_Decimal_Fixed_Point_Definition |
+ N_Defining_Character_Literal |
+ N_Defining_Identifier |
+ N_Defining_Operator_Symbol |
+ N_Defining_Program_Unit_Name |
+ N_Delta_Constraint |
+ N_Derived_Type_Definition |
+ N_Designator |
+ N_Digits_Constraint |
+ N_Discriminant_Association |
+ N_Discriminant_Specification |
+ N_Elsif_Part |
+ N_Entry_Call_Statement |
+ N_Enumeration_Type_Definition |
+ N_Exception_Handler |
+ N_Floating_Point_Definition |
+ N_Formal_Decimal_Fixed_Point_Definition |
+ N_Formal_Derived_Type_Definition |
+ N_Formal_Discrete_Type_Definition |
+ N_Formal_Floating_Point_Definition |
+ N_Formal_Modular_Type_Definition |
+ N_Formal_Ordinary_Fixed_Point_Definition |
+ N_Formal_Private_Type_Definition |
+ N_Formal_Incomplete_Type_Definition |
+ N_Formal_Signed_Integer_Type_Definition |
+ N_Function_Specification |
+ N_Generic_Association |
+ N_Index_Or_Discriminant_Constraint |
+ N_Iteration_Scheme |
+ N_Mod_Clause |
+ N_Modular_Type_Definition |
+ N_Ordinary_Fixed_Point_Definition |
+ N_Parameter_Specification |
+ N_Pragma_Argument_Association |
+ N_Procedure_Specification |
+ N_Real_Range_Specification |
+ N_Record_Definition |
+ N_Signed_Integer_Type_Definition |
+ N_Unconstrained_Array_Definition |
+ N_Unused_At_Start |
+ N_Unused_At_End |
+ N_Variant =>
raise Program_Error;
end case;
then
Expand (N);
end if;
+
+ -- Restore the original Ghost mode once analysis and expansion have
+ -- taken place.
+
+ Ghost_Mode := GM;
end Analyze;
-- Version with check(s) suppressed
---------------
procedure Semantics (Comp_Unit : Node_Id) is
+ procedure Do_Analyze;
+ -- Perform the analysis of the compilation unit
+
+ ----------------
+ -- Do_Analyze --
+ ----------------
+
+ procedure Do_Analyze is
+ GM : constant Ghost_Mode_Type := Ghost_Mode;
+ -- Save the current Ghost mode in effect in case the compilation unit
+ -- is withed from a unit with a different Ghost mode.
+
+ List : Elist_Id;
+
+ begin
+ List := Save_Scope_Stack;
+ Push_Scope (Standard_Standard);
+
+ -- Set up a clean environment before analyzing
+
+ Ghost_Mode := None;
+ Outer_Generic_Scope := Empty;
+ Scope_Suppress := Suppress_Options;
+ Scope_Stack.Table
+ (Scope_Stack.Last).Component_Alignment_Default := Calign_Default;
+ Scope_Stack.Table
+ (Scope_Stack.Last).Is_Active_Stack_Base := True;
+
+ -- Now analyze the top level compilation unit node
+
+ Analyze (Comp_Unit);
+
+ -- Check for scope mismatch on exit from compilation
+
+ pragma Assert (Current_Scope = Standard_Standard
+ or else Comp_Unit = Cunit (Main_Unit));
+
+ -- Then pop entry for Standard, and pop implicit types
+
+ Pop_Scope;
+ Restore_Scope_Stack (List);
+ Ghost_Mode := GM;
+ end Do_Analyze;
+
+ -- Local variables
-- The following locations save the corresponding global flags and
-- variables so that they can be restored on completion. This is needed
S_Outer_Gen_Scope : constant Entity_Id := Outer_Generic_Scope;
S_Style_Check : constant Boolean := Style_Check;
+ Already_Analyzed : constant Boolean := Analyzed (Comp_Unit);
+
Curunit : constant Unit_Number_Type := Get_Cunit_Unit_Number (Comp_Unit);
-- New value of Current_Sem_Unit
-- unit. All with'ed units are analyzed with config restrictions reset
-- and we need to restore these saved values at the end.
- procedure Do_Analyze;
- -- Procedure to analyze the compilation unit
-
- ----------------
- -- Do_Analyze --
- ----------------
-
- procedure Do_Analyze is
- List : Elist_Id;
-
- begin
- List := Save_Scope_Stack;
- Push_Scope (Standard_Standard);
- Scope_Suppress := Suppress_Options;
- Scope_Stack.Table
- (Scope_Stack.Last).Component_Alignment_Default := Calign_Default;
- Scope_Stack.Table
- (Scope_Stack.Last).Is_Active_Stack_Base := True;
- Outer_Generic_Scope := Empty;
-
- -- Now analyze the top level compilation unit node
-
- Analyze (Comp_Unit);
-
- -- Check for scope mismatch on exit from compilation
-
- pragma Assert (Current_Scope = Standard_Standard
- or else Comp_Unit = Cunit (Main_Unit));
-
- -- Then pop entry for Standard, and pop implicit types
-
- Pop_Scope;
- Restore_Scope_Stack (List);
- end Do_Analyze;
-
- Already_Analyzed : constant Boolean := Analyzed (Comp_Unit);
-
-- Start of processing for Semantics
begin
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;
procedure Analyze_Exception_Declaration (N : Node_Id) is
Id : constant Entity_Id := Defining_Identifier (N);
PF : constant Boolean := Is_Pure (Current_Scope);
+
begin
+ -- The exception declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Exception);
Set_Is_Statically_Allocated (Id);
Set_Is_Pure (Id, PF);
- -- An exception declared within a Ghost scope is automatically Ghost
+ -- An exception declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
with Fname; use Fname;
with Fname.UF; use Fname.UF;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Itypes; use Itypes;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
Decl : Node_Id;
begin
+ -- The generic package declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- We introduce a renaming of the enclosing package, to have a usable
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
- -- A generic package declared within a Ghost scope is rendered Ghost
+ -- A generic package declared within a Ghost region is rendered Ghost
-- (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
Typ : Entity_Id;
begin
+ -- The generic subprogram declaration may be subject to pragma Ghost
+ -- with policy Ignore. Set the mode now to ensure that any nodes
+ -- generated during analysis and expansion are properly flagged as
+ -- ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic is not allowed", N);
-- Create copy of generic unit, and save for instantiation. If the unit
Set_Etype (Id, Standard_Void_Type);
end if;
- -- A generic subprogram declared within a Ghost scope is rendered Ghost
+ -- A generic subprogram declared within a Ghost region is rendered Ghost
-- (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Itypes; use Itypes;
with Layout; use Layout;
with Lib; use Lib;
function Find_Type_Of_Object
(Obj_Def : Node_Id;
Related_Nod : Node_Id) return Entity_Id;
- -- Get type entity for object referenced by Obj_Def, attaching the
- -- implicit types generated to Related_Nod
+ -- Get type entity for object referenced by Obj_Def, attaching the implicit
+ -- types generated to Related_Nod.
procedure Floating_Point_Type_Declaration (T : Entity_Id; Def : Node_Id);
-- Create a new float and apply the constraint to obtain subtype of it
begin
Prev := Find_Type_Name (N);
- -- The full view, if present, now points to the current type
- -- If there is an incomplete partial view, set a link to it, to
- -- simplify the retrieval of primitive operations of the type.
+ -- The type declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N, Prev);
+
+ -- The full view, if present, now points to the current type. If there
+ -- is an incomplete partial view, set a link to it, to simplify the
+ -- retrieval of primitive operations of the type.
-- Ada 2005 (AI-50217): If the type was previously decorated when
-- imported through a LIMITED WITH clause, it appears as incomplete
Check_SPARK_05_Restriction ("controlled type is not allowed", N);
end if;
- -- A type declared within a Ghost scope is automatically Ghost
+ -- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Comes_From_Source (T) and then Within_Ghost_Scope then
+ if Comes_From_Source (T) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
end if;
Set_Is_First_Subtype (T, True);
Set_Etype (T, T);
- -- An incomplete type declared within a Ghost scope is automatically
+ -- An incomplete type declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (T);
end if;
It : Interp;
begin
+ -- The number declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
Generate_Definition (Id);
Enter_Name (Id);
- -- A number declared within a Ghost scope is automatically Ghost
+ -- A number declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
end if;
end if;
+ -- The object declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N, Prev_Entity);
+
if Present (Prev_Entity) then
Constant_Redeclaration (Id, N, T);
Set_Ekind (Id, E_Variable);
end if;
- -- An object declared within a Ghost scope is automatically
+ -- An object declared within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
- if Comes_From_Source (Id) and then Within_Ghost_Scope then
+ if Comes_From_Source (Id) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
-- The Ghost policy in effect at the point of declaration
Init_Esize (Id);
Set_Optimize_Alignment_Flags (Id);
- -- An object declared within a Ghost scope is automatically Ghost
- -- (SPARK RM 6.9(2)). This property is also inherited when its type
- -- is Ghost or the previous declaration of the deferred constant is
- -- Ghost.
+ -- An object declared within a Ghost region is automatically Ghost
+ -- (SPARK RM 6.9(2)).
if Comes_From_Source (Id)
- and then (Is_Ghost_Entity (T)
+ and then (Ghost_Mode > None
or else (Present (Prev_Entity)
- and then Is_Ghost_Entity (Prev_Entity))
- or else Within_Ghost_Scope)
+ and then Is_Ghost_Entity (Prev_Entity)))
then
Set_Is_Ghost_Entity (Id);
Parent_Base : Entity_Id;
begin
+ -- The private extension declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
-- Ada 2005 (AI-251): Decorate all names in list of ancestor interfaces
if Is_Non_Empty_List (Interface_List (N)) then
R_Checks : Check_Result;
begin
+ -- The subtype declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
Generate_Definition (Id);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Init_Size_Align (Id);
-- The constrained array type is a subtype of the unconstrained one
- Set_Ekind (T, E_Array_Subtype);
- Init_Size_Align (T);
- Set_Etype (T, Implicit_Base);
- Set_Scope (T, Current_Scope);
- Set_Is_Constrained (T, True);
- Set_First_Index (T, First (Discrete_Subtype_Definitions (Def)));
+ Set_Ekind (T, E_Array_Subtype);
+ Init_Size_Align (T);
+ Set_Etype (T, Implicit_Base);
+ Set_Scope (T, Current_Scope);
+ Set_Is_Constrained (T);
+ Set_First_Index (T,
+ First (Discrete_Subtype_Definitions (Def)));
Set_Has_Delayed_Freeze (T);
-- Complete setup of implicit base type
Set_Has_Protected (Implicit_Base, Has_Protected (Element_Type));
Set_Component_Size (Implicit_Base, Uint_0);
Set_Packed_Array_Impl_Type (Implicit_Base, Empty);
- Set_Has_Controlled_Component
- (Implicit_Base,
- Has_Controlled_Component (Element_Type)
- or else Is_Controlled (Element_Type));
- Set_Finalize_Storage_Only
- (Implicit_Base, Finalize_Storage_Only
- (Element_Type));
+ Set_Has_Controlled_Component (Implicit_Base,
+ Has_Controlled_Component (Element_Type)
+ or else Is_Controlled (Element_Type));
+ Set_Finalize_Storage_Only (Implicit_Base,
+ Finalize_Storage_Only (Element_Type));
+
+ -- Inherit the "ghostness" from the constrained array type
+
+ if Is_Ghost_Entity (T) or else Ghost_Mode > None then
+ Set_Is_Ghost_Entity (Implicit_Base);
+ end if;
-- Unconstrained array case
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 Is_Ghost_Entity (Parent_Base) or else Ghost_Mode > None then
+ Set_Is_Ghost_Entity (Implicit_Base);
+ end if;
end Make_Implicit_Base;
-- Start of processing for Build_Derived_Array_Type
Derived_Type : Entity_Id;
Derive_Subps : Boolean := True)
is
- function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ implements at least one Ghost interface
-
- --------------------------------
- -- Implements_Ghost_Interface --
- --------------------------------
-
- function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
- Iface_Elmt : Elmt_Id;
- begin
- -- Traverse the list of interfaces looking for a Ghost interface
-
- if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
- Iface_Elmt := First_Elmt (Interfaces (Typ));
- while Present (Iface_Elmt) loop
- if Is_Ghost_Entity (Node (Iface_Elmt)) then
- return True;
- end if;
-
- Next_Elmt (Iface_Elmt);
- end loop;
- end if;
-
- return False;
- end Implements_Ghost_Interface;
-
- -- Local variables
-
Discriminant_Specs : constant Boolean :=
Present (Discriminant_Specifications (N));
Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type);
-- An empty Discs list means that there were no constraints in the
-- subtype indication or that there was an error processing it.
- -- Start of processing for Build_Derived_Record_Type
-
begin
if Ekind (Parent_Type) = E_Record_Type_With_Private
and then Present (Full_View (Parent_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.
with Exp_Ch6; use Exp_Ch6;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
-- proper use of a Ghost entity need to know the enclosing context.
Analyze (Lhs);
+
+ -- The left hand side of an assignment may reference an entity subject
+ -- to pragma Ghost with policy Ignore. Set the mode now to ensure that
+ -- any nodes generated during analysis and expansion are properly
+ -- flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
Analyze (Rhs);
-- Ensure that we never do an assignment on a variable marked as
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib.Xref; use Lib.Xref;
Scop : constant Entity_Id := Current_Scope;
begin
+ -- The abstract subprogram declaration may be subject to pragma Ghost
+ -- with policy Ignore. Set the mode now to ensure that any nodes
+ -- generated during analysis and expansion are properly flagged as
+ -- ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
Set_Categorization_From_Scope (Designator, Scop);
- -- An abstract subprogram declared within a Ghost scope is automatically
+ -- An abstract subprogram declared within a Ghost region is rendered
-- Ghost (SPARK RM 6.9(2)).
- if Comes_From_Source (Designator) and then Within_Ghost_Scope then
+ if Comes_From_Source (Designator) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
end if;
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
- if Is_Ghost_Entity (Gen_Id) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Gen_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at
return;
end if;
+ -- The name of the procedure call may reference an entity subject to
+ -- pragma Ghost with policy Ignore. Set the mode now to ensure that any
+ -- nodes generated during analysis and expansion are properly flagged as
+ -- ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
-- Otherwise analyze the parameters
if Present (Actuals) then
then
if Is_Generic_Subprogram (Prev_Id) then
Spec_Id := Prev_Id;
+
+ -- The corresponding spec may be subject to pragma Ghost with
+ -- policy Ignore. Set 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);
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Set_Is_Child_Unit (Body_Id, Is_Child_Unit (Spec_Id));
then
if Is_Private_Concurrent_Primitive (Body_Id) then
Spec_Id := Disambiguate_Spec;
+
+ -- The corresponding spec may be subject to pragma Ghost with
+ -- policy Ignore. Set 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);
+
else
Spec_Id := Find_Corresponding_Spec (N);
+ -- The corresponding spec may be subject to pragma Ghost with
+ -- policy Ignore. Set 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);
+
-- In GNATprove mode, if the body has no previous spec, create
-- one so that the inlining machinery can operate properly.
-- Transfer aspects, if any, to the new spec, so that they
else
Spec_Id := Corresponding_Spec (N);
+
+ -- The corresponding spec may be subject to pragma Ghost with
+ -- policy Ignore. Set 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);
end if;
end if;
-- property is not directly inherited as the body may be subject
-- to a different Ghost assertion policy.
- if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and
-- Indicates whether a null procedure declaration is a completion
begin
+ -- The subprogram declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
-- Null procedures are not allowed in SPARK
if Nkind (Specification (N)) = N_Procedure_Specification
-- explicit pragma).
Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Designator, True);
+ Set_SPARK_Pragma_Inherited (Designator);
- -- A subprogram declared within a Ghost scope is automatically Ghost
+ -- A subprogram declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Comes_From_Source (Designator) and then Within_Ghost_Scope then
+ if Comes_From_Source (Designator) and then Ghost_Mode > None then
Set_Is_Ghost_Entity (Designator);
end if;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Dbug; use Exp_Dbug;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
end if;
end if;
+ -- The corresponding spec of the package body may be subject to pragma
+ -- Ghost with policy Ignore. Set 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);
+
Set_Is_Compilation_Unit (Body_Id, Is_Compilation_Unit (Spec_Id));
Style.Check_Identifier (Body_Id, Spec_Id);
-- property is not directly inherited as the body may be subject to a
-- different Ghost assertion policy.
- if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Spec_Id) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at the
Indent;
end if;
+ -- The package declaration may be subject to pragma Ghost with policy
+ -- Ignore. Set the mode now to ensure that any nodes generated during
+ -- analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
Generate_Definition (Id);
Enter_Name (Id);
Set_Ekind (Id, E_Package);
Id : constant Entity_Id := Defining_Identifier (N);
begin
+ -- The private type declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
Generate_Definition (Id);
Set_Is_Pure (Id, PF);
Init_Size_Align (Id);
New_Private_Type (N, Id, N);
Set_Depends_On_Private (Id);
- -- A type declared within a Ghost scope is automatically Ghost
+ -- A type declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Impunit; use Impunit;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
Nam : constant Node_Id := Name (N);
begin
+ -- The exception renaming declaration may be subject to pragma Ghost
+ -- with policy Ignore. Set the mode now to ensure that any nodes
+ -- generated during analysis and expansion are properly flagged as
+ -- ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
Enter_Name (Id);
-- An exception renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
- if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (Id);
end if;
end if;
return;
end if;
+ -- The generic renaming declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
Generate_Definition (New_P);
-- An generic renaming is Ghost if the renamed entity is Ghost or the
-- construct appears within a Ghost scope.
- if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
return;
end if;
+ -- The object renaming declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
Check_SPARK_05_Restriction ("object renaming is not allowed", N);
Set_Is_Pure (Id, Is_Pure (Current_Scope));
if (Is_Entity_Name (Nam)
and then Is_Ghost_Entity (Entity (Nam)))
- or else Within_Ghost_Scope
+ or else Ghost_Mode > None
then
Set_Is_Ghost_Entity (Id);
end if;
return;
end if;
+ -- The package renaming declaration may be subject to pragma Ghost with
+ -- policy Ignore. Set the mode now to ensure that any nodes generated
+ -- during analysis and expansion are properly flagged as ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
-- Check for Text_IO special unit (we may be renaming a Text_IO child)
Check_Text_IO_Special_Unit (Name (N));
-- A package renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
- if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Old_P) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_P);
end if;
-- Start of processing for Analyze_Subprogram_Renaming
begin
+ -- The subprogram renaming declaration may be subject to pragma Ghost
+ -- with policy Ignore. Set the mode now to ensure that any nodes
+ -- generated during analysis and expansion are properly flagged as
+ -- ignored Ghost.
+
+ Set_Ghost_Mode (N);
+
-- We must test for the attribute renaming case before the Analyze
-- call because otherwise Sem_Attr will complain that the attribute
-- is missing an argument when it is analyzed.
-- A subprogram renaming is Ghost if the renamed entity is Ghost or
-- the construct appears within a Ghost scope.
- if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then
+ if Is_Ghost_Entity (Entity (Nam)) or else Ghost_Mode > None then
Set_Is_Ghost_Entity (New_S);
end if;
elsif Is_Floating_Point_Type (Etype (N)) then
Check_Restriction (No_Floating_Point, N);
end if;
+
+ -- A Ghost type must appear in a specific context
+
+ if Is_Ghost_Entity (Etype (N)) then
+ Check_Ghost_Context (Etype (N), N);
+ end if;
end if;
end Find_Type;
with Exp_Dist; use Exp_Dist;
with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Writ; use Lib.Writ;
with Lib.Xref; use Lib.Xref;
-- If previous error, avoid cascaded errors
Check_Error_Detected;
- Applies := True;
+ Applies := True;
else
Make_Inline (Subp);
end if;
if not Applies then
- Error_Pragma_Arg
- ("inappropriate argument for pragma%", Assoc);
+ Error_Pragma_Arg ("inappropriate argument for pragma%", Assoc);
end if;
Next (Assoc);
Set_Refinement_Constituents (State_Id, New_Elmt_List);
Set_Part_Of_Constituents (State_Id, New_Elmt_List);
- -- An abstract state declared within a Ghost scope becomes
+ -- An abstract state declared within a Ghost region becomes
-- Ghost (SPARK RM 6.9(2)).
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Set_Is_Ghost_Entity (State_Id);
end if;
-- Pragma Check_Policy specifying a Ghost policy cannot
-- occur within a ghost subprogram or package.
- if Within_Ghost_Scope then
+ if Ghost_Mode > None then
Error_Pragma
("pragma % cannot appear within ghost subprogram or "
& "package");
-- region (SPARK RM 6.9(7)).
if Is_False (Expr_Value (Expr))
- and then Within_Ghost_Scope
+ and then Ghost_Mode > None
then
Error_Pragma
("pragma % with value False cannot appear in enabled "
-- Independent_Components --
----------------------------
- -- pragma Independent_Components (array_or_record_LOCAL_NAME);
+ -- pragma Atomic_Components (array_or_record_LOCAL_NAME);
when Pragma_Independent_Components => Independent_Components : declare
E_Id : Node_Id;
with Exp_Util; use Exp_Util;
with Fname; use Fname;
with Freeze; use Freeze;
+with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
Pref : Node_Id);
-- Check that the type of the prefix of a dereference is not incomplete
- 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.
-
function Check_Infinite_Recursion (N : Node_Id) return Boolean;
-- Given a call node, N, which is known to occur immediately within the
-- subprogram being called, determines whether it is a detectable case of
end if;
end Check_Fully_Declared_Prefix;
- -------------------------
- -- Check_Ghost_Context --
- -------------------------
-
- procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
- procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
- -- Verify that the Ghost policy at the point of declaration of entity Id
- -- matches the policy at the point of reference. If this is not the case
- -- emit an error at Err_N.
-
- function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
- -- Determine whether node Context denotes a Ghost-friendly context where
- -- a Ghost entity can safely reside.
-
- -------------------------
- -- Is_OK_Ghost_Context --
- -------------------------
-
- function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
- function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
- -- Determine whether node Decl is a Ghost declaration or appears
- -- within a Ghost declaration.
-
- --------------------------
- -- Is_Ghost_Declaration --
- --------------------------
-
- function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
- Par : Node_Id;
- Subp_Decl : Node_Id;
- Subp_Id : Entity_Id;
-
- begin
- -- Climb the parent chain looking for an object declaration
-
- Par := Decl;
- while Present (Par) loop
- case Nkind (Par) is
- when N_Abstract_Subprogram_Declaration |
- N_Exception_Declaration |
- N_Exception_Renaming_Declaration |
- 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 Is_Subject_To_Ghost (Par);
-
- when others =>
- null;
- end case;
-
- -- Special cases
-
- -- A reference to a Ghost entity may appear as the default
- -- expression of a formal parameter of a subprogram body. This
- -- context must be treated as suitable because the relation
- -- between the spec and the body has not been established and
- -- the body is not marked as Ghost yet. The real check was
- -- performed on the spec.
-
- if Nkind (Par) = N_Parameter_Specification
- and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
- then
- return True;
-
- -- References to Ghost entities may be relocated in internally
- -- generated bodies.
-
- elsif Nkind (Par) = N_Subprogram_Body
- and then not Comes_From_Source (Par)
- then
- Subp_Id := Corresponding_Spec (Par);
-
- -- The original context is an expression function that has
- -- been split into a spec and a body. The context is OK as
- -- long as the the initial declaration is Ghost.
-
- if Present (Subp_Id) then
- Subp_Decl :=
- Original_Node (Unit_Declaration_Node (Subp_Id));
-
- if Nkind (Subp_Decl) = N_Expression_Function then
- return Is_Subject_To_Ghost (Subp_Decl);
- end if;
- end if;
-
- -- Otherwise this is either an internal body or an internal
- -- completion. Both are OK because the real check was done
- -- before expansion activities.
-
- return True;
- end if;
-
- -- Prevent the search from going too far
-
- if Is_Body_Or_Package_Declaration (Par) then
- return False;
- end if;
-
- Par := Parent (Par);
- end loop;
-
- return False;
- end Is_Ghost_Declaration;
-
- -- Start of processing for Is_OK_Ghost_Context
-
- begin
- -- The Ghost entity appears within an assertion expression
-
- if In_Assertion_Expr > 0 then
- return True;
-
- -- The Ghost entity is part of a declaration or its completion
-
- elsif Is_Ghost_Declaration (Context) then
- return True;
-
- -- The Ghost entity is referenced within a Ghost statement
-
- elsif Is_Ghost_Statement_Or_Pragma (Context) then
- return True;
-
- else
- return False;
- end if;
- end Is_OK_Ghost_Context;
-
- ------------------------
- -- Check_Ghost_Policy --
- ------------------------
-
- procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
-
- begin
- -- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(14)).
-
- if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
- Error_Msg_Sloc := Sloc (Err_N);
-
- Error_Msg_N ("incompatible ghost policies in effect", Err_N);
- Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
- Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
-
- elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
- Error_Msg_Sloc := Sloc (Err_N);
-
- Error_Msg_N ("incompatible ghost policies in effect", Err_N);
- Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
- Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
- end if;
- end Check_Ghost_Policy;
-
- -- Start of processing for Check_Ghost_Context
-
- begin
- -- Once it has been established that the reference to the Ghost entity
- -- is within a suitable context, ensure that the policy at the point of
- -- declaration and at the point of use match.
-
- if Is_OK_Ghost_Context (Ghost_Ref) then
- Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
-
- -- Otherwise the Ghost entity appears in a non-Ghost context and affects
- -- its behavior or value.
-
- else
- Error_Msg_N
- ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
- Ghost_Ref);
- end if;
- end Check_Ghost_Context;
-
------------------------------
-- Check_Infinite_Recursion --
------------------------------
package body Sem_Util is
----------------------------------------
- -- Global_Variables for New_Copy_Tree --
+ -- Global Variables for New_Copy_Tree --
----------------------------------------
-- These global variables are used by New_Copy_Tree. See description of the
-- and Build_Discriminal_Subtype_Of_Component. C is a list of constraints,
-- Loc is the source location, T is the original subtype.
- function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
- -- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
- -- with discriminants whose default values are static, examine only the
- -- components in the selected variant to determine whether all of them
- -- have a default.
-
function Has_Enabled_Property
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
-- If the parent type is fully initialized, T can be treated as such.
+ function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
+ -- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
+ -- with discriminants whose default values are static, examine only the
+ -- components in the selected variant to determine whether all of them
+ -- have a default.
+
------------------------------
-- Abstract_Interface_List --
------------------------------
end if;
end Check_Function_Writable_Actuals;
- ----------------------------
- -- Check_Ghost_Completion --
- ----------------------------
-
- procedure Check_Ghost_Completion
- (Partial_View : Entity_Id;
- Full_View : Entity_Id)
- is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
-
- begin
- -- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(15)).
-
- if Is_Checked_Ghost_Entity (Partial_View)
- and then Policy = Name_Ignore
- then
- Error_Msg_Sloc := Sloc (Full_View);
-
- 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);
-
- elsif Is_Ignored_Ghost_Entity (Partial_View)
- and then Policy = Name_Check
- then
- Error_Msg_Sloc := Sloc (Full_View);
-
- 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);
- end if;
- end Check_Ghost_Completion;
-
- ----------------------------
- -- Check_Ghost_Derivation --
- ----------------------------
-
- procedure Check_Ghost_Derivation (Typ : Entity_Id) is
- Parent_Typ : constant Entity_Id := Etype (Typ);
- Iface : Entity_Id;
- Iface_Elmt : Elmt_Id;
-
- begin
- -- Allow untagged derivations from predefined types such as Integer as
- -- those are not Ghost by definition.
-
- if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
- null;
-
- -- The parent type of a Ghost type extension must be Ghost
-
- elsif not Is_Ghost_Entity (Parent_Typ) then
- Error_Msg_N ("type extension & cannot be ghost", Typ);
- Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
- return;
- end if;
-
- -- All progenitors (if any) must be Ghost as well
-
- if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
- Iface_Elmt := First_Elmt (Interfaces (Typ));
- while Present (Iface_Elmt) loop
- Iface := Node (Iface_Elmt);
-
- if not Is_Ghost_Entity (Iface) then
- Error_Msg_N ("type extension & cannot be ghost", Typ);
- Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
- return;
- end if;
-
- Next_Elmt (Iface_Elmt);
- end loop;
- end if;
- end Check_Ghost_Derivation;
-
--------------------------------
-- Check_Implicit_Dereference --
--------------------------------
Pkg_Decl : Node_Id := Pkg;
begin
- if Ekind (Pkg) = E_Package then
+ if Present (Pkg) and then Ekind (Pkg) = E_Package then
while Nkind (Pkg_Decl) /= N_Package_Specification loop
Pkg_Decl := Parent (Pkg_Decl);
end loop;
and then Is_Imported (Entity (Name (N)));
end Is_CPP_Constructor_Call;
+ --------------------
+ -- Is_Declaration --
+ --------------------
+
+ function Is_Declaration (N : Node_Id) return Boolean is
+ begin
+ case Nkind (N) is
+ when N_Abstract_Subprogram_Declaration |
+ N_Exception_Declaration |
+ N_Exception_Renaming_Declaration |
+ 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;
+
-----------------
-- Is_Delegate --
-----------------
end if;
end Is_Fully_Initialized_Variant;
- ---------------------
- -- Is_Ghost_Entity --
- ---------------------
-
- function Is_Ghost_Entity (Id : Entity_Id) return Boolean is
- begin
- return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id);
- end Is_Ghost_Entity;
-
- ----------------------------------
- -- Is_Ghost_Statement_Or_Pragma --
- ----------------------------------
-
- function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is
- function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean;
- -- Determine whether an arbitrary node denotes a reference to a Ghost
- -- entity.
-
- -------------------------------
- -- Is_Ghost_Entity_Reference --
- -------------------------------
-
- function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is
- Ref : Node_Id;
-
- begin
- Ref := N;
-
- -- When the reference extracts a subcomponent, recover the related
- -- object (SPARK RM 6.9(1)).
-
- while Nkind_In (Ref, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component,
- N_Slice)
- loop
- Ref := Prefix (Ref);
- end loop;
-
- return
- Is_Entity_Name (Ref)
- and then Present (Entity (Ref))
- and then Is_Ghost_Entity (Entity (Ref));
- end Is_Ghost_Entity_Reference;
-
- -- Local variables
-
- Arg : Node_Id;
- Stmt : Node_Id;
-
- -- Start of processing for Is_Ghost_Statement_Or_Pragma
-
- begin
- if Nkind (N) = N_Pragma then
-
- -- A pragma is Ghost when it appears within a Ghost package or
- -- subprogram.
-
- if Within_Ghost_Scope then
- return True;
- end if;
-
- -- A pragma is Ghost when it mentions a Ghost entity
-
- Arg := First (Pragma_Argument_Associations (N));
- while Present (Arg) loop
- if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then
- return True;
- end if;
-
- Next (Arg);
- end loop;
- end if;
-
- Stmt := N;
- while Present (Stmt) loop
-
- -- A statement is Ghost when it appears within a Ghost package or
- -- subprogram.
-
- if Is_Statement (Stmt) and then Within_Ghost_Scope then
- return True;
-
- -- An assignment statement is Ghost when the target is a Ghost
- -- variable. A procedure call is Ghost when the invoked procedure
- -- is Ghost.
-
- elsif Nkind_In (Stmt, N_Assignment_Statement,
- N_Procedure_Call_Statement)
- then
- return Is_Ghost_Entity_Reference (Name (Stmt));
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (Stmt) then
- return False;
- end if;
-
- Stmt := Parent (Stmt);
- end loop;
-
- return False;
- end Is_Ghost_Statement_Or_Pragma;
-
----------------------------
-- Is_Inherited_Operation --
----------------------------
or else Nkind (N) = N_Procedure_Call_Statement;
end Is_Statement;
- -------------------------
- -- Is_Subject_To_Ghost --
- -------------------------
-
- function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
- function Enables_Ghostness (Arg : Node_Id) return Boolean;
- -- Determine whether aspect or pragma argument Arg enables "ghostness"
-
- -----------------------
- -- Enables_Ghostness --
- -----------------------
-
- function Enables_Ghostness (Arg : Node_Id) return Boolean is
- Expr : Node_Id;
-
- begin
- Expr := Arg;
-
- if Nkind (Expr) = N_Pragma_Argument_Association then
- Expr := Get_Pragma_Arg (Expr);
- end if;
-
- -- Determine whether the expression of the aspect is static and
- -- denotes True.
-
- if Present (Expr) then
- Preanalyze_And_Resolve (Expr);
-
- return
- Is_OK_Static_Expression (Expr)
- and then Is_True (Expr_Value (Expr));
-
- -- Otherwise Ghost defaults to True
-
- else
- return True;
- end if;
- end Enables_Ghostness;
-
- -- Local variables
-
- Id : constant Entity_Id := Defining_Entity (N);
- Asp : Node_Id;
- Decl : Node_Id;
- Prev_Id : Entity_Id;
-
- -- Start of processing for Is_Subject_To_Ghost
-
- begin
- if Is_Ghost_Entity (Id) then
- return True;
-
- -- The completion of a type or a constant is not fully analyzed when the
- -- reference to the Ghost entity is resolved. Because the completion is
- -- not marked as Ghost yet, inspect the partial view.
-
- elsif Is_Record_Type (Id)
- or else Ekind (Id) = E_Constant
- or else (Nkind (N) = N_Object_Declaration
- and then Constant_Present (N))
- then
- Prev_Id := Incomplete_Or_Partial_View (Id);
-
- if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
- return True;
- end if;
- end if;
-
- -- Examine the aspect specifications (if any) looking for aspect Ghost
-
- if Permits_Aspect_Specifications (N) then
- Asp := First (Aspect_Specifications (N));
- while Present (Asp) loop
- if Chars (Identifier (Asp)) = Name_Ghost then
- return Enables_Ghostness (Expression (Asp));
- end if;
-
- Next (Asp);
- end loop;
- end if;
-
- Decl := Empty;
-
- -- When the context is a [generic] package declaration, pragma Ghost
- -- resides in the visible declarations.
-
- if Nkind_In (N, N_Generic_Package_Declaration,
- N_Package_Declaration)
- then
- Decl := First (Visible_Declarations (Specification (N)));
-
- -- Otherwise pragma Ghost appears in the declarations following N
-
- elsif Is_List_Member (N) then
- Decl := Next (N);
- end if;
-
- while Present (Decl) loop
- if Nkind (Decl) = N_Pragma
- and then Pragma_Name (Decl) = Name_Ghost
- then
- return
- Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
-
- -- A source construct ends the region where pragma Ghost may appear,
- -- stop the traversal.
-
- elsif Comes_From_Source (Decl) then
- exit;
- end if;
-
- Next (Decl);
- end loop;
-
- return False;
- end Is_Subject_To_Ghost;
-
--------------------------------------------------
-- Is_Subprogram_Stub_Without_Prior_Declaration --
--------------------------------------------------
Set_Entity (N, Val);
end Set_Entity_With_Checks;
- -------------------------
- -- Set_Is_Ghost_Entity --
- -------------------------
-
- procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
-
- begin
- if Policy = Name_Check then
- Set_Is_Checked_Ghost_Entity (Id);
-
- elsif Policy = Name_Ignore then
- Set_Is_Ignored_Ghost_Entity (Id);
- end if;
- end Set_Is_Ghost_Entity;
-
------------------------
-- Set_Name_Entity_Id --
------------------------
return List_1;
end Visible_Ancestors;
- ------------------------
- -- Within_Ghost_Scope --
- ------------------------
-
- function Within_Ghost_Scope
- (Id : Entity_Id := Current_Scope) return Boolean
- is
- S : Entity_Id;
-
- begin
- -- Climb the scope stack looking for a Ghost scope
-
- S := Id;
- while Present (S) and then S /= Standard_Standard loop
- if Is_Ghost_Entity (S) then
- return True;
- end if;
-
- S := Scope (S);
- end loop;
-
- return False;
- end Within_Ghost_Scope;
-
----------------------
-- Within_Init_Proc --
----------------------
-- the one containing C2, that is known to refer to the same object (RM
-- 6.4.1(6.17/3)).
- 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_Derivation (Typ : Entity_Id);
- -- Verify that the parent type and all progenitors of derived type or type
- -- extension Typ are Ghost. If this is not the case, issue an error.
-
procedure Check_Implicit_Dereference (N : Node_Id; Typ : Entity_Id);
-- AI05-139-2: Accessors and iterators for containers. This procedure
-- checks whether T is a reference type, and if so it adds an interprettion
-- First determine whether type T is an interface and then check whether
-- it is of protected, synchronized or task kind.
+ function Is_Declaration (N : Node_Id) return Boolean;
+ -- Determine whether arbitrary node N denotes a declaration
+
function Is_Delegate (T : Entity_Id) return Boolean;
-- Returns true if type T represents a delegate. A Delegate is the CIL
-- object used to represent access-to-subprogram types. This is only
-- means that the result returned is not crucial, but should err on the
-- side of thinking things are fully initialized if it does not know.
- function Is_Ghost_Entity (Id : Entity_Id) return Boolean;
- -- Determine whether entity Id is Ghost. To qualify as such, the entity
- -- must be subject to Convention Ghost.
-
- function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean;
- -- Determine whether statement or pragma N is ghost. To qualify as such, N
- -- must either
- -- 1) Occur within a ghost subprogram or package
- -- 2) Denote a call to a ghost procedure
- -- 3) Denote an assignment statement whose target is a ghost variable
- -- 4) Denote a pragma that mentions a ghost entity
-
function Is_Inherited_Operation (E : Entity_Id) return Boolean;
-- E is a subprogram. Return True is E is an implicit operation inherited
-- by a derived type declaration.
-- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo).
-- Note that a label is *not* a statement, and will return False.
- function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
- -- Determine whether declarative node 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.
-
function Is_Subprogram_Stub_Without_Prior_Declaration
(N : Node_Id) return Boolean;
-- Return True if N is a subprogram stub with no prior subprogram
-- If restriction No_Implementation_Identifiers is set, then it checks
-- that the entity is not implementation defined.
- procedure Set_Is_Ghost_Entity (Id : Entity_Id);
- -- Set the relevant ghost attribute of entity Id depending on the current
- -- Ghost assertion policy in effect.
-
procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
pragma Inline (Set_Name_Entity_Id);
-- Sets the Entity_Id value associated with the given name, which is the
-- generate the list of visible ancestors; otherwise their partial
-- view is added to the resulting list.
- function Within_Ghost_Scope
- (Id : Entity_Id := Current_Scope) return Boolean;
- -- Determine whether an arbitrary entity is either a scope or within a
- -- scope subject to convention Ghost or one that inherits "ghostness" from
- -- an enclosing construct.
-
function Within_Init_Proc return Boolean;
-- Determines if Current_Scope is within an init proc
-- simply ignore these nodes, since they are not relevant to the task
-- of back annotating representation information.
+ ----------------
+ -- 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:
+
+ -- 1. Check - All static semantics as defined in SPARK RM 6.9 are in
+ -- effect.
+
+ -- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI
+ -- files, object files as well as the final executable.
+
+ -- 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.
+
+ -- 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
+ -- from all units stored in the auxiliary table.
+
--------------------
-- GNATprove Mode --
--------------------
-----------------------
procedure Print_Node_Header (N : Node_Id) is
- Notes : Boolean := False;
+ Enumerate : Boolean := False;
+ -- Flag set when enumerating multiple header flags
+
+ procedure Print_Header_Flag (Flag : String);
+ -- Output one of the flags that appears in a node header. The routine
+ -- automatically handles enumeration of multiple flags.
+
+ -----------------------
+ -- Print_Header_Flag --
+ -----------------------
+
+ procedure Print_Header_Flag (Flag : String) is
+ begin
+ if Enumerate then
+ Print_Char (',');
+ else
+ Enumerate := True;
+ Print_Char ('(');
+ end if;
+
+ Print_Str (Flag);
+ end Print_Header_Flag;
+
+ -- Start of processing for Print_Node_Header
begin
Print_Node_Ref (N);
return;
end if;
+ Print_Char (' ');
+
if Comes_From_Source (N) then
- Notes := True;
- Print_Str (" (source");
+ Print_Header_Flag ("source");
end if;
if Analyzed (N) then
- if not Notes then
- Notes := True;
- Print_Str (" (");
- else
- Print_Str (",");
- end if;
-
- Print_Str ("analyzed");
+ Print_Header_Flag ("analyzed");
end if;
if Error_Posted (N) then
- if not Notes then
- Notes := True;
- Print_Str (" (");
- else
- Print_Str (",");
- end if;
+ Print_Header_Flag ("posted");
+ end if;
- Print_Str ("posted");
+ if Is_Ignored_Ghost_Node (N) then
+ Print_Header_Flag ("ignored ghost");
end if;
- if Notes then
+ if Enumerate then
Print_Char (')');
end if;
projects / gcc.git / commitdiff