File: safety.mss

package info (click to toggle)
ada-reference-manual 1%3A2012.3-2
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 12,872 kB
  • sloc: ada: 29,393; makefile: 193; python: 92
file content (1277 lines) | stat: -rwxr-xr-x 52,642 bytes parent folder | download | duplicates (6)
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
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
@Comment{ $Source: e:\\cvsroot/ARM/Source/safety.mss,v $ }
@Comment{ $Revision: 1.39 $ $Date: 2006/10/19 06:40:32 $ $Author: Randy $ }
@Part(safety, Root="ada.mss")

@Comment{$Date: 2006/10/19 06:40:32 $}
@LabeledRevisedNormativeAnnex{Version=[2],
New=[High Integrity Systems], Old=[Safety and Security]}

@begin{Intro}
@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00347-01]}
@Leading@Defn{safety-critical systems}
@Defn{secure systems}
This Annex addresses requirements for @Chg{Version=[2],
New=[high integrity ],Old=[]}systems @Chg{Version=[2],New=[(including],
Old=[that are]} safety@Chg{Version=[2],New=[-],Old=[ ]}critical
@Chg{Version=[2],New=[systems and],Old=[or have]}
security@Chg{Version=[2],New=[-critical systems)],Old=[ constraints]}. It
provides facilities and specifies documentation requirements that relate to
several needs:
@begin{Itemize}
Understanding program execution;

Reviewing object code;

Restricting language constructs whose usage might
complicate the demonstration of program correctness
@end{Itemize}
@ChgNote{The following paragraph is missing a number in the original version.
To give it a number in the new version, it is marked as an insertion.}
@ChgRef{Version=[0],Kind=[Added]}
@Chg{New=[],Old=[@Noparanum@;]}Execution understandability
is supported by pragma Normalize_Scalars, and also by
requirements for the implementation to document the effect of a program
in the presence of a bounded error or where the language rules leave
the effect unspecified.
@PDefn{unspecified}

The @nt[pragma]s Reviewable and Restrictions relate to the other
requirements addressed by this Annex.
@end{Intro}

@begin{Notes}
The @attr[Valid] attribute (see @RefSecNum(The Valid Attribute)) is
also useful in addressing these needs,
to avoid problems that could otherwise arise from scalars
that have values outside their declared range constraints.
@begin{Discussion}

The Annex tries to provide high assurance rather than language features.
However, it is not possible, in general, to test for high assurance. For any
specific language feature, it is possible to demonstrate its presence by a
functional test, as in the ACVC. One can also check for the presence of some
documentation requirements, but it is not easy to determine objectively that
the documentation is @lquotes@;adequate@rquotes@;.

@end{Discussion}
@end{Notes}

@begin{Extend83}
@Defn{extensions to Ada 83}
This Annex is new to Ada 95.
@end{Extend83}

@begin{DiffWord95}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00347-01]}
  @ChgAdded{Version=[2],Text=[The title of this annex was changed to better
  reflect its purpose and scope. High integrity systems has become the standard
  way of identifying systems that have high reliability requirements; it
  subsumes terms such as safety and security. Moreover, the annex does not
  include any security specific features and as such the previous title is
  somewhat misleading.]}
@end{DiffWord95}

@LabeledClause{Pragma Normalize_Scalars}
@begin{Intro}
This pragma ensures that an otherwise
uninitialized scalar object is set to a
predictable value, but out of range if possible.
@begin[discussion]
The goal of the pragma is to reduce the impact of a bounded error
that results from a reference to an uninitialized scalar object, by
having such a reference violate a range check and thus raise
Constraint_Error.
@end[discussion]
@end{Intro}

@begin{Syntax}
@begin{SyntaxText}
@Leading@Keepnext@;The form of a @nt{pragma} Normalize_Scalars is as follows:
@end{SyntaxText}

