diff options
Diffstat (limited to 'gcc/ada/ghost.ads')
-rw-r--r-- | gcc/ada/ghost.ads | 63 |
1 files changed, 46 insertions, 17 deletions
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index 436e84f..c267e70 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-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- -- @@ -49,6 +49,13 @@ package Ghost is -- 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_Ghost_Overriding + (Subp : Entity_Id; + Overridden_Subp : Entity_Id); + -- Verify that the Ghost policy of parent subprogram Overridden_Subp is the + -- same as the Ghost policy of overriding subprogram Subp. Emit an error if + -- this is not the case. + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean; -- Determine whether type Typ implements at least one Ghost interface @@ -68,6 +75,24 @@ package Ghost is procedure Lock; -- Lock internal tables before calling backend + 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. + + 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. + + 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. + procedure Remove_Ignored_Ghost_Code; -- Remove all code marked as ignored Ghost from the trees of all qualifying -- units. @@ -75,7 +100,7 @@ package Ghost is -- 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); + procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty); -- Set the value of global variable Ghost_Mode depending on the following -- scenarios: -- @@ -83,33 +108,37 @@ package Ghost is -- 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 completion of a deferred constant, the Ghost_Mode is set + -- based on the mode of partial declaration entity denoted by Id. + -- + -- 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. + -- + -- If N is an assignment statement or a procedure call, the Ghost_Mode is + -- set based on the mode of the name. -- - -- N is the full view of a private type, Prev_Id denotes the entity - -- of the partial declaration. + -- 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. -- - -- 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 is a pragma, the Ghost_Mode is set based on the mode of the + -- pragma. -- - -- 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. + -- If N is a freeze node, the Global_Mode is set based on the mode of + -- entity Id. -- -- 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. + procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); + -- Set the valye of global variable Ghost_Mode depending on the mode of + -- entity Id. -- -- 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 + -- Set the relevant Ghost attributes of entity Id depending on the current -- Ghost assertion policy in effect. end Ghost; |