Pragma Inspection

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

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

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.

NOTE 1 Because reaching an inspection point is considered an external interaction relative to the values of the inspectable variables, the implementation cannot perform “dead store elimination” on the last assignment to such a variable prior to an inspection point. Thus an inspection point has the effect of an implicit read of each of its inspectable objects.

NOTE 2 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.

NOTE 3 The identification of the mapping from source program objects to machine resources can be in the form of an annotated object listing, in human-readable or tool-processable form.