@PragmaSyn`@key{pragma} @prag(Normalize_Scalars);'
@end{Syntax}

@begin{LinkTime}
@PDefn2{Term=[configuration pragma], Sec=(Normalize_Scalars)}
@PDefn2{Term=[pragma, configuration], Sec=(Normalize_Scalars)}
Pragma Normalize_Scalars is a configuration pragma.
It applies to all
@nt[compilation_unit]s included in a partition.
@end{LinkTime}

@begin{DocReq}
@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00434-01]}
If a @nt{pragma} Normalize_Scalars applies,
the implementation shall document the implicit initial @Chg{Version=[2],
New=[values],Old=[value]} for scalar subtypes,
and shall identify each case in which such a value is used
and is not an invalid representation.
@ChgDocReq{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],Text=[If
a @nt{pragma} Normalize_Scalars applies, the implicit initial values of
scalar subtypes shall be documented. Such a value should be an
invalid representation when possible; any cases when is it not shall be
documented.]}]}
@begin{Honest}
It's slightly inaccurate to say that the value is a
representation, but the point should be clear anyway.
@end{Honest}
@begin{Discussion}

By providing a type with a size specification so that spare bits are
present, it is possible to force an implementation of Normalize_Scalars to use
an out of range value. This can be tested for by ensuring that
Constraint_Error is raised. Similarly, for an unconstrained integer type, in
which no spare bit is surely present, one can check that the initialization
takes place to the value specified in the documentation of the
implementation. For a floating point type, spare bits might not
be available, but a range constraint can provide the ability to use an out
of range value.

If it is difficult to document the general rule for the implicit initial
value, the implementation might choose instead to record the value on
the object code listing or similar output produced during compilation.

@end{Discussion}
@end{DocReq}

@begin{ImplAdvice}
@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00434-01]}
Whenever possible, the implicit initial @Chg{Version=[2],
New=[values],Old=[value]} for a scalar subtype
should be an invalid representation
(see @RefSecNum{Data Validity}).
@begin{Discussion}

  When an out of range value is used for the initialization,
  it is likely that constraint checks will detect it.
  In addition, it can be detected by the Valid attribute.

  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[This rule is included in the documentation
  requirements, and thus does not need a separate summary item.]}

@end{Discussion}
@end{ImplAdvice}

@begin{Notes}
The initialization requirement applies to
uninitialized scalar objects that are subcomponents of composite
objects, to allocated objects, and to stand-alone objects. It also
applies to scalar @key{out} parameters. Scalar
subcomponents of composite @key{out} parameters are initialized to the
corresponding part of the actual, by virtue of
@RefSecNum(Parameter Associations).

The initialization requirement does not apply to a scalar for which
pragma Import has been specified,
since initialization of an imported object is performed
solely by the foreign language environment
 (see @RefSecNum[Interfacing Pragmas]).

The use of pragma Normalize_Scalars in conjunction with
Pragma Restrictions(No_Exceptions) may result in erroneous execution
(see @RefSecNum[High Integrity Restrictions]).
@begin{Discussion}

Since the effect of an access to an out of range value will often be to
raise Constraint_Error, it is clear that suppressing the exception mechanism
could result in erroneous execution. In particular, the assignment to an
array, with the array index out of range, will result in a write to an
arbitrary store location, having unpredictable effects.

@end{Discussion}
@end{Notes}

@LabeledClause{Documentation of Implementation Decisions}

@begin{DocReq}
@PDefn{unspecified}
The implementation shall document the range of effects for each
situation that the language rules identify as either a
bounded error or as having an unspecified effect.
If the implementation can constrain the effects of erroneous
execution for a given construct,
then it shall document such constraints.
@Redundant[The documentation might be provided either
independently of any compilation unit or partition, or as part of an annotated
listing for a given unit or partition.
See also @RefSecNum(Conformity of an Implementation with the Standard), and
@RefSecNum(Structure).]
@ChgImplDef{Version=[2],Kind=[Deleted],Text=[@ChgDeleted{Version=[2],
Text=[Information regarding bounded errors and erroneous execution.]}]}
@ChgDocReq{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],Text=[
The range of effects for each bounded error and each unspecified effect.
If the effects of a given erroneous construct are
constrained, the constraints shall be documented.]}]}

@end{DocReq}

@begin{Notes}
Among the situations to be
documented are the conventions
chosen for parameter passing, the methods used for the management of
run-time storage, and the method used to evaluate numeric expressions if
this involves extended range or extra precision.
@begin{Discussion}

Look up @lquotes@;unspecified@rquotes@; and @lquotes@;erroneous execution@rquotes@;
in the index for a list of the cases.

The management of run-time storage is particularly important. For safety
applications, it is often necessary to show that a program cannot raise
Storage_Error, and for security applications that information cannot leak
via the run-time system. Users are likely to prefer a simple storage model
that can be easily validated.

The documentation could helpfully take into account that users may well
adopt a subset to avoid some forms of erroneous execution, for instance, not
using the abort statement, so that the effects of a partly completed
@nt{assignment_statement} do not have to be considered in the validation of a
program
(see @RefSecNum{Abort of a Task - Abort of a Sequence of Statements}).
For this reason documentation linked to an actual compilation may be
most useful. Similarly, an implementation may be able to take into
account use of the Restrictions pragma.

@end{Discussion}
@end{Notes}


@LabeledClause{Reviewable Object Code}

@begin{Intro}
Object code review and validation are supported by
pragmas Reviewable and Inspection_Point.
@end{Intro}

@LabeledSubClause{Pragma Reviewable}
@begin{Intro}
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.
@begin{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.

@end{Discussion}
@end{Intro}

@begin{Syntax}
@begin{SyntaxText}
@Leading@Keepnext@;The form of a @nt{pragma} Reviewable is as follows:
@end{SyntaxText}

@PragmaSyn`@key{pragma} @prag(Reviewable);'
@end{Syntax}

@begin{LinkTime}
@PDefn2{Term=[configuration pragma], Sec=(Reviewable)}
@PDefn2{Term=[pragma, configuration], Sec=(Reviewable)}
Pragma Reviewable is a configuration pragma.
It applies to all
@nt[compilation_unit]s included in a partition.
@end{LinkTime}

@begin{ImplReq}
@Leading@;The implementation shall provide the following
information for any compilation unit to which such a
pragma applies:
@begin{Discussion}

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

@end{Discussion}
@begin{itemize}
Where compiler-generated run-time checks remain;
@begin{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.

@end{Discussion}

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);
@begin{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 @i{will} detect such
situations. Of course, such events could well indicate a programmer error.

@end{Discussion}

@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00209-01]}
For each @Chg{Version=[2],New=[read of],Old=[reference to]} a scalar object,
an identification of the @Chg{Version=[2],New=[read],Old=[reference]} as
either @lquotes@;known to be initialized,@rquotes@; or
@lquotes@;possibly uninitialized,@rquotes@;
independent of whether pragma Normalize_Scalars applies;
@begin{Discussion}

