8. Visibility Rules

8.1. Declarative Region

No extensions or restrictions.

8.2. Scope of Declarations

No extensions or restrictions.

8.3. Visibility

No extensions or restrictions.

8.3.1. Overriding Indicators

No extensions or restrictions.

8.4. Use Clauses

Legality Rules

  1. Use clauses are always in SPARK 2014, even if the unit mentioned is not completely in SPARK 2014.

8.5. Renaming Declarations

8.5.1. Object Renaming Declarations

Legality Rules

  1. [An expression or range occurring as part of an object_renaming_declaration shall not have a variable input; see Expressions for the statement of this rule.] [This rule can apply to an index of an indexed_component and the range of a slice.]

8.5.2. Exception Renaming Declarations

No extensions or restrictions.

8.5.3. Package Renaming Declarations

No extensions or restrictions.

8.5.4. Subprogram Renaming Declarations

From the point of view of both static and dynamic verification, a renaming-as-body is treated as a one-line subprogram that “calls through” to the renamed unit.

Legality Rules

  1. The aspect_specification on a subprogram_renaming_declaration shall not include any of the SPARK 2014-defined aspects introduced in this document.

8.5.5. Generic Renaming Declarations

No extensions or restrictions.

8.6. The Context of Overload Resolution

No extensions or restrictions.