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.
Syntax
The form of a
pragma
Reviewable is as follows:
Post-Compilation Rules
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.
Where compiler-generated run-time checks remain;
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);
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.
{
AI95-00209-01}
For each read of a scalar object, an identification of the read as either
“known to be initialized,” or “possibly uninitialized,”
independent of whether pragma Normalize_Scalars applies;
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;
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;
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;
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.
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;
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.
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;
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.
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.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