This issue again raises the question as to what the compiler has determined.
A lazy implementation could clearly mark all scalars as @lquotes@;possibly
uninitialized@rquotes@;, 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 @lquotes@;known to be initialized@rquotes@; 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.

@end{Discussion}

Where run-time support routines are implicitly invoked;
@begin{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.

@end{Discussion}

@Leading@Keepnext@;An object code listing, including:
@begin{inneritemize}
Machine instructions, with relative offsets;
@begin{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.

@end{Discussion}

Where each data object is stored during its lifetime;
@begin{Discussion}

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

@end{Discussion}

Correspondence with the source program, including an identification of the
 code produced per declaration and per statement.
@begin{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.

@end{Discussion}
@end{inneritemize}

An identification of each construct for which the implementation detects
the possibility of erroneous execution;
@begin{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.

@end{Discussion}

@Trailing@;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.
@begin{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
@key[pragma] Restrictions(No_Exceptions)).
@end{Discussion}
@end{itemize}

@Leading@;The implementation shall provide the following
information for any partition to which the
pragma applies:
@begin{Itemize}
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;
@begin{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.@end{discussion}

A description of the run-time model relevant to the partition.
@begin{Discussion}
For example,
a description of the storage model is vital,
since the Ada language does not explicitly define such a model.
@end{Discussion}
@end{itemize}
@end{ImplReq}

@Chgnote{The following paragraph is missing a number in the original version.
To give it a number in the new version, it is marked as an insertion.}
@ChgRef{Version=[0],Kind=[Added]}
@Chg{New=[],Old=[@Noparanum@;]}The implementation shall provide control- and data-flow
information, both within each compilation unit and across
the compilation units of the partition.
@begin{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 @lquotes@;possibly uninitialized@rquotes@;
objects referred to above.

@end{Discussion}
@begin{ImplAdvice}
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.
@ChgImplAdvice{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],
Text=[The information produced by @nt{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).
@ChgImplAdvice{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],
Text=[Object code listings should be provided both in a symbolic
format and in a numeric format.]}]}
@begin{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.

@end{Reason}
@end{ImplAdvice}

@begin{Notes}
The order of elaboration of library units will be documented
even in the absence of @nt[pragma] Reviewable
(see @RefSecNum{Program Execution}).
@end{Notes}

@begin[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 @nt<pragma> Optimize (@RefSecNum{Pragmas}).
@end[discussion]

@begin{DiffWord95}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00209-01]}
  @ChgAdded{Version=[2],Text=[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.]}
@end{DiffWord95}

@LabeledSubClause{Pragma Inspection_Point}
@begin{Intro}
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.
@begin{Discussion}

Inspection points are a high level equivalent of break points used by
debuggers.

@end{Discussion}
@end{Intro}

@begin{Syntax}
@begin{SyntaxText}
@Leading@Keepnext@;The form of a @nt{pragma} Inspection_Point is as follows:
@end{SyntaxText}

@PragmaSyn`@key{pragma} @prag(Inspection_Point)[(@SynI{object_}@Syn2{name} {, @SynI{object_}@Syn2{name}})];'
@end{Syntax}

@begin{Legality}
A pragma Inspection_Point is allowed wherever a
@nt[declarative_item]
or @nt[statement] is allowed.
Each @SynI{object_}name shall statically denote the declaration of an object.
@begin{Discussion}

The static denotation is required, since no dynamic evaluation of a name
is involved in this pragma.

@end{Discussion}
@end{Legality}

@begin{StaticSem}
@ChgRef{Version=[1],Kind=[Revised],Ref=[8652/0093],ARef=[AI95-00207-01]}
@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00434-01]}
@Defn{inspection point}
An @i{inspection point} is a point in the object code
corresponding to the occurrence of a pragma Inspection_@!Point in the
compilation unit.
@Defn{inspectable object}
An object is @i{inspectable} at an inspection point if the corresponding
pragma Inspection_Point either has an argument denoting that object,
or has no arguments@Chg{New=[ and the @Chg{Version=[2],New=[declaration
of the ],Old=[]}object is visible at the inspection point],Old=[]}.
@begin{ramification}
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 @lquotes@;unrolled@rquotes@; by an optimizer.

@ChgRef{Version=[1],Kind=[Added],Ref=[8652/0093],ARef=[AI95-00207-01]}
@ChgAdded{Version=[1],Text=[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> contain a short form Inspection_Point
pragma.]}
@end{ramification}
@begin{Discussion}
@ChgRef{Version=[1],Kind=[Revised],Ref=[8652/0093],ARef=[AI95-00207-01]}
If the short form of the pragma is used, then all@Chg{New=[ visible],Old=[]}
objects are inspectable.
This implies that @Chg{New=[global objects from other compilation units],
Old=[objects out of scope at the point of the pragma]} 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.
@end{Discussion}
@end{StaticSem}

@begin{RunTime}
Execution of a pragma Inspection_Point has no effect.
@begin{Discussion}

@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00114-01]}
Although an inspection point has no (semantic) effect,
the removal or adding @Chg{Version=[2],New=[of ],Old=[]}a new point could
change the machine code generated by the compiler.

@end{Discussion}
@end{RunTime}

@begin{ImplReq}
Reaching an inspection point is an external interaction
with respect to the values
of the inspectable objects at that point
(see @RefSecNum{Conformity of an Implementation with the Standard}).
@begin{Ramification}
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 @RefSecNum[Exceptions and Optimization]).@end{ramification}
@end{ImplReq}

@begin{DocReq}
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.
@ChgImplDef{Version=[2],Kind=[Deleted],Text=[@ChgDeleted{Version=[2],
Text=[Implementation-defined aspects of pragma Inspection_Point.]}]}
@ChgDocReq{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],
Text=[For each inspection point, a mapping between each inspectable object
and the machine resources where the object's value can be obtained shall
be provided.]}]}
@end{DocReq}

@begin{Notes}
@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00209-01]}
The implementation is not allowed to perform @lquotes@;dead store elimination@rquotes@; 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 @Chg{Version=[2],New=[read of],Old=[reference to]} each of its
inspectable objects.

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.
@begin{Discussion}

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

@end{Discussion}

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.
@begin{Discussion}

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.

@end{Discussion}
@end{Notes}

@begin{DiffWord95}
@ChgRef{Version=[2],Kind=[AddedNormal],Ref=[8652/0093],ARef=[AI95-00207-01]}
@ChgAdded{Version=[2],Text=[@b<Corrigendum:> Corrected the definition of
the Inspection_Point pragma to apply to only variables visible at the point
of the pragma. Otherwise, the compiler would have to assume that some
other code somewhere could have a pragma Inspection_Point, preventing many
optimizations (such as unused object elimination).]}
@end{DiffWord95}


@LabeledRevisedClause{Version=[2],New=[High Integrity Restrictions],Old=[Safety and Security Restrictions]}
@begin{Intro}
This clause defines restrictions that can be used with pragma
Restrictions (see @RefSecNum(Pragma Restrictions)); these facilitate
the demonstration of program correctness by allowing
tailored versions of the run-time system.
@begin{Discussion}

Note that the restrictions are absolute. If a partition has 100 library
units and just one needs Unchecked_Conversion, then the pragma cannot be
used to ensure the other 99 units do not use Unchecked_Conversion. Note also
that these are restrictions on all Ada code within a partition, and
therefore it may not be evident from the specification of a package whether
a restriction can be imposed.

@end{Discussion}
@end{Intro}

@begin{StaticSem}
@ChgRef{Version=[2],Kind=[Deleted],ARef=[AI95-00347-01],ARef=[AI95-00394-01]}
@ChgDeleted{Version=[2],Text=[The following restrictions,
the same as in @RefSecNum{Tasking Restrictions},
apply in this Annex:
 No_Task_@!Hierarchy,
 No_Abort_@!Statement,
 No_Implicit_@!Heap_@!Allocation,
 Max_@!Task_@!Entries is 0,
 Max_@!Asynchronous_@!Select_@!Nesting is 0, and
 Max_@!Tasks is 0.
@redundant[The last three restrictions are checked prior to program execution.]]}

@Trailing@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00394-01]}
The following @Chg{Version=[2],New=[@SynI{restriction_}@nt{identifier}s are
language defined:],Old=[additional restrictions apply in this Annex.]}

@leading@keepnext@b{Tasking-related restriction:}

@begin{Description}
@Trailing@;@Defn2{Term=[Restrictions],Sec=(No_Protected_Types)}No_Protected_Types @\There
are no declarations of protected types or protected objects.
@end{Description}

@leading@keepnext@b{Memory-management related restrictions:}

@begin{Description}
@Defn2{Term=[Restrictions],Sec=(No_Allocators)}No_Allocators @\There are no
occurrences of an @nt{allocator}.

@ChgRef{Version=[1],Kind=[Revised],Ref=[8652/0042],ARef=[AI95-00130]}
@Defn2{Term=[Restrictions],Sec=(No_Local_Allocators)}No_Local_Allocators @\@nt{Allocator}s
are prohibited in subprograms, generic subprograms,
tasks, and entry bodies@Chg{New=[],Old=[; instantiations of generic packages
are also prohibited in these contexts]}.
@begin[Ramification]
Thus @nt{allocator}s are permitted only in expressions whose
evaluation can only be performed before the main subprogram is invoked.
@end[Ramification]
@begin[Reason]
@ChgRef{Version=[1],Kind=[Deleted],Ref=[8652/0042],ARef=[AI95-00130]}
@ChgNote{The associated rule has been deleted.}
@ChgDeleted{Version=[1],Text=[The reason for the prohibition against
instantiations of
generic packages is to avoid contract model violations.
An alternative would be to prohibit @nt{allocator}s from generic
packages, but it seems preferable to allow generality on the
defining side and then place the restrictions on the usage (instantiation),
rather than inhibiting what can be in the generic while
liberalizing where they can be instantiated.]}
@end[Reason]

@ChgRef{Version=[2],Kind=[Deleted],ARef=[AI95-00394-01]}
@ChgDeleted{Version=[2],Text=[@Defn2{Term=[Restrictions],
Sec=(No_Unchecked_Deallocation)}No_Unchecked_Deallocation @\Semantic
dependence on Unchecked_Deallocation is not allowed.]}
@begin{Discussion}
  @ChgRef{Version=[2],Kind=[Deleted]}
  @ChgDeleted{Version=[2],Text=[This restriction would be useful in those
  contexts in which heap storage is needed on program start-up, but need not be
  increased subsequently. The danger of a dangling pointer can therefore be
  avoided.]}
@end{Discussion}

@Trailing@;Immediate_Reclamation @\Except for storage occupied by objects created by
@nt{allocator}s and not deallocated via unchecked deallocation, any storage
reserved at run time for an object is immediately reclaimed when the
object no longer exists.
@Defn2{Term=[Restrictions],Sec=(Immediate_Reclamation)}
@begin{Discussion}
Immediate reclamation would apply to storage created by the compiler, such
as for a return value from a function whose size is not known at the
call site.
@end{Discussion}
@end{Description}

@leading@keepnext@b{Exception-related restriction:}

@begin{Description}
@Trailing@Defn2{Term=[Restrictions],Sec=(No_Exceptions)}No_Exceptions @\@nt{Raise_statement}s
and @nt{exception_handler}s are not allowed.
No language-defined run-time checks are generated;
however, a run-time check performed automatically by the hardware
is permitted.
@begin{Discussion}

This restriction mirrors a method of working that is quite common in the
safety area. The programmer is required to show that exceptions cannot be
raised. Then a simplified run-time system is used without exception
handling. However, some hardware checks may still be enforced. If the
software check would have failed, or if the hardware check actually fails,
then the execution of the program is unpredictable.
There are obvious dangers in this approach, but it is similar to
programming at the assembler level.

@end{Discussion}
@end{Description}

@leading@keepnext@b{Other restrictions:}

@begin{Description}
@Defn2{Term=[Restrictions],Sec=(No_Floating_Point)}No_Floating_Point @\Uses of predefined floating point types and
operations, and declarations of new floating point types, are
not allowed.
@begin{Discussion}

@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00114-01]}
The intention is to avoid the use of floating point hardware at run time,
but this is expressed in
language terms. It is conceivable that floating point is used implicitly in
some contexts, say fixed point type conversions of high accuracy. However,
the @ImplReqTitle below make it clear that the restriction would apply
to the @lquotes@;run-time system@rquotes@; and hence not be allowed.
This @Chg{Version=[2],New=[restriction],Old=[parameter]} could be used to
inform a compiler that a variant of the architecture is being used which does
not have floating point instructions.

@end{Discussion}

@Defn2{Term=[Restrictions],Sec=(No_Fixed_Point)}No_Fixed_Point @\Uses of predefined fixed point types and
operations, and declarations of new fixed point types, are
not allowed.
@begin{Discussion}

This restriction would have the side-effect of prohibiting the
@nt{delay_relative_statement}.
As with the No_Floating_Point restriction, this might be used to
avoid any question of rounding errors. Unless an Ada run-time is written in
Ada, it seems hard to rule out implicit use of fixed point, since at the
machine level, fixed point is virtually the same as integer arithmetic.

@end{Discussion}

@ChgRef{Version=[2],Kind=[Deleted],ARef=[AI95-00394-01]}
@ChgDeleted{Version=[2],Text=[@Defn2{Term=[Restrictions],
Sec=(No_Unchecked_Conversion)}No_Unchecked_Conversion @\Semantic dependence
on the predefined generic Unchecked_Conversion is not allowed.]}
@begin{Discussion}
  @ChgRef{Version=[2],Kind=[Deleted]}
  @ChgDeleted{Version=[2],Text=[Most critical applications would require
  some restrictions or additional validation checks on uses of unchecked
  conversion. If the application does not require the functionality, then
  this restriction provides a means of ensuring the design requirement has
  been satisfied. The same applies to several of the following restrictions.]}
@end{Discussion}

No_Access_Subprograms @\The declaration of access-to-subprogram types
is not allowed.
@Defn2{Term=[Restrictions],Sec=(No_Access_Subprograms)}
@begin{Discussion}@ChgNote{Moved from above}
  @ChgRef{Version=[2],Kind=[Added]}
  @ChgAdded{Version=[2],Text=[Most critical applications would require
  some restrictions or additional validation checks on uses of
  access-to-subprogram types. If the application does not require the
  functionality, then this restriction provides a means of ensuring the design
  requirement has been satisfied. The same applies to several of the following
  restrictions, and to restriction No_Dependence => Ada.Unchecked_Conversion.]}
@end{Discussion}

@Defn2{Term=[Restrictions],Sec=(No_Unchecked_Access)}No_Unchecked_Access @\The @attr[Unchecked_Access] attribute
is not allowed.

@Defn2{Term=[Restrictions],Sec=(No_Dispatch)}No_Dispatch @\Occurrences of T'Class are not allowed, for any
(tagged)
subtype T.

@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00285-01]}
@Defn2{Term=[Restrictions],Sec=(No_IO)}No_IO @\Semantic dependence on
any of the library units
Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, @Chg{Version=[2],
New=[Wide_Wide_Text_IO, ],Old=[]}or Stream_IO is not allowed.
@begin{Discussion}

Excluding the input-output facilities of an implementation may be needed
in those environments which cannot support the supplied functionality.
A program in such an environment is likely to require some low level
facilities or a call on a non-Ada feature.

@end{Discussion}

@Defn2{Term=[Restrictions],Sec=(No_Delay)}No_Delay @\@nt[Delay_Statement]s
and semantic dependence on package Calendar
are not allowed.
@begin[Ramification]
This implies that @nt[delay_alternative]s in a
@nt[select_statement] are prohibited.

The purpose of this restriction is to avoid the need for timing facilities
within the run-time system.

@end[ramification]

@Defn2{Term=[Restrictions],Sec=(No_Recursion)}No_Recursion @\As part of the execution of a subprogram, the same
subprogram is not invoked.

@Defn2{Term=[Restrictions],Sec=(No_Reentrancy)}No_Reentrancy @\During the execution of a subprogram by a task, no other
task invokes the same subprogram.

@end{description}
@end{StaticSem}

@begin{ImplReq}

@ChgRef{Version=[2],Kind=[Added],ARef=[AI95-00394-01]}
@ChgAdded{Version=[2],Type=[Leading],Text=[An implementation of this Annex
shall support:]}
@begin{Itemize}
@ChgRef{Version=[2],Kind=[Added]}
@ChgAdded{Version=[2],Text=[the restrictions defined in this subclause; and]}

@ChgRef{Version=[2],Kind=[Added]}
@ChgAdded{Version=[2],Text=[the following restrictions defined in
@RefSecNum{Tasking Restrictions}: No_Task_Hierarchy,
No_Abort_Statement, No_Implicit_Heap_Allocation; and]}

@ChgRef{Version=[2],Kind=[Added],ARef=[AI95-00347-01]}
@ChgAdded{Version=[2],Text=[the @key{pragma} Profile(Ravenscar); and]}
@begin{Discussion}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00347-01]}
  @ChgAdded{Version=[2],Text=[The reference to pragma Profile(Ravenscar) is
  intended to show that properly restricted tasking is appropriate for use
  in high integrity systems. The Ada 95
  Annex seemed to suggest that tasking was inappropriate for such systems.]}
@end{Discussion}

@ChgRef{Version=[2],Kind=[Added]}
@ChgAdded{Version=[2],Type=[Leading],Text=[the following uses of
@SynI{restriction_parameter_}@nt{identifier}s defined in
@RefSecNum{Tasking Restrictions}@Redundant[, which are checked
prior to program execution]:]}
@begin{InnerItemize}
  @ChgRef{Version=[2],Kind=[Added]}
  @ChgAdded{Version=[2],Text=[Max_Task_Entries => 0,]}

  @ChgRef{Version=[2],Kind=[Added]}
  @ChgAdded{Version=[2],Text=[Max_Asynchronous_Select_Nesting => 0, and]}

  @ChgRef{Version=[2],Kind=[Added]}
  @ChgAdded{Version=[2],Text=[Max_Tasks => 0.]}
@end{InnerItemize}
@end{Itemize}

If an implementation supports @nt[pragma] Restrictions for a particular
argument, then except for the restrictions No_Unchecked_Deallocation,
No_Unchecked_Conversion, No_Access_Subprograms, and No_Unchecked_Access,
 the associated restriction applies to the
run-time system.
@begin[reason]
Permission is granted for the run-time system to use the specified
otherwise-restricted features, since the use of these features may
simplify the run-time system by allowing more of it to be written
in Ada.
@end[reason]
@begin{Discussion}

The restrictions that are applied to the partition are also applied to the
run-time system. For example, if No_Floating_Point is specified,
then an implementation that uses floating point for implementing the delay
statement (say) would require that No_Floating_Point is
only used in conjunction with No_Delay. It is clearly important that
restrictions are effective so that Max_Tasks=0 does imply that tasking is
not used, even implicitly (for input-output, say).

An implementation of tasking could be produced based upon a run-time
system written in Ada in which the rendezvous was controlled by
protected types. In this case, No_Protected_Types could only be used in
conjunction with Max_Task_Entries=0. Other implementation dependencies
could be envisaged.

If the run-time system is not written in Ada, then the wording needs to be
applied in an appropriate fashion.

@end{Discussion}
@end{ImplReq}

@begin{DocReq}
If a pragma Restrictions(No_Exceptions) is specified, the implementation
shall document the effects of all constructs where language-defined checks are
still performed automatically (for example, an overflow check performed
by the processor).
@ChgImplDef{Version=[2],Kind=[Deleted],Text=[@ChgDeleted{Version=[2],
Text=[Implementation-defined aspects of pragma Restrictions.]}]}
@ChgDocReq{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],Text=[
If a pragma Restrictions(No_Exceptions) is specified, the effects of all
constructs where language-defined checks are still performed.]}]}
@begin{Discussion}

@ChgRef{Version=[2],Kind=[Revised],ARef=[AI95-00114-01]}
The documentation requirements here are quite difficult to satisfy. One
method is to review the object code generated and determine the checks that
are still present, either explicitly, or implicitly within the architecture.
As another example from that of overflow, consider the question of
@Chg{Version=[2],New=[dereferencing],Old=[deferencing]} a null pointer.
This could be undertaken by a memory access trap
when checks are performed. When checks are suppressed via the argument
No_Exceptions, it would not be necessary to have the memory access trap
mechanism enabled.

@end{Discussion}
@end{DocReq}

@begin{Erron}
@PDefn2{Term=(erroneous execution),Sec=(cause)}
Program execution is erroneous if pragma Restrictions(No_Exceptions)
has been specified and the conditions arise under which a generated
language-defined run-time check would fail.
@begin{Discussion}

The situation here is very similar to the application of pragma Suppress.
Since users are removing some of the protection the language
provides, they had better be careful!

@end{Discussion}

@PDefn2{Term=(erroneous execution),Sec=(cause)}
Program execution is erroneous if pragma Restrictions(No_Recursion)
has been specified and a subprogram is invoked as part of its
own execution,
or if pragma Restrictions(No_Reentrancy) has been specified and
during the execution of a subprogram by a task, another task invokes
the same subprogram.
@begin{Discussion}

In practice, many implementations may not exploit the absence of recursion
or need for reentrancy, in which case the program execution would be
unaffected by the use of recursion or reentrancy, even though the program is
still formally erroneous.

@end{Discussion}
@end{Erron}

@ChgNote{I can't find any reason in the normative wording for this item;
therefore I've removed it. The notes below (commented out anyway) refer only
to a non-standard mode, which is irrelevant in the Standard.}
@ChgImplDef{Version=[2],Kind=[Deleted],Text=[@ChgDeleted{Version=[2],
Text=[Any restrictions on pragma Restrictions.]}]}

@begin{Notes}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00394-01]}
@ChgAdded{Version=[2],Text=[Uses of @Syni{restriction_parameter_}@nt{identifier}
No_Dependence defined in @RefSecNum{Language-Defined Restrictions}:
No_Dependence => Ada.@!Unchecked_@!Deallocation and No_Dependence =>
Ada.@!Unchecked_@!Conversion may be appropriate for high-integrity systems.
Other uses of No_Dependence can also be appropriate for high-integrity
systems.]}
@begin{Discussion}
  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[The specific mention of these two uses
  is meant to replace the identifiers now banished to
  @RefSec{Dependence Restriction Identifiers}.]}

  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[Restriction No_Dependence => Ada.Unchecked_Deallocation
  would be useful in those
  contexts in which heap storage is needed on program start-up, but need not be
  increased subsequently. The danger of a dangling pointer can therefore be
  avoided.]}@ChgNote{Moved down from above.}
@end{Discussion}

@end{Notes}

@begin{comment}
@begin{Notes}
The standard mode for pragma Restrictions is that a
compilation unit
(or a partition if at link time) is illegal
if it makes use of a feature identified in the pragma.
However, an implementation is allowed to have a mode of operation
where it issues a warning message versus rejecting the unit or partition,
and where the run-time system supplied for the partition
includes support for the identified feature.

An implementation need not independently support the restrictions
identified above, but may instead require that if a particular
restriction is identified in a @nt(pragma) Restrictions, then
other restrictions (the exact set of which is implementation defined)
need also to be identified.

In such a case, if the additional
restrictions are not specified in a @nt(pragma) Restrictions, and
a unit or partition uses such a feature, the implementation should
@begin{itemize}
issue a warning that the pragma is being ignored (that is, the
full RTS is being used),

identify to the user the additional restrictions that need to be
specified in the pragma in order to obtain the reduced RTS, and
identify any constructs that would use any of the features so
proscribed
@end{itemize}
@end{Notes}
@end{comment}

@begin{Extend95}
  @ChgRef{Version=[2],Kind=[AddedNormal],Ref=[8652/0042],ARef=[AI95-00130-01]}
  @ChgAdded{Version=[2],Text=[@Defn{extensions to Ada 95}
  No_Local_Allocators no longer prohibits generic instantiations.]}
@end{Extend95}

@begin{DiffWord95}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00285-01]}
  @ChgAdded{Version=[2],Text=[Wide_Wide_Text_IO (which is new) is added to the
  No_IO restriction.]}

  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00347-01]}
  @ChgAdded{Version=[2],Text=[The title of this clause was changed to match the
  change to the Annex title. Pragma Profile(Ravenscar) is part of this annex.]}

  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00394-01]}
  @ChgAdded{Version=[2],Text=[Restriction No_Dependence is used instead of
  special @i<restriction_>@nt<identifier>s. The old names are banished to
  Obsolescent Features (see @RefSecNum{Dependence Restriction Identifiers}).]}

  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00394-01]}
  @ChgAdded{Version=[2],Text=[The bizarre wording @lquotes@;apply in this
  Annex@rquotes (which no one quite can explain the meaning of) is banished.]}
@end{DiffWord95}

@LabeledAddedClause{Version=[2],Name=[Pragma Detect_Blocking]}

@begin{Intro}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Text=[The following @nt{pragma} forces an implementation
to detect potentially blocking operations within a protected operation.]}
@end{Intro}

@begin{Syntax}
@begin{SyntaxText}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Type=[Leading],Keepnext=[T],Text=[The form of a
@nt{pragma} Detect_Blocking is as follows:]}
@end{SyntaxText}
@ChgRef{Version=[2],Kind=[AddedNormal]}
@ChgAdded{Version=[2],Text=[@AddedPragmaSyn`Version=[2],@key{pragma} @prag<Detect_Blocking>;']}
@end{Syntax}

@begin{LinkTime}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Text=[@PDefn2{Term=[configuration pragma], Sec=(Detect_Blocking)}
@PDefn2{Term=[pragma, configuration], Sec=(Detect_Blocking)}
A @nt{pragma} Detect_Blocking is a configuration
pragma.]}
@end{LinkTime}

@begin{RunTime}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Text=[An implementation is required to detect a
potentially blocking operation within a protected operation, and to raise
Program_Error (see @RefSecNum{Protected Subprograms and Protected Actions}).]}
@end{RunTime}

@begin{ImplPerm}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Text=[An implementation is allowed to reject a
@nt{compilation_unit} if a potentially blocking operation is present directly
within an @nt{entry_body} or the body of a protected subprogram.]}
@end{ImplPerm}

@begin{Notes}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
@ChgAdded{Version=[2],Text=[An operation that causes a task to be blocked
within a foreign language domain is not defined to be potentially blocking,
and need not be detected.]}
@end{Notes}

@begin{Extend95}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00305-01]}
  @ChgAdded{Version=[2],Text=[@Defn{extensions to Ada 95}
  Pragma Detect_Blocking is new.]}
