H.3.1 Pragma Reviewable

This pragma directs the implementation to provide information to facilitate analysis and review of a program's object code, in particular to allow determination of execution time and storage usage and to identify the correspondence between the source and object programs.

1.a

Discussion: Since the purpose of this pragma is to provide information to the user, it is hard to objectively test for conformity. In practice, users want the information in an easily understood and convenient form, but neither of these properties can be easily measured.

Syntax

The form of a pragma Reviewable is as follows:

pragma Reviewable;

Post-Compilation Rules

{configuration pragma (Reviewable) [partial]} {pragma, configuration (Reviewable) [partial]} Pragma Reviewable is a configuration pragma. It applies to all compilation_units included in a partition.

Implementation Requirements

The implementation shall provide the following information for any compilation unit to which such a pragma applies:

5.a

Discussion: The list of requirements can be checked for, even if issues like intelligibility are not addressed.

Where compiler-generated run-time checks remain;

6.a

Discussion: A constraint check which is implemented via a check on the upper and lower bound should clearly be indicated. If a check is implicit in the form of machine instructions used (such an overflow checking), this should also be covered by the documentation. It is particularly important to cover those checks which are not obvious from the source code, such as that for stack overflow.

An identification of any construct with a language-defined check that is recognized prior to run time as certain to fail if executed (even if the generation of run-time checks has been suppressed);

7.a

Discussion: In this case, if the compiler determines that a check must fail, the user should be informed of this. However, since it is not in general possible to know what the compiler will detect, it is not easy to test for this. In practice, it is thought that compilers claiming conformity to this Annex will perform significant optimizations and therefore will detect such situations. Of course, such events could well indicate a programmer error.

For each reference to a scalar object, an identification of the reference as either ``known to be initialized,'' or ``possibly uninitialized,'' independent of whether pragma Normalize_Scalars applies;

8.a

Discussion: This issue again raises the question as to what the compiler has determined. A lazy implementation could clearly mark all scalars as ``possibly uninitialized'', but this would be very unhelpful to the user. It should be possible to analyze a range of scalar uses and note the percentage in each class. Note that an access marked ``known to be initialized'' does not imply that the value is in range, since the initialization could be from an (erroneous) call of unchecked conversion, or by means external to the Ada program.

Where run-time support routines are implicitly invoked;

9.a

Discussion: Validators will need to know the calls invoked in order to check for the correct functionality. For instance, for some safety applications, it may be necessary to ensure that certain sections of code can execute in a particular time.

An object code listing, including:

Machine instructions, with relative offsets;

11.a

Discussion: The machine instructions should be in a format that is easily understood, such as the symbolic format of the assembler. The relative offsets are needed in numeric format, to check any alignment restrictions that the architecture might impose.

Where each data object is stored during its lifetime;

12.a

Discussion: This requirement implies that if the optimizer assigns a variable to a register, this needs to be evident.

Correspondence with the source program, including an identification of the code produced per declaration and per statement.

13.a

Discussion: This correspondence will be quite complex when extensive optimization is performed. In particular, address calculation to access some data structures could be moved from the actual access. However, when all the machine code arising from a statement or declaration is in one basic block, this must be indicated by the implementation.

An identification of each construct for which the implementation detects the possibility of erroneous execution;

14.a

Discussion: This requirement is quite vague. In general, it is hard for compilers to detect erroneous execution and therefore the requirement will be rarely invoked. However, if the pragma Suppress is used and the compiler can show that a predefined exception will be raised, then such an identification would be useful.

For each subprogram, block, task, or other construct implemented by reserving and subsequently freeing an area on a run-time stack, an identification of the length of the fixed-size portion of the area and an indication of whether the non-fixed size portion is reserved on the stack or in a dynamically-managed storage region.

15.a

Discussion: This requirement is vital for those requiring to show that the storage available to a program is sufficient. This is crucial in those cases in which the internal checks for stack overflow are suppressed (perhaps by pragma Restrictions(No_Exceptions)).

The implementation shall provide the following information for any partition to which the pragma applies:

An object code listing of the entire partition, including initialization and finalization code as well as run-time system components, and with an identification of those instructions and data that will be relocated at load time;

17.a

Discussion: The object code listing should enable a validator to estimate upper bounds for the time taken by critical parts of a program. Similarly, by an analysis of the entire partition, it should be possible to ensure that the storage requirements are suitably bounded, assuming that the partition was written in an appropriate manner.

A description of the run-time model relevant to the partition.

18.a

Discussion: For example, a description of the storage model is vital, since the Ada language does not explicitly define such a model.

18.1

The implementation shall provide control- and data-flow information, both within each compilation unit and across the compilation units of the partition.

18.b

Discussion: This requirement is quite vague, since it is unclear what control and data flow information the compiler has produced. It is really a plea not to throw away information that could be useful to the validator. Note that the data flow information is relevant to the detection of ``possibly uninitialized'' objects referred to above.

Implementation Advice

The implementation should provide the above information in both a human-readable and machine-readable form, and should document the latter so as to ease further processing by automated tools.

Object code listings should be provided both in a symbolic format and also in an appropriate numeric format (such as hexadecimal or octal).

20.a

Reason: This is to enable other tools to perform any analysis that the user needed to aid validation. The format should be in some agreed form.

NOTES

6 The order of elaboration of library units will be documented even in the absence of pragma Reviewable (see 10.2).

21.a

Discussion: There might be some interactions between pragma Reviewable and compiler optimizations. For example, an implementation may disable some optimizations when pragma Reviewable is in force if it would be overly complicated to provide the detailed information to allow review of the optimized object code. See also pragma Optimize (2.8).

Contents Index Search Previous Next Legal