H.3.2 Pragma Inspection_Point
An occurrence of a pragma Inspection_Point identifies
a set of objects each of whose values is to be available at the point(s)
during program execution corresponding to the position of the pragma
in the compilation unit. The purpose of such a pragma is to facilitate
code validation.
Syntax
The form of a
pragma
Inspection_Point is as follows:
pragma Inspection_Point[(
object_name
{,
object_name})];
Legality Rules
A pragma Inspection_Point is allowed wherever a
declarative_item
or
statement
is allowed. Each
object_name shall statically denote the declaration
of an object.
Static Semantics
An
inspection point is
a point in the object code corresponding to the occurrence of a pragma
Inspection_Point in the compilation unit.
An object
is
inspectable at an inspection point if the corresponding pragma
Inspection_Point either has an argument denoting that object, or has
no arguments and the declaration of the object is visible at the inspection
point.
Dynamic Semantics
Execution of a pragma Inspection_Point has no effect.
Implementation Requirements
Reaching an inspection point is an external interaction
with respect to the values of the inspectable objects at that point (see
1.1.3).
Documentation Requirements
For each inspection point, the implementation shall
identify a mapping between each inspectable object and the machine resources
(such as memory locations or registers) from which the object's value
can be obtained.
7 The implementation is not allowed to
perform “dead store elimination” on the last assignment to
a variable prior to a point where the variable is inspectable. Thus an
inspection point has the effect of an implicit read of each of its inspectable
objects.
8 Inspection points are useful in maintaining
a correspondence between the state of the program in source code terms,
and the machine state during the program's execution. Assertions about
the values of program objects can be tested in machine terms at inspection
points. Object code between inspection points can be processed by automated
tools to verify programs mechanically.
9 The identification of the mapping from
source program objects to machine resources is allowed to be in the form
of an annotated object listing, in human-readable or tool-processable
form.
Sponsored by Ada-Europe