- procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id);
- -- Special analyze routine for contract-case and test-case pragmas that
- -- appears within a declarative part where the pragma is associated with
- -- a subprogram specification. N is the pragma node, and S is the entity
- -- for the related subprogram. This procedure does a preanalysis of the
- -- expressions in the pragma as "spec expressions" (see section in Sem
- -- "Handling of Default and Per-Object Expressions...").
-
- procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id);
- -- Special analyze routine for precondition/postcondition pragma that
- -- appears within a declarative part where the pragma is associated
- -- with a subprogram specification. N is the pragma node, and S is the
- -- entity for the related subprogram. This procedure does a preanalysis
- -- of the expressions in the pragma as "spec expressions" (see section
- -- in Sem "Handling of Default and Per-Object Expressions...").
-
- function Check_Kind (Nam : Name_Id) return Name_Id;
- -- This function is used in connection with pragmas Assertion, Check,
- -- and assertion aspects and pragmas, to determine if Check pragmas
- -- (or corresponding assertion aspects or pragmas) are currently active
- -- as determined by the presence of -gnata on the command line (which
- -- sets the default), and the appearance of pragmas Check_Policy and
- -- Assertion_Policy as configuration pragmas either in a configuration
- -- pragma file, or at the start of the current unit, or locally given
- -- Check_Policy and Assertion_Policy pragmas that are currently active.
- --
- -- The value returned is one of the names Check, Ignore, Disable (On
- -- returns Check, and Off returns Ignore).
- --
- -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
- -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
- -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
- -- _Post, _Invariant, or _Type_Invariant, which are special names used
- -- in identifiers to represent these attribute references.
+ procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis and expansion of delayed pragma Contract_Cases
+
+ procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Depends. This routine is also
+ -- capable of performing basic analysis of pragma Refined_Depends.
+
+ procedure Analyze_Global_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Global. This routine is also
+ -- capable of performing basic analysis of pragma Refind_Global.
+
+ procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Initial_Condition
+
+ procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Initializes
+
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id);
+ -- Perform preanalysis of a [refined] precondition or postcondition that
+ -- appears on a subprogram declaration or body [stub]. Prag denotes the
+ -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis
+ -- of the expression is done as "spec expression" (see section "Handling
+ -- of Default and Per-Object Expressions in Sem).
+
+ procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
+ -- Preform full analysis of delayed pragma Refined_Depends. This routine
+ -- uses Analyze_Depends_In_Decl_Part as a starting point, then performs
+ -- various consistency checks between Depends and Refined_Depends.
+
+ procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Refined_Global. This routine
+ -- uses Analyze_Global_In_Decl_Part as a starting point, then performs
+ -- various consistency checks between Global and Refined_Global.
+
+ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Refined_State
+
+ procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
+ -- Perform preanalysis of pragma Test_Case that applies to a subprogram
+ -- declaration. Parameter N denotes the pragma, S is the entity of the
+ -- related subprogram. The preanalysis of the expression is done as "spec
+ -- expression" (see section "Handling of Default and Per-Object Expressions
+ -- in Sem).