diff options
Diffstat (limited to 'gcc/ada/ghost.ads')
| -rw-r--r-- | gcc/ada/ghost.ads | 196 |
1 files changed, 139 insertions, 57 deletions
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 7a0aec3..d5f11df 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2014-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2014-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -26,6 +26,7 @@ -- This package contains routines that deal with the static and runtime -- semantics of Ghost entities. +with Opt; use Opt; with Types; use Types; package Ghost is @@ -35,13 +36,15 @@ package Ghost is -- post processing. procedure Check_Ghost_Completion - (Partial_View : Entity_Id; - Full_View : Entity_Id); - -- Verify that the Ghost policy of a full view or a completion is the same - -- as the Ghost policy of the partial view. Emit an error if this is not - -- the case. - - procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); + (Prev_Id : Entity_Id; + Compl_Id : Entity_Id); + -- Verify that the Ghost policy of initial entity Prev_Id is compatible + -- with the Ghost policy of completing entity Compl_Id. Emit an error if + -- this is not the case. + + procedure Check_Ghost_Context + (Ghost_Id : Entity_Id; + Ghost_Ref : Node_Id); -- Determine whether node Ghost_Ref appears within a Ghost-friendly context -- where Ghost entity Ghost_Id can safely reside. @@ -71,70 +74,149 @@ package Ghost is procedure Initialize; -- Initialize internal tables - procedure Lock; - -- Lock internal tables before calling backend + procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); + -- Set the value of global variable Ghost_Mode depending on the Ghost + -- policy denoted by Mode. - procedure Mark_Full_View_As_Ghost - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id); - -- Set all Ghost-related attributes of type Full_Typ depending on the Ghost - -- mode of incomplete or private type Priv_Typ. + function Is_Ghost_Assignment (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes an assignment statement whose + -- target is a Ghost entity. - procedure Mark_Pragma_As_Ghost - (Prag : Node_Id; - Context_Id : Entity_Id); - -- Set all Ghost-related attributes of pragma Prag if its context denoted - -- by Id is a Ghost entity. + function Is_Ghost_Declaration (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a declaration which defines + -- a Ghost entity. - procedure Mark_Renaming_As_Ghost - (Ren_Decl : Node_Id; - Nam_Id : Entity_Id); - -- Set all Ghost-related attributes of renaming declaration Ren_Decl if its - -- renamed name denoted by Nam_Id is a Ghost entity. + function Is_Ghost_Pragma (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a pragma which encloses a + -- Ghost entity or is associated with a Ghost entity. - procedure Remove_Ignored_Ghost_Code; - -- Remove all code marked as ignored Ghost from the trees of all qualifying - -- units (SPARK RM 6.9(4)). - -- - -- WARNING: this is a separate front end pass, care should be taken to keep - -- it optimized. + function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean; + -- Determine whether arbitrary node N denotes a procedure call invoking a + -- Ghost procedure. - procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty); - -- Set the value of global variable Ghost_Mode depending on the following - -- scenarios: + procedure Lock; + -- Lock internal tables before calling backend + + procedure Mark_And_Set_Ghost_Assignment + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark assignment statement N as Ghost when: + -- + -- * The left hand side denotes a Ghost entity + -- + -- Install the Ghost mode of the assignment statement. Mode is the Ghost + -- mode in effect prior to processing the assignment. This routine starts + -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Body + (N : Node_Id; + Spec_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark package or subprogram body N as Ghost when: + -- + -- * The body is subject to pragma Ghost + -- + -- * The body completes a previous declaration whose spec denoted by + -- Spec_Id is a Ghost entity. + -- + -- * The body appears within a Ghost region -- - -- If N is a declaration, determine whether N is subject to pragma Ghost. - -- If this is the case, the Ghost_Mode is set based on the current Ghost - -- policy in effect. Special cases: + -- Install the Ghost mode of the body. Mode is the Ghost mode prior to + -- processing the body. This routine starts a Ghost region and must be + -- used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Completion + (N : Node_Id; + Prev_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark completion N of a deferred constant or private type [extension] + -- Ghost when: -- - -- N is the completion of a deferred constant, the Ghost_Mode is set - -- based on the mode of partial declaration entity denoted by Id. + -- * The entity of the previous declaration denoted by Prev_Id is Ghost -- - -- N is the full view of a private type, the Ghost_Mode is set based - -- on the mode of the partial declaration entity denoted by Id. + -- * The completion appears within a Ghost region -- - -- If N is an assignment statement or a procedure call, the Ghost_Mode is - -- set based on the mode of the name. + -- Install the Ghost mode of the completion. Mode is the Ghost mode prior + -- to processing the completion. This routine starts a Ghost region and + -- must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Declaration + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark declaration N as Ghost when: -- - -- If N denotes a package or a subprogram body, the Ghost_Mode is set to - -- the current Ghost policy in effect if the body is subject to Ghost or - -- the corresponding spec denoted by Id is a Ghost entity. + -- * The declaration is subject to pragma Ghost -- - -- If N is a pragma, the Ghost_Mode is set based on the mode of the - -- pragma. + -- * The declaration denotes a child package or subprogram and the parent + -- is a Ghost unit. -- - -- If N is a freeze node, the Global_Mode is set based on the mode of - -- entity Id. + -- * The declaration appears within a Ghost region -- - -- WARNING: the caller must save and restore the value of Ghost_Mode in a - -- a stack-like fasion as this routine may override the existing value. + -- Install the Ghost mode of the declaration. Mode is the Ghost mode prior + -- to processing the declaration. This routine starts a Ghost region and + -- must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Instantiation + (N : Node_Id; + Gen_Id : Entity_Id; + Mode : out Ghost_Mode_Type); + -- Mark instantiation N as Ghost when: + -- + -- * The instantiation is subject to pragma Ghost + -- + -- * The generic template denoted by Gen_Id is Ghost + -- + -- * The instantiation appears within a Ghost region + -- + -- Install the Ghost mode of the instantiation. Mode is the Ghost mode + -- prior to processing the instantiation. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_And_Set_Ghost_Procedure_Call + (N : Node_Id; + Mode : out Ghost_Mode_Type); + -- Mark procedure call N as Ghost when: + -- + -- * The procedure being invoked is a Ghost entity + -- + -- Install the Ghost mode of the procedure call. Mode is the Ghost mode + -- prior to processing the procedure call. This routine starts a Ghost + -- region and must be used in conjunction with Restore_Ghost_Mode. + + procedure Mark_Ghost_Pragma + (N : Node_Id; + Id : Entity_Id); + -- Mark pragma N as Ghost when: + -- + -- * The pragma encloses Ghost entity Id + -- + -- * The pragma is associated with Ghost entity Id - procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); - -- Set the valye of global variable Ghost_Mode depending on the mode of - -- entity Id. + procedure Mark_Ghost_Renaming + (N : Node_Id; + Id : Entity_Id); + -- Mark renaming declaration N as Ghost when: -- - -- WARNING: the caller must save and restore the value of Ghost_Mode in a - -- a stack-like fasion as this routine may override the existing value. + -- * Renamed entity Id denotes a Ghost entity + + procedure Remove_Ignored_Ghost_Code; + -- Remove all code marked as ignored Ghost from the trees of all qualifying + -- units (SPARK RM 6.9(4)). + -- + -- WARNING: this is a separate front end pass, care should be taken to keep + -- it optimized. + + procedure Restore_Ghost_Mode (Mode : Ghost_Mode_Type); + -- Terminate a Ghost region by restoring the Ghost mode prior to the + -- region denoted by Mode. This routine must be used in conjunction + -- with Mark_And_Set_xxx routines as well as Set_Ghost_Mode. + + procedure Set_Ghost_Mode + (N : Node_Or_Entity_Id; + Mode : out Ghost_Mode_Type); + -- Install the Ghost mode of arbitrary node N. Mode is the Ghost mode prior + -- to processing the node. This routine starts a Ghost region and must be + -- used in conjunction with Restore_Ghost_Mode. procedure Set_Is_Ghost_Entity (Id : Entity_Id); -- Set the relevant Ghost attributes of entity Id depending on the current |