aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/ghost.ads
diff options
context:
space:
mode:
authorHristian Kirtchev <kirtchev@adacore.com>2018-05-24 13:04:52 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-05-24 13:04:52 +0000
commit9057bd6af94f176dd904b476534cc42158799ae5 (patch)
tree997a1975d4d27d3f02d7214a4d6b041148013d1e /gcc/ada/ghost.ads
parent883ccddf496f6a6d037e72b49fee66878a11b1a1 (diff)
downloadgcc-9057bd6af94f176dd904b476534cc42158799ae5.zip
gcc-9057bd6af94f176dd904b476534cc42158799ae5.tar.gz
gcc-9057bd6af94f176dd904b476534cc42158799ae5.tar.bz2
[Ada] Fix crash on formal containers
This patch modifies several mechanisms in the compiler: 1) The handling of Ghost regions now records the start of the outermost ignored Ghost region which is currently in effect. 2) Generation of freeze actions for an arbitrary entity now inserts the actions prior to the start of the outermost ignored Ghost region when the freezing takes effect within an ignored Ghost region, but the entity being frozen is "living". This ensures that any freeze actions associated with the living entity will not be eliminated from the tree once ignored Ghost code is stripped away. 3) The Default_Initial_Condition and Invariant procedures are not treated as primitives even when they apply to tagged types. These procedures already employ class-wide precondition-like semantics to handle inheritance and overriding. In addition, the procedures cannot be invoked from source and should not be targets of dispatching calls. 2018-05-24 Hristian Kirtchev <kirtchev@adacore.com> gcc/ada/ * expander.adb (Expand): Update the save and restore of the Ghost region. * exp_ch3.adb (Freeze_Type): Likewise. * exp_disp.adb (Make_DT): Likewise. * exp_util.adb (Build_DIC_Procedure_Body): Likewise. (Build_DIC_Procedure_Declaration): Likewise. (Build_Invariant_Procedure_Body): Likewise. (Build_Invariant_Procedure_Declaration): Likewise. (Make_Predicate_Call): Likewise. * freeze.adb (Add_To_Result): Insert the freeze action of a living entity prior to the start of the enclosing ignored Ghost region. (Freeze_Entity): Update the save and restore of the Ghost region. * ghost.adb (Install_Ghost_Mode): Reimplemented. (Install_Ghost_Region): New routine. (Mark_And_Set_Ghost_Assignment): Install a region rather than a mode. (Mark_And_Set_Ghost_Body): Likewise. (Mark_And_Set_Ghost_Completion): Likewise. (Mark_And_Set_Ghost_Declaration): Likewise. (Mark_And_Set_Ghost_Instantiation): Likewise. (Mark_And_Set_Ghost_Procedure_Call): Likewise. (Name_To_Ghost_Mode): New routine. (Restore_Ghost_Region): New routine. * ghost.ads (Install_Ghost_Region): New routine. (Restore_Ghost_Region): New routine. * opt.ads: Add new global variable Ignored_Ghost_Region. * rtsfind.adb (Load_RTU): Update the save and restore of the Ghost region. Install a clean region. * sem.adb (Analyze): Likewise. (Do_Analyze): Likewise. * sem_ch3.adb (Analyze_Object_Declaration): Likewise (Derive_Progenitor_Subprograms): Use local variable Iface_Alias to capture the ultimate alias of the current primitive. (Process_Full_View): Update the save and restore of the Ghost region. Do not inherit DIC and invariant procedures. * sem_ch5.adb (Analyze_Assignment): Update the save and restore of the Ghost region. * sem_ch6.adb (Analyze_Procedure_Call): Likewise. (Analyze_Subprogram_Body_Helper): Likewise. * sem_ch7.adb (Analyze_Package_Body_Helper): Likewise. * sem_ch12.adb (Analyze_Package_Instantiation): Likewise. (Analyze_Subprogram_Instantiation): Likewise. (Instantiate_Package_Body): Likewise. (Instantiate_Subprogram_Body): Likewise. * sem_ch13.adb (Build_Predicate_Functions): Likewise. (Build_Predicate_Function_Declaration): Likewise. * sem_disp.adb (Add_Dispatching_Operation): Do not consider DIC and invariant procedures. (Check_Dispatching_Operation): Use Add_Dispatching_Operation to collect a dispatching subprogram. (Check_Operation_From_Private_View): Likewise. (Override_Dispatching_Operation): Likewise. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Update the save and restore of the Ghost region. (Analyze_Initial_Condition_In_Decl_Part): Likewise. (Analyze_Pragma): Update the save and restore of the Ghost region. (Analyze_Pre_Post_Condition_In_Decl_Part): Likewise. * sem_util.adb (Is_Suitable_Primitive): New routine. * sem_util.ads (Is_Suitable_Primitive): New routine. * sinfo.ads: Update the section of Ghost regions. gcc/testsuite/ * gnat.dg/formal_containers.adb: New testcase. From-SVN: r260648
Diffstat (limited to 'gcc/ada/ghost.ads')
-rw-r--r--gcc/ada/ghost.ads34
1 files changed, 20 insertions, 14 deletions
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 8e23bcf..ef95116 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -78,9 +78,10 @@ package Ghost is
procedure Initialize;
-- Initialize internal tables
- 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 Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+ pragma Inline (Install_Ghost_Region);
+ -- Install a Ghost region described by mode Mode and ignored region start
+ -- node N.
function Is_Ghost_Assignment (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes an assignment statement whose
@@ -111,7 +112,7 @@ package Ghost is
-- * The left hand side denotes a Ghost entity
--
-- Install the Ghost mode of the assignment statement. This routine starts
- -- a Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+ -- a Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Body
(N : Node_Id;
@@ -126,7 +127,7 @@ package Ghost is
-- * The body appears within a Ghost region
--
-- Install the Ghost mode of the body. This routine starts a Ghost region
- -- and must be used in conjunction with Restore_Ghost_Mode.
+ -- and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Completion
(N : Node_Id;
@@ -139,7 +140,7 @@ package Ghost is
-- * The completion appears within a Ghost region
--
-- Install the Ghost mode of the completion. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
-- Mark declaration N as Ghost when:
@@ -152,7 +153,7 @@ package Ghost is
-- * The declaration appears within a Ghost region
--
-- Install the Ghost mode of the declaration. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Instantiation
(N : Node_Id;
@@ -166,7 +167,7 @@ package Ghost is
-- * The instantiation appears within a Ghost region
--
-- Install the Ghost mode of the instantiation. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
-- Mark procedure call N as Ghost when:
@@ -174,7 +175,7 @@ package Ghost is
-- * The procedure being invoked is a Ghost entity
--
-- Install the Ghost mode of the procedure call. This routine starts a
- -- Ghost region and must be used in conjunction with Restore_Ghost_Mode.
+ -- Ghost region and must be used with routine Restore_Ghost_Region.
procedure Mark_Ghost_Clause (N : Node_Id);
-- Mark use package, use type, or with clause N as Ghost when:
@@ -204,14 +205,19 @@ package Ghost is
-- 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 Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+ pragma Inline (Restore_Ghost_Region);
+ -- Restore a Ghost region to a previous state described by mode Mode and
+ -- ignored region start node N. This routine must be used in conjunction
+ -- with the following routines:
+ --
+ -- Install_Ghost_Region
+ -- Mark_And_Set_xxx
+ -- Set_Ghost_Mode
procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
-- Install the Ghost mode of arbitrary node N. This routine starts a Ghost
- -- region and must be used in conjunction with Restore_Ghost_Mode.
+ -- region and must be used with routine Restore_Ghost_Region.
procedure Set_Is_Ghost_Entity (Id : Entity_Id);
-- Set the relevant Ghost attributes of entity Id depending on the current