Annotated Ada Reference ManualLegal Information
Table of Contents   Index   References   Search   Previous   Next 

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


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: 
Discussion: The list of requirements can be checked for, even if issues like intelligibility are not addressed.
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.
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.
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.
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.
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.
Discussion: This requirement implies that if the optimizer assigns a variable to a register, this needs to be evident.
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.
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.
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: 
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.
Discussion: For example, a description of the storage model is vital, since the Ada language does not explicitly define such a model. 
 The implementation shall provide control- and data-flow information, both within each compilation unit and across the compilation units of the partition. 
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. 
Implementation Advice: The information produced by pragma Reviewable should be provided in both a human-readable and machine-readable form, and the latter form should be documented.
Object code listings should be provided both in a symbolic format and also in an appropriate numeric format (such as hexadecimal or octal). 
Implementation Advice: Object code listings should be provided both in a symbolic format and in a numeric format.
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.
6  The order of elaboration of library units will be documented even in the absence of pragma Reviewable (see 10.2). 
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). 

Wording Changes from Ada 95

{AI95-00209-01} The wording was clarified that pragma Reviewable applies to each read of an object, as it makes no sense to talk about the state of an object that will immediately be overwritten. 

Table of Contents   Index   References   Search   Previous   Next 
Ada-Europe Sponsored by Ada-Europe