diff options
Diffstat (limited to 'gcc/ada/sinfo.ads')
| -rw-r--r-- | gcc/ada/sinfo.ads | 121 |
1 files changed, 95 insertions, 26 deletions
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 6c5472a1..dd1aec5 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -528,26 +528,81 @@ package Sinfo is -- 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: + -- The SPARK RM 6.9 defines two classes of constructs - Ghost entities and + -- Ghost statements. The intent of the feature is to treat Ghost constructs + -- as non-existent when Ghost assertion policy Ignore is in effect. + + -- The corresponding nodes which map to Ghost constructs are: + + -- Ghost entities + -- Declaration nodes + -- N_Package_Body + -- N_Subprogram_Body + + -- Ghost statements + -- N_Assignment_Statement + -- N_Procedure_Call_Statement + -- N_Pragma + + -- In addition, the compiler treats instantiations as Ghost entities + + -- To achieve the removal of ignored Ghost constructs, the compiler relies + -- on global variable Ghost_Mode and a mechanism called "Ghost regions". + -- The values of the global variable are as follows: -- 1. Check - All static semantics as defined in SPARK RM 6.9 are in - -- effect. + -- effect. The Ghost region has mode Check. -- 2. Ignore - Same as Check, ignored Ghost code is not present in ALI - -- files, object files as well as the final executable. + -- files, object files, and the final executable. The Ghost region + -- has mode Ignore. + + -- 3. None - No Ghost region is in effect + + -- A Ghost region is a compiler operating mode, similar to Check_Syntax, + -- however a region is much more finely grained and depends on the policy + -- in effect. The region starts prior to the analysis of a Ghost construct + -- and ends immediately after its expansion. The region is established as + -- follows: + + -- 1. Declarations - Prior to analysis, if the declaration is subject to + -- pragma Ghost. + + -- 2. Renaming declarations - Same as 1) or when the renamed entity is + -- Ghost. - -- 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. + -- 3. Completing declarations - Same as 1) or when the declaration is + -- partially analyzed and the declaration completes a Ghost entity. + + -- 4. N_Package_Body, N_Subprogram_Body - Same as 1) or when the body is + -- partially analyzed and completes a Ghost entity. + + -- 5. N_Assignment_Statement - After the left hand side is analyzed and + -- references a Ghost entity. + + -- 6. N_Procedure_Call_Statement - After the name is analyzed and denotes + -- a Ghost procedure. + + -- 7. N_Pragma - During analysis, when the related entity is Ghost or the + -- pragma encloses a Ghost entity. + + -- 8. Instantiations - Save as 1) or when the instantiation is partially + -- analyzed and the generic template is Ghost. + + -- Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine + -- Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled + -- similar to scopes for decoupled expansion such as the generation of + -- dispatch tables or the creation of a predicate function. + + -- If the mode of a Ghost region is Ignore, any newly created nodes as well + -- as source entities are marked as ignored Ghost. In additon, the marking + -- process signals all enclosing scopes that an ignored Ghost 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 + -- driver initiates a separate pass which removes all ignored Ghost nodes -- from all units stored in the auxiliary table. -------------------- @@ -1581,6 +1636,11 @@ package Sinfo is -- be further modified (in some cases these flags are copied when a -- pragma is rewritten). + -- Is_Checked_Ghost_Pragma (Flag3-Sem) + -- This flag is present in N_Pragma nodes. It is set when the pragma is + -- related to a checked Ghost entity or encloses a checked Ghost entity. + -- This flag has no relation to Is_Checked. + -- Is_Component_Left_Opnd (Flag13-Sem) -- Is_Component_Right_Opnd (Flag14-Sem) -- Present in concatenation nodes, to indicate that the corresponding @@ -1651,11 +1711,6 @@ package Sinfo is -- Refined_State -- Test_Case - -- Is_Ghost_Pragma (Flag3-Sem) - -- This flag is present in N_Pragma nodes. It is set when the pragma is - -- either declared within a Ghost construct or it applies to a Ghost - -- construct. - -- Is_Ignored (Flag9-Sem) -- A flag set in an N_Aspect_Specification or N_Pragma node if there was -- a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma) @@ -1670,6 +1725,11 @@ package Sinfo is -- aspect/pragma is fully analyzed and checked for other syntactic -- and semantic errors, but it does not have any semantic effect. + -- Is_Ignored_Ghost_Pragma (Flag8-Sem) + -- This flag is present in N_Pragma nodes. It is set when the pragma is + -- related to an ignored Ghost entity or encloses ignored Ghost entity. + -- This flag has no relation to Is_Ignored. + -- Is_In_Discriminant_Check (Flag11-Sem) -- This flag is present in a selected component, and is used to indicate -- that the reference occurs within a discriminant check. The @@ -2519,11 +2579,12 @@ package Sinfo is -- Import_Interface_Present (Flag16-Sem) -- Is_Analyzed_Pragma (Flag5-Sem) -- Is_Checked (Flag11-Sem) + -- Is_Checked_Ghost_Pragma (Flag3-Sem) -- Is_Delayed_Aspect (Flag14-Sem) -- Is_Disabled (Flag15-Sem) -- Is_Generic_Contract_Pragma (Flag2-Sem) - -- Is_Ghost_Pragma (Flag3-Sem) -- Is_Ignored (Flag9-Sem) + -- Is_Ignored_Ghost_Pragma (Flag8-Sem) -- Is_Inherited_Pragma (Flag4-Sem) -- Split_PPC (Flag17) set if corresponding aspect had Split_PPC set -- Uneval_Old_Accept (Flag7-Sem) @@ -9364,6 +9425,9 @@ package Sinfo is function Is_Checked (N : Node_Id) return Boolean; -- Flag11 + function Is_Checked_Ghost_Pragma + (N : Node_Id) return Boolean; -- Flag3 + function Is_Component_Left_Opnd (N : Node_Id) return Boolean; -- Flag13 @@ -9403,12 +9467,12 @@ package Sinfo is function Is_Generic_Contract_Pragma (N : Node_Id) return Boolean; -- Flag2 - function Is_Ghost_Pragma - (N : Node_Id) return Boolean; -- Flag3 - function Is_Ignored (N : Node_Id) return Boolean; -- Flag9 + function Is_Ignored_Ghost_Pragma + (N : Node_Id) return Boolean; -- Flag8 + function Is_In_Discriminant_Check (N : Node_Id) return Boolean; -- Flag11 @@ -10414,6 +10478,9 @@ package Sinfo is procedure Set_Is_Checked (N : Node_Id; Val : Boolean := True); -- Flag11 + procedure Set_Is_Checked_Ghost_Pragma + (N : Node_Id; Val : Boolean := True); -- Flag3 + procedure Set_Is_Component_Left_Opnd (N : Node_Id; Val : Boolean := True); -- Flag13 @@ -10453,12 +10520,12 @@ package Sinfo is procedure Set_Is_Generic_Contract_Pragma (N : Node_Id; Val : Boolean := True); -- Flag2 - procedure Set_Is_Ghost_Pragma - (N : Node_Id; Val : Boolean := True); -- Flag3 - procedure Set_Is_Ignored (N : Node_Id; Val : Boolean := True); -- Flag9 + procedure Set_Is_Ignored_Ghost_Pragma + (N : Node_Id; Val : Boolean := True); -- Flag8 + procedure Set_Is_In_Discriminant_Check (N : Node_Id; Val : Boolean := True); -- Flag11 @@ -12865,6 +12932,7 @@ package Sinfo is pragma Inline (Is_Asynchronous_Call_Block); pragma Inline (Is_Boolean_Aspect); pragma Inline (Is_Checked); + pragma Inline (Is_Checked_Ghost_Pragma); pragma Inline (Is_Component_Left_Opnd); pragma Inline (Is_Component_Right_Opnd); pragma Inline (Is_Controlling_Actual); @@ -12878,8 +12946,8 @@ package Sinfo is pragma Inline (Is_Finalization_Wrapper); pragma Inline (Is_Folded_In_Parser); pragma Inline (Is_Generic_Contract_Pragma); - pragma Inline (Is_Ghost_Pragma); pragma Inline (Is_Ignored); + pragma Inline (Is_Ignored_Ghost_Pragma); pragma Inline (Is_In_Discriminant_Check); pragma Inline (Is_Inherited_Pragma); pragma Inline (Is_Machine_Number); @@ -13210,6 +13278,7 @@ package Sinfo is pragma Inline (Set_Is_Asynchronous_Call_Block); pragma Inline (Set_Is_Boolean_Aspect); pragma Inline (Set_Is_Checked); + pragma Inline (Set_Is_Checked_Ghost_Pragma); pragma Inline (Set_Is_Component_Left_Opnd); pragma Inline (Set_Is_Component_Right_Opnd); pragma Inline (Set_Is_Controlling_Actual); @@ -13223,8 +13292,8 @@ package Sinfo is pragma Inline (Set_Is_Finalization_Wrapper); pragma Inline (Set_Is_Folded_In_Parser); pragma Inline (Set_Is_Generic_Contract_Pragma); - pragma Inline (Set_Is_Ghost_Pragma); pragma Inline (Set_Is_Ignored); + pragma Inline (Set_Is_Ignored_Ghost_Pragma); pragma Inline (Set_Is_In_Discriminant_Check); pragma Inline (Set_Is_Inherited_Pragma); pragma Inline (Set_Is_Machine_Number); |