1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML>
<HEAD>
<TITLE>AARM95 - Pragma Reviewable</TITLE>
<META NAME="Author" CONTENT="JTC1/SC22/WG9/ARG, by Randall Brukardt, ARG Editor">
<META NAME="GENERATOR" CONTENT="Arm_Form.Exe, Ada Reference Manual generator">
<STYLE type="text/css">
DIV.paranum {position: absolute; font-family: Arial, Helvetica, sans-serif; left: 0.5 em; top: auto}
TT {font-family: "Courier New", monospace}
DT {display: compact}
DIV.Normal {font-family: "Times New Roman", Times, serif; margin-bottom: 0.6em}
DIV.Wide {font-family: "Times New Roman", Times, serif; margin-top: 0.6em; margin-bottom: 0.6em}
DIV.Annotations {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-bottom: 0.6em}
DIV.WideAnnotations {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-top: 0.6em; margin-bottom: 0.6em}
DIV.Index {font-family: "Times New Roman", Times, serif}
DIV.SyntaxSummary {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-bottom: 0.4em}
DIV.Notes {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-bottom: 0.6em}
DIV.NotesHeader {font-family: "Times New Roman", Times, serif; margin-left: 2.0em}
DIV.SyntaxIndented {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-bottom: 0.4em}
DIV.Indented {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-bottom: 0.6em}
DIV.CodeIndented {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-bottom: 0.6em}
DIV.SmallIndented {font-family: "Times New Roman", Times, serif; margin-left: 10.0em; margin-bottom: 0.6em}
DIV.SmallCodeIndented {font-family: "Times New Roman", Times, serif; margin-left: 8.0em; margin-bottom: 0.6em}
DIV.Examples {font-family: "Courier New", monospace; margin-left: 2.0em; margin-bottom: 0.6em}
DIV.SmallExamples {font-family: "Courier New", monospace; font-size: 80%; margin-left: 7.5em; margin-bottom: 0.6em}
DIV.IndentedExamples {font-family: "Courier New", monospace; margin-left: 8.0em; margin-bottom: 0.6em}
DIV.SmallIndentedExamples {font-family: "Courier New", monospace; font-size: 80%; margin-left: 15.0em; margin-bottom: 0.6em}
UL.Bulleted {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-right: 2.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.SmallBulleted {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-right: 6.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.NestedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-right: 4.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.SmallNestedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 8.0em; margin-right: 8.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.IndentedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 8.0em; margin-right: 8.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.CodeIndentedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-right: 6.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.CodeIndentedNestedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 8.0em; margin-right: 8.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.SyntaxIndentedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-right: 4.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.NotesBulleted {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-right: 4.0em; margin-top: 0em; margin-bottom: 0.5em}
UL.NotesNestedBulleted {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-right: 6.0em; margin-top: 0em; margin-bottom: 0.5em}
DL.Hanging {font-family: "Times New Roman", Times, serif; margin-top: 0em; margin-bottom: 0.6em}
DD.Hanging {margin-left: 6.0em}
DL.IndentedHanging {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-top: 0em; margin-bottom: 0.6em}
DD.IndentedHanging {margin-left: 2.0em}
DL.HangingInBulleted {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-right: 2.0em; margin-top: 0em; margin-bottom: 0.5em}
DD.HangingInBulleted {margin-left: 4.0em}
DL.SmallHanging {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-top: 0em; margin-bottom: 0.6em}
DD.SmallHanging {margin-left: 7.5em}
DL.SmallIndentedHanging {font-family: "Times New Roman", Times, serif; margin-left: 8.0em; margin-top: 0em; margin-bottom: 0.6em}
DD.SmallIndentedHanging {margin-left: 2.0em}
DL.SmallHangingInBulleted {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-right: 6.0em; margin-top: 0em; margin-bottom: 0.5em}
DD.SmallHangingInBulleted {margin-left: 5.0em}
DL.Enumerated {font-family: "Times New Roman", Times, serif; margin-right: 0.0em; margin-top: 0em; margin-bottom: 0.5em}
DD.Enumerated {margin-left: 2.0em}
DL.SmallEnumerated {font-family: "Times New Roman", Times, serif; margin-left: 4.0em; margin-right: 4.0em; margin-top: 0em; margin-bottom: 0.5em}
DD.SmallEnumerated {margin-left: 2.5em}
DL.NestedEnumerated {font-family: "Times New Roman", Times, serif; margin-left: 2.0em; margin-right: 2.0em; margin-top: 0em; margin-bottom: 0.5em}
DL.SmallNestedEnumerated {font-family: "Times New Roman", Times, serif; margin-left: 6.0em; margin-right: 6.0em; margin-top: 0em; margin-bottom: 0.5em}
</STYLE>
</HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFF0" LINK="#0000FF" VLINK="#800080" ALINK="#FF0000">
<P><A HREF="AA-TOC.html">Contents</A> <A HREF="AA-0-29.html">Index</A> <A HREF="AA-H-3.html">Previous</A> <A HREF="AA-H-3-2.html">Next</A></P>
<HR>
<H1> H.3.1 Pragma Reviewable</H1>
<DIV Class="Paranum"><FONT SIZE=-2>1</FONT></DIV>
<DIV Class="Normal"> 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.
</DIV>
<DIV Class="Paranum"><FONT SIZE=-2>1.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<H4 ALIGN=CENTER>Syntax</H4>
<DIV Class="Paranum"><FONT SIZE=-2>2</FONT></DIV>
<DIV Class="SyntaxIndented" Style="margin-bottom: 0.2em">The form of
a <FONT FACE="Arial, Helvetica">pragma</FONT> Reviewable is as follows:
</DIV>
<DIV Class="Paranum"><FONT SIZE=-2>3</FONT></DIV>
<DIV Class="SyntaxIndented"> <B>pragma</B> <A NAME="I7300"></A>Reviewable;
</DIV>
<H4 ALIGN=CENTER>Post-Compilation Rules</H4>
<DIV Class="Paranum"><FONT SIZE=-2>4</FONT></DIV>
<DIV Class="Normal"> <A NAME="I7301"></A><A NAME="I7302"></A>Pragma
Reviewable is a configuration pragma. It applies to all <FONT FACE="Arial, Helvetica">compilation_unit</FONT>s
included in a partition. </DIV>
<H4 ALIGN=CENTER>Implementation Requirements</H4>
<DIV Class="Paranum"><FONT SIZE=-2>5</FONT></DIV>
<DIV Class="Normal" Style="margin-bottom: 0.4em"> The implementation
shall provide the following information for any compilation unit to which
such a pragma applies: </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>5.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>The list of
requirements can be checked for, even if issues like intelligibility
are not addressed.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>6</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>Where compiler-generated run-time checks remain; </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>6.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>7</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>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); </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>7.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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 <I>will</I> detect such situations.
Of course, such events could well indicate a programmer error.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>8</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>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;
</LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>8.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>9</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>Where run-time support routines are implicitly invoked;
</LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>9.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>10</FONT></DIV>
<UL Class="Bulleted" Style="margin-bottom: 0.3em"><LI TYPE=DISC>An object code listing, including: </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>11</FONT></DIV>
<UL Class="NestedBulleted"><LI TYPE=DISC>Machine instructions, with relative offsets; </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>11.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>12</FONT></DIV>
<UL Class="NestedBulleted"><LI TYPE=DISC>Where each data object is stored during its lifetime; </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>12.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>This requirement
implies that if the optimizer assigns a variable to a register, this
needs to be evident.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>13</FONT></DIV>
<UL Class="NestedBulleted"><LI TYPE=DISC>Correspondence with the source program, including an identification
of the code produced per declaration and per statement. </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>13.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>14</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>An identification of each construct for which the implementation
detects the possibility of erroneous execution; </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>14.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>15</FONT></DIV>
<UL Class="Bulleted" Style="margin-bottom: 0.7em"><LI TYPE=DISC>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. </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>15.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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 <B>pragma</B> Restrictions(No_Exceptions)).
</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>16</FONT></DIV>
<DIV Class="Normal" Style="margin-bottom: 0.4em"> The implementation
shall provide the following information for any partition to which the
pragma applies: </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>17</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>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; </LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>17.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>18</FONT></DIV>
<UL Class="Bulleted"><LI TYPE=DISC>A description of the run-time model relevant to the partition.
</LI></UL>
<DIV Class="Paranum"><FONT SIZE=-2>18.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>For example,
a description of the storage model is vital, since the Ada language does
not explicitly define such a model. </FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>18.1</FONT></DIV>
<DIV Class="Normal"> <S></S>The implementation shall provide control-
and data-flow information, both within each compilation unit and across
the compilation units of the partition. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>18.b</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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.</FONT></DIV>
<H4 ALIGN=CENTER>Implementation Advice</H4>
<DIV Class="Paranum"><FONT SIZE=-2>19</FONT></DIV>
<DIV Class="Normal"> 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.</DIV>
<DIV Class="Paranum"><FONT SIZE=-2>20</FONT></DIV>
<DIV Class="Normal"> Object code listings should be provided both
in a symbolic format and also in an appropriate numeric format (such
as hexadecimal or octal). </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>20.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Reason: </B>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.</FONT></DIV>
<DIV Class="NotesHeader"><FONT SIZE=-1>NOTES</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>21</FONT></DIV>
<DIV Class="Notes"><FONT SIZE=-1>6 The order of elaboration
of library units will be documented even in the absence of <FONT FACE="Arial, Helvetica">pragma</FONT>
Reviewable (see <A HREF="AA-10-2.html">10.2</A>). </FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>21.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>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 <FONT FACE="Arial, Helvetica">pragma</FONT> Optimize (<A HREF="AA-2-8.html">2.8</A>).
</FONT></DIV>
<HR>
<P><A HREF="AA-TOC.html">Contents</A> <A HREF="AA-0-29.html">Index</A> <A HREF="AA-H-3.html">Previous</A> <A HREF="AA-H-3-2.html">Next</A> <A HREF="AA-TTL.html">Legal</A></P>
</BODY>
</HTML>
|
