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
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML>
<HEAD>
<TITLE>AARM95 - Pragma Inspection_Point</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-1.html">Previous</A> <A HREF="AA-H-4.html">Next</A></P>
<HR>
<H1> H.3.2 Pragma Inspection_Point</H1>
<DIV Class="Paranum"><FONT SIZE=-2>1</FONT></DIV>
<DIV Class="Normal"> 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. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>1.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>Inspection
points are a high level equivalent of break points used by debuggers.</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> Inspection_Point is as
follows: </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>3</FONT></DIV>
<DIV Class="SyntaxIndented"> <B>pragma</B> <A NAME="I7303"></A>Inspection_Point[(<I>object_</I><A NAME="I7304"></A><FONT FACE="Arial, Helvetica">name</FONT>
{, <I>object_</I><A NAME="I7305"></A><FONT FACE="Arial, Helvetica">name</FONT>})];
</DIV>
<H4 ALIGN=CENTER>Legality Rules</H4>
<DIV Class="Paranum"><FONT SIZE=-2>4</FONT></DIV>
<DIV Class="Normal"> A pragma Inspection_Point is allowed wherever
a <FONT FACE="Arial, Helvetica">declarative_item</FONT> or <FONT FACE="Arial, Helvetica">statement</FONT>
is allowed. Each <I>object_</I>name shall statically denote the declaration
of an object. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>4.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>The static
denotation is required, since no dynamic evaluation of a name is involved
in this pragma.</FONT></DIV>
<H4 ALIGN=CENTER>Static Semantics</H4>
<DIV Class="Paranum"><FONT SIZE=-2>5/1</FONT></DIV>
<DIV Class="Normal"> {<I><A HREF="defect1.html#8652/0093">8652/0093</A></I>}
<A NAME="I7306"></A>An <I>inspection point</I> is a point in the object
code corresponding to the occurrence of a pragma Inspection_Point in
the compilation unit. <A NAME="I7307"></A>An object is <I>inspectable</I>
at an inspection point if the corresponding pragma Inspection_Point either
has an argument denoting that object, or has no arguments<U> and the
object is visible at the inspection point</U>. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>5.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Ramification: </B>If a pragma
Inspection_Point is in an in-lined subprogram, there might be numerous
inspection points in the object code corresponding to the single occurrence
of the pragma in the source; similar considerations apply if such a pragma
is in a generic, or in a loop that has been ``unrolled'' by an optimizer.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>5.a.1/1</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1>{<I><A HREF="defect1.html#8652/0093">8652/0093</A></I>}
<U>The short form of the pragma is a convenient shorthand for listing
all objects which could be explicitly made inspectable by the long form
of the pragma; thus only visible objects are made inspectable by it.
Objects that are not visible at the point of the pragma are not made
inspectable by the short form pragma. This is necessary so that implementations
need not keep information about (or prevent optimizations on) a unit
simply because some other unit <I>might</I> contain a short form Inspection_Point
pragma.</U> </FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>5.b/1</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>{<I><A HREF="defect1.html#8652/0093">8652/0093</A></I>}
If the short form of the pragma is used, then all<U> visible</U> objects
are inspectable. This implies that <U>global objects from other compilation
units</U><S>objects out of scope at the point of the pragma</S> are inspectable.
A good interactive debugging system could provide information similar
to a post-mortem dump at such inspection points. The annex does not require
that any inspection facility is provided, merely that the information
is available to understand the state of the machine at those points.</FONT></DIV>
<H4 ALIGN=CENTER>Dynamic Semantics</H4>
<DIV Class="Paranum"><FONT SIZE=-2>6</FONT></DIV>
<DIV Class="Normal"> Execution of a pragma Inspection_Point has no
effect. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>6.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>Although an
inspection point has no (semantic) effect, the removal or adding a new
point could change the machine code generated by the compiler.</FONT></DIV>
<H4 ALIGN=CENTER>Implementation Requirements</H4>
<DIV Class="Paranum"><FONT SIZE=-2>7</FONT></DIV>
<DIV Class="Normal"> Reaching an inspection point is an external interaction
with respect to the values of the inspectable objects at that point (see
<A HREF="AA-1-1-3.html">1.1.3</A>). </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>7.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Ramification: </B>The compiler
is inhibited from moving an assignment to an inspectable variable past
an inspection point for that variable. On the other hand, the evaluation
of an expression that might raise an exception may be moved past an inspection
point (see <A HREF="AA-11-6.html">11.6</A>).</FONT></DIV>
<H4 ALIGN=CENTER>Documentation Requirements</H4>
<DIV Class="Paranum"><FONT SIZE=-2>8</FONT></DIV>
<DIV Class="Normal"> 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. </DIV>
<DIV Class="Paranum"><FONT SIZE=-2>8.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Implementation defined: </B>Implementation-defined
aspects of pragma Inspection_Point.</FONT></DIV>
<DIV Class="NotesHeader"><FONT SIZE=-1>NOTES</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>9</FONT></DIV>
<DIV Class="Notes"><FONT SIZE=-1>7 The implementation is not
allowed to perform ``dead store elimination'' on the last assignment
to a variable prior to a point where the variable is inspectable. Thus
an inspection point has the effect of an implicit reference to each of
its inspectable objects.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>10</FONT></DIV>
<DIV Class="Notes"><FONT SIZE=-1>8 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. </FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>10.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>Although it
is not a requirement of the annex, it would be useful if the state of
the stack and heap could be interrogated. This would allow users to check
that a program did not have a `storage leak'.</FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>11</FONT></DIV>
<DIV Class="Notes"><FONT SIZE=-1>9 The identification of the
mapping from source program objects to machine resources is allowed to
be in the form of an annotated object listing, in human-readable or tool-processable
form. </FONT></DIV>
<DIV Class="Paranum"><FONT SIZE=-2>11.a</FONT></DIV>
<DIV Class="Annotations"><FONT SIZE=-1><B>Discussion: </B>In principle,
it is easy to check an implementation for this pragma, since one merely
needs to check the content of objects against those values known from
the source listing. In practice, one needs a tool similar to an interactive
debugger to perform the check.</FONT></DIV>
<HR>
<P><A HREF="AA-TOC.html">Contents</A> <A HREF="AA-0-29.html">Index</A> <A HREF="AA-H-3-1.html">Previous</A> <A HREF="AA-H-4.html">Next</A> <A HREF="AA-TTL.html">Legal</A></P>
</BODY>
</HTML>
|
