aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/ghost.ads
diff options
context:
space:
mode:
Diffstat (limited to 'gcc/ada/ghost.ads')
-rw-r--r--gcc/ada/ghost.ads63
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;