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

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

8.5. Renaming Declarations

8.5.1. Object Renaming Declarations

Legality Rules

[An expression or range occurring as part of an object_renaming_declaration shall not have a variable input; similarly, the access-valued prefix of a dereference occurring as part of an object_renaming declaration shall not have a variable input. See Expressions for the statement of this rule.] [The first part of 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

The aspect_specification on a subprogram_renaming_declaration shall not include any of the SPARK-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.