@end{Extend95}

@RMNewPage@Comment{For printed version of Ada 2007 RM}
@LabeledAddedClause{Version=[2],Name=[Pragma Partition_Elaboration_Policy]}

@begin{Intro}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[This clause defines a @nt{pragma}
for user control over elaboration policy.]}
@end{Intro}

@begin{Syntax}
@begin{SyntaxText}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Type=[Leading],Keepnext=[T],Text=[The form of a
@nt{pragma} Partition_Elaboration_Policy is as follows:]}
@end{SyntaxText}
@ChgRef{Version=[2],Kind=[AddedNormal]}
@ChgAdded{Version=[2],Text=[@AddedPragmaSyn`Version=[2],@key{pragma} @prag<Partition_Elaboration_Policy> (@SynI<policy_>@Syn2<identifier>);']}

@begin{SyntaxText}
@ChgRef{Version=[2],Kind=[AddedNormal]}
@ChgAdded{Version=[2],Text=[The @SynI<policy_>@nt{identifier} shall be either
Sequential, Concurrent or an implementation-defined identifier.]}
@ChgImplDef{Version=[2],Kind=[AddedNormal],Text=[@Chg{Version=[2],New=[Implementation-defined
@SynI<policy_>@nt<identifier>s allowed in a @nt{pragma} Partition_Elaboration_Policy.],Old=[]}]}
@end{SyntaxText}
@end{Syntax}

@begin{LinkTime}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[@PDefn2{Term=[configuration pragma], Sec=(Partition_Elaboration_Policy)}
@PDefn2{Term=[pragma, configuration], Sec=(Partition_Elaboration_Policy)}
A @nt{pragma} Partition_Elaboration_Policy is a configuration pragma.
It specifies the elaboration policy for a partition.
At most one elaboration policy shall be specified for a partition.]}

@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[If the Sequential policy is
specified for a partition then pragma Restrictions (No_Task_Hierarchy) shall
also be specified for the partition.]}
@end{LinkTime}

@begin{RunTime}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[Notwithstanding what this International Standard
says elsewhere, this @nt{pragma} allows partition elaboration rules concerning
task activation and interrupt attachment to be changed. If the
@SynI{policy_}@nt{identifier} is Concurrent, or if there is no pragma
Partition_Elaboration_Policy defined for the partition, then the rules defined
elsewhere in this Standard apply.]}

@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01],ARef=[AI95-00421-01]}
@ChgAdded{Version=[2],Type=[Leading],Text=[If the partition elaboration policy
is Sequential, then task activation and interrupt attachment are performed in
the following sequence of steps:]}

@begin{Itemize}
  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[The activation of all library-level tasks and the
  attachment of interrupt handlers are deferred until all library units are
  elaborated.]}

  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[The interrupt handlers are attached by the
  environment task.]}

  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[The environment task is suspended while the
  library-level tasks are activated.]}

  @ChgRef{Version=[2],Kind=[AddedNormal]}
  @ChgAdded{Version=[2],Text=[The environment task executes the main subprogram
  (if any) concurrently with these executing tasks.]}
@end{Itemize}

@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01],ARef=[AI95-00421-01]}
@ChgAdded{Version=[2],Text=[If several dynamic interrupt handler attachments for
the same interrupt are deferred, then the most recent call of
Attach_Handler or Exchange_Handler determines which handler is attached.]}

@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01],ARef=[AI95-00421-01]}
@ChgAdded{Version=[2],Text=[If any deferred task activation fails, Tasking_Error
is raised at the beginning of the sequence of statements of the
body of the environment task prior to calling the
main subprogram.]}

@end{RunTime}

@begin{ImplAdvice}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[If the partition elaboration policy is Sequential
and the Environment task becomes permanently blocked during elaboration then
the partition is deadlocked and it is recommended that the partition be
immediately terminated.]}
@ChgImplAdvice{Version=[2],Kind=[AddedNormal],Text=[@ChgAdded{Version=[2],
Text=[If the partition elaboration policy is Sequential
and the Environment task becomes permanently blocked during elaboration then
the partition should be immediately terminated.]}]}

@end{ImplAdvice}

@begin{ImplPerm}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01]}
@ChgAdded{Version=[2],Text=[If the partition elaboration policy is Sequential
and any task activation fails then an implementation may immediately terminate
the active partition to mitigate the hazard posed by continuing to execute with
a subset of the tasks being active.]}
@end{ImplPerm}

@begin{Notes}
@ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00421-01]}
@ChgAdded{Version=[2],Text=[If any deferred task activation fails, the
environment task is unable to handle the Tasking_Error exception and completes
immediately. By contrast, if the partition elaboration policy is Concurrent,
then this exception could be handled within a library unit.]}
@end{Notes}


@begin{Extend95}
  @ChgRef{Version=[2],Kind=[AddedNormal],ARef=[AI95-00265-01],ARef=[AI95-00421-01]}
  @ChgAdded{Version=[2],Text=[@Defn{extensions to Ada 95}
  @nt{Pragma} Partition_Elaboration_Policy is new.]}
@end{Extend95}