| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The GNAT Pro High-Integrity Edition contains a number of features especially useful for safety-critical programming:
-gnatD or -gnatG
options, the compiler generates a low-level version of the source program
in an Ada-like format.
This serves as an intermediate form between the original source program and the generated object code. This intermediate representation may be used to understand the assembly code and verify some of the origins of non-traceable code. This expanded low-level generated code can also be used as the reference point for run-time debugging.
-gnatR option, the
compiler generates information about the
choice of data representations.
pragma Restrictions prohibit
constructs that would generate implicit loops
(No_Implicit_Loops) or implicit conditionals
(No_Implicit_Conditionals).
If these restrictions are specified, then either alternative code is
generated without the implicit code, or the construct in question is
rejected, forcing the programmer to make the loop or conditional
explicit in the source. This is desirable in ensuring full testing of
conditionals. See 2.6 Controlling Implicit Conditionals and Loops.
pragma Restrictions can be used
to restrict the form of explicit conditionals. Using the
restriction identifier No_Direct_Boolean_Operators
prohibits the use of and and or operators,
forcing instead the use of and then and or else.
This can be useful in some certification
procedures in order to reduce the number of test cases needed to
fully exercise compound conditions.
-gnatyx options, the compiler performs various
style checks that can be used to enforce rigorous coding standards,
easing the verification process by ensuring that the source is
formatted in a uniform manner.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The predefined profiles implement two different levels of support for
exception handling. The ZFP and Ravenscar SFP (Small Footprint) profiles
implement the scenario where
pragma Restrictions (No_Exception_Propagation) is
implicitly applied to an application (see below). The Cert and Ravenscar Cert
profiles implement full Ada 83 exception handling, plus limited use of Ada 95 /
Ada 2005 exception occurrences. Both implementations provide a last chance
handler capability to deal with unhandled exceptions. Details are described
in the sections on exceptions in the chapters specific to the individual
profiles.
The restriction No_Exception_Propagation, which is the default
mode for the ZFP and Ravenscar SFP profiles, allows exceptions to be raised
and handled only if the handler is in the same subprogram (more generally
in the same scope not counting packages and blocks). This limits the
handling of exceptions to cases where raising the exception corresponds
to a simple goto to the exception handler. This is especially useful
for predefined exceptions. For example, the following is allowed in the
ZFP or Ravenscar SFP profiles:
begin
X := Y + Z;
exception
when Constraint_Error =>
... result of addition outside range of X
end;
|
With this restriction in place, handlers are allowed, but can only be entered if the raise is local to the scope with the handler. The handler may not have a choice parameter, use of GNAT.Current_Exception is not permitted, and use of reraise statements (raise with no operand) is not permitted.
Warnings are given if an implicit or explicit exception raise is not covered by a local handler, or if an exception handler does not cover a case of a local raise. The following example shows these warnings in action:
1. pragma Restrictions (No_Exception_Propagation);
2. procedure p (C : in out Natural) is
3. begin
4. begin
5. C := C - 1;
6. exception
7. when Constraint_Error =>
8. null;
9. when Tasking_Error =>
|
>>> warning: pragma Restrictions
(No_Exception_Propagation) in effect, this
handler can never be entered, and has been
removed
10. null;
11. end;
12.
13. begin
14. C := C - 1;
|
>>> warning: pragma Restrictions
(No_Exception_Propagation) in effect,
"Constraint_Error" may call
Last_Chance_Handler
15. end;
16.
17. begin
18. raise Program_Error;
|
>>> warning: pragma Restrictions
(No_Exception_Propagation) in effect,
Last_Chance_Handler will be called
on exception
19. end;
20. end p;
|
These warnings may be turned off globally using the switch -gnatw.X, or by using pragma Warnings (Off) locally.
As shown by the warnings above, if any other exception is raised, it is treated as unhandled, and causes the last chance handler to be entered.
In a High-Integrity program, you can forbid exception handling entirely, but still allow the raising of exceptions by using:
pragma Restrictions (No_Exception_Handlers); |
No handlers are permitted in a program if this restriction is specified,
so exceptions can never be handled in the usual Ada way. If run time
checking is enabled, then
it is possible for the predefined exceptions Constraint_Error,
Program_Error, or Storage_Error to be raised at run time.
When such an exception is raised, a call is made to the routine designated
by the symbol __gnat_last_chance_handler. This routine has distinct
parameters for the ZFP and Ravenscar SFP profiles vs. the Cert and Ravenscar
Cert profiles, as detailed in the profile-specific sections.
If your program may raise Constraint_Error,
Program_Error, or Storage_Error, then the application must
include an appropriate "last chance handler" to deal with the fatal errors
represented by these exception occurrences. This handler can be written in C
or in Ada using the profile-specific parameters. All last chance handler
implementations must terminate or suspend the thread that executes the handler.
Exception declarations and raise statements are still permitted under
this restriction.
A raise statement is compiled into a call of
__gnat_last_chance_handler.
To suppress all run-time error checking and generation of implicit
calls to the last chance handler, and to disallow all raise
statements, you may use:
pragma Restrictions (No_Exceptions); |
The following switch is not relevant if the program has
pragma Restrictions (No_Exception_Handlers) or
pragma Restrictions (No_Exception_Propagation):
The following switches are not relevant if the program has
pragma Restrictions (No_Exceptions) or
pragma Restrictions (No_Exception_Propagation):
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Allocators and unchecked deallocation are permitted in a High-Integrity Profile program. Use of these features will generate calls on one of the following C convention functions:
void *__gnat_malloc (size_t size); void __gnat_free (void *ptr); |
The corresponding Ada subprogram declarations are:
type Pointer is access Character;
-- This is really a void pointer type, the result from
-- Gnat_Malloc will always be maximally aligned.
function Gnat_Malloc (size : Interfaces.C.size_t)
return Pointer;
pragma Export (C, Gnat_Malloc, "__gnat_malloc");
procedure Gnat_Free (Ptr : Pointer);
pragma Export (C, Gnat_Free, "__gnat_free");
|
These functions are part of the run-time library for some High Integrity Profiles, and must be provided by the user otherwise. If included in the run-time library, they appear in the file `s-memory.adb'. To know if a given profile provides this feature, see the relevant section in 3. The Predefined Profiles.
If these functions are not provided, then the user must define
__gnat_malloc either in C or in Ada, using the above
declarations; otherwise the program will fail to bind. Analogously, if
the program uses Unchecked_Deallocation, then
__gnat_free must be defined.
For example, on VxWorks DO-178B,
one approach (if no deallocation is to be allowed) is for the user
to implement Gnat_Malloc through
calls on memLib routines.
The memNoMoreAllocations function can be
invoked to prevent further allocations, for example at the end of package
elaboration.
To prohibit the use of allocators or unchecked deallocation, you can use
pragma Restrictions with the following restriction identifiers
(these are defined in the Ada Reference Manual):
pragma Restrictions (No_Local_Allocators);
pragma Restrictions (No_Allocators);
pragma Restrictions (No_Implicit_Heap_Allocations);
pragma Restrictions (No_Unchecked_Deallocation);
Ada.Unchecked_Deallocation.
If any or all of these pragmas appear in the `gnat.adc' file,
the corresponding construct(s) will be forbidden throughout the
application. If all four of the above restrictions are in place, then
no calls to either __gnat_malloc or __gnat_free will be
generated.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The use of assignments of arrays and records is permitted in a
High-Integrity Profile program. However, on some targets such
constructs may generate calls on the C library functions memcpy,
memmove or bcopy.
There are two ways to deal with this issue.
First, such assignments can be avoided at the source code level. You can replace an array assignment by an explicit loop, and a record assignment by a series of assignments to individual components. You can encapsulate such statements in a procedure if many such assignments occur.
Second, you can reuse or define an appropriate memcpy
(and/or memove and/or bcopy) routine.
For example, if certification protocols permit, you can use the memcpy,
memmove or bcopy routine(s) from the C library.
Otherwise, the following Ada procedure will supply
the needed memcpy functionality:
with System; use System;
with Interfaces.C; use Interfaces.C;
function memcpy (dest, src : Address;
n : size_t) return Address;
pragma Export (C, memcpy, "memcpy");
with Ada.Unchecked_Conversion;
function memcpy (dest, src : Address;
n : size_t) return Address is
subtype mem is char_array (size_t);
type memptr is access mem;
function to_memptr is
new Ada.Unchecked_Conversion (address, memptr);
dest_p : constant memptr := to_memptr (dest);
src_p : constant memptr := to_memptr (src);
begin
if n > 0 then -- need to guard against n=0 since size_t is a modular type
for J in 0 .. n - 1 loop
dest_p (J) := src_p (J);
end loop;
end if;
return dest;
end memcpy;
|
The above memcpy routine provides the minimal required functionality.
A more elaborate version that deals with alignments and moves by words
rather than bytes where possible would improve performance. On some
targets there may be hardware instructions (e.g. rep movsb on
the x86 architecture) that can be used to provide the needed
functionality.
Note that memcpy is not required to handle the overlap case, and the
GNAT Pro compiler ensures that any call to memcpy meets the requirement
that the operands do not overlap.
On the other hand, memmove and bcopy are required to handle
overlaps. Note that the order of the arguments of bcopy differs from
memcpy and memmove. A user-supplied version of bcopy
should take into account these differences.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Objects of tagged and class-wide types may be declared. Dispatching and class-wide subprograms are allowed.
Restrictions are:
Ada.Tags.Internal_Tag and Ada.Tags.Tag_Error are not
available in the default implementations of these profiles.
Ada 2005 object-operation notation is fully supported under ZFP profile. Ada 2005 generic dispatching constructors are not supported under ZFP profile, and a subset of Ada 2005 interface types is supported under ZFP profile. Restrictions on interfaces are:
In order for the debugger to be able to print the complete type description of a tagged type, the program must have Ada.Tags as part of its closure. Otherwise, the debugger will not be able to print the name of the type from which the tagged type has been derived. This limitation can easily be addressed by introducing an artificial dependency on the Ada.Tags unit. Another option is to compile one unit that declares a tagged type with -fno-eliminate-unused-debug-types. This does not affect the ability to print the value of tagged objects, which should work without problem regardless.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
By default, the High-Integrity Profiles allow functions returning unconstrained
objects such as unconstrained arrays or discriminated records without
default initializations for discriminants.
To implement this capability, the compiler generates references to a
secondary stack mechanism that requires run-time support.
If you need to
use this capability, you should refer to the relevant section in
3. The Predefined Profiles, to see if it is already provided in the
run-time library or if you are responsible for providing an appropriate
implementation of this unit for a given profile. The specification of the
secondary stack mechanism is described in the Ada package
System.Secondary_Stack,
which is in the file `s-secsta.ads'.
If you wish to disable this capability, you can use the
pragma Restrictions (No_Secondary_Stack);
that will generate an error
at compile time for each call to a function returning an unconstrained object.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Certain complex constructs in Ada result in generated code that
contains implicit conditionals, or implicit for loops.
("Implicit" means that the conditionals/loops are not present in the
Ada source code.)
For example,
slice assignments result in both kinds of generated code.
In some certification protocols, conditionals and loops require special treatment. For example, in the case of a conditional, it may be necessary to ensure that the test suite contains cases that branch in both directions for a given conditional. A question arises as to whether implicit conditionals and loops generated by the compiler are subject to the same verification requirements.
To address this issue, the GNAT Pro High-Integrity Edition defines two restriction identifiers that control whether the compiler is permitted to generate implicit conditionals and loops :
pragma Restrictions (No_Implicit_Conditionals); pragma Restrictions (No_Implicit_Loops); |
These are partition-wide restrictions that ensure that the generated code respectively contains no conditionals and no loops. This is achieved in one of two ways. Either the compiler generates alternative code to avoid the implicit construct (possibly with some loss of efficiency) or, if it cannot find an equivalent code sequence, it rejects the program and flags the offending construct. In the latter situation, the programmer will need to revise the source program to avoid the implicit conditional or loop.
As an example, consider the slice assignment:
Data (J .. K) := Data (R .. S); |
Ada language semantics requires that a slice assignment of this type be
performed nondestructively, as though the right hand side were computed
first into a temporary, with the value then assigned to the left hand side.
In practice it is more efficient to use a single loop, but the direction of
the loop needs to depend on the values of J and R. If
J is less than R them the move can take place left to right,
otherwise it needs to be done right to left. The normal code generated by
GNAT Pro reflects this requirement:
if J < R then
for L in J .. K loop
Data (L) := Data (L - J + R);
end loop;
else
for L in reverse J .. K loop
Data (L) := Data (L - J + R);
end loop;
end if;
|
This code clearly contains both implicit conditionals and implicit loops.
If the restriction No_Implicit_Conditionals is active, then the
effect is to generate code that uses a temporary:
for L in R .. S loop
Temp (L - R) := Data (L);
end loop;
for L in J .. K loop
Data (L) := Temp (L - J);
end loop;
|
This code avoids an implicit conditional at the expense of doing twice
as many moves. If the restriction No_Implicit_Loops is also
specified, then the slice assignment above would not be permitted,
and would be rejected as illegal. This means that the programmer would
need to modify the source program
to have an explicit loop (in the appropriate
direction). This loop could then be treated in whatever manner is
required by the certification protocols in use.
The following constructs are not permitted in the presence of
No_Implicit_Conditionals (note that some are in any event
excluded from the High-Integrity Profiles):
Width attribute applied to real type
rem, mod, and division operators if checks are on
Is_Negative intrinsic function
The following constructs are not permitted in the presence
of No_Implicit_Loops (note that entry families are in any event
excluded from some or all High-Integrity Profiles):
others clause
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Some testing procedures for certification can be more efficient if application
programs avoid the explicit use of and/or
and instead use and then/or else.
This can facilitate meeting the requirement for MCDC
("Modified Condition / Decision Coverage") testing. The net effect of
using the short-circuit versions is a significant reduction in the number
of test cases needed to demonstrate code and condition coverage.
The GNAT Pro High-Integrity Edition provides an additional restriction identifier that addresses this issue by controlling the presence of direct boolean conditional operators:
pragma Restrictions (No_Direct_Boolean_Operators); |
These are partition-wide restrictions that ensure that the source code
does not contain any instances of the direct boolean operators
and or or. This will alert the programmer to the requirement
to use and then or or else as appropriate
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Ada allows constructs (e.g., variables with implicit initializations) for which so-called elaboration code must be generated. In a certification context the need to certify elaboration code will increase costs, as it will be necessary to address questions such as why the compiler implicitly generated the elaboration code, which Ada requirement it met, which test cases are needed.
The GNAT Pro High-Integrity Edition provides the
pragma Restrictions (No_Elaboration_Code),
which alerts you to constructs for which elaboration code would be generated
by the compiler.
When this pragma is specified
for a compilation unit, the compiler outputs an error message
whenever it needs to generate elaboration code. You must then
revise the program so that no elaboration code is generated.
As an example consider the following:
package List is
type Elmt;
type Temperature is range 0.0 ... 1_000.0;
type Elmt_Ptr is access all Elmt;
type Elmt is record
T : Temperature;
Next : Elmt_Ptr;
end record;
end List;
pragma Restrictions (No_Elaboration_Code);
with List;
procedure Client is
The_List : List.Elmt;
begin
null;
end Client;
|
When compiling unit Client, the compiler will generate the error
message:
client.adb:4:04: violation of restriction "No_Elaboration_Code" at line 1 |
In this example GNAT Pro needs to generate elaboration code for object
The_List because Ada requires access values to be null initialized
(unless they have explicit initializations).
To see the elaboration code that would be generated you can remove the
No_Elaboration_Code restriction and use the `-gnatG' switch
to view the low-level version of the Ada code generated by GNAT Pro.
In this case we obtain:
package list is
type list__elmt;
type list__temperature is new float range 0.0E0 .. (16384000.0*2**(-14));
type list__elmt_ptr is access all list__elmt;
type list__elmt is record
t : list__temperature;
next : list__elmt_ptr;
end record;
freeze list__elmt [
procedure list__elmtIP (_init : in out list__elmt) is
begin
_init.next := null;
return;
end list__elmtIP;
]
end list;
with list; use list;
procedure client is
the_list : list.list__elmt;
list__elmtIP (the_list);
begin
null;
return;
end client;
|
Elaboration code is generated inside procedure Client
to null-initialize the access value inside The_List object,
by calling the initialization procedure for the type, namely elmtIP.
To avoid generating elaboration code, you can add explicit initialization as follows:
pragma Restrictions (No_Elaboration_Code); with List; use List; procedure Client is The_List : List.Elmt := (0.0, null); begin null; end Client; |
Since the initialization is now explicit, it becomes part of the requirements mapping and application design. In a certification context it is preferable to certify code that you write explicitly rather than code that gets generated implicitly.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Deactivated code in the executable requires specific treatment with standards such ED12/DO-178b (see 6.4.4.3d). This treatment can be simplified by diminishing the footprint of deactivated code in the final executable. This section summarizes the various features that can be used to minimize the footprint of deactivated code in the final executable program.
type Configs is (config1, config2, config3); ... C : constant Configs := config2; |
the following code
if C = config1 then
some_code0;
end if;
case C is
when config1 => some_code1;
when config2 => some_code2;
when config3 => some_code3;
end case;
|
is transformed into:
some_code2; |
The elimination done by the compiler can be traced thanks to a compiler
optional warning enabled with -gnatwt.
The user can prevent code generation for subprograms that are known to be deactivated by placing pragmas eliminate in the configuration pragmas file:
pragma Eliminate (Unit, Unused_Subp, Source_Location => "unit.adb:19") |
gnatelim can produce
automatically the list of pragmas Eliminate that can be used for the
construction of a given executable.
Some configurations support linker level removal of unused subprograms and
data. The source code needs to be compiled with the options
-ffunction-sections and -fdata-sections and the linking
must be performed with option -Wl,--gc-sections. Traceability of
the code removal is provided through a chapter called "Discarded
Input sections" in the map file
that can be produced by the linker with option -Wl,-M.
These methods can be used to reduce the amount of code in the final executable corresponding to deactivated source code. The last three offer means of tracing the removed code and thus can be used for traceability purposes or as documentation of the deactivation mechanism. The last method can also remove code added by the compiler such as the implicit initialization procedures associated with composite types when they are not used. It therefore simplifies the reverse traceability from object to source.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
During the build process, the GNAT Pro toolchain manipulates several program representations, in particular:
In order to help the traceability process, GNAT Pro gives access to the intermediate format, through the following flags:
-gnatD
or -gnatG.
-Wa,-adhl=file.lst which
save it in the file file.lst.
$ <target>-gcc -c -gnatDL -Wa,-adhl -fverbose-asm -mregnames prg.adb |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The `-On' compiler switch sets the optimization level to n, where n is an integer between 0 and 3. If n is omitted, it is set to 1.
Generally you should use the `-O' switch to enable optimization, because this is the level at which you can most easily track the correspondence between source code and object code. Although for safety-critical programs optimizations are often regarded with suspicion, the fundamental reason for this concern is traceability. At the `-O0' level, traceability is in fact more difficult due to the large amount of naive code that is generated. The optimizations performed at level `-O1' eliminate redundant code, but avoid the kind of code-shuffling transformations that can obscure the correspondence between source and object code.
If you consider coverage, it can be useful to disable optimizations on
conditional statements. The option
`-fno-short-circuit-optimize' specifically disables boolean
operator optimizations (those which transform or else into
or or and then into and), and the options
`-fno-if-conversion' and `-fno-if-conversion2' disable
optimization passes that try to remove conditional jumps for if statements and
use conditional move instead. These switches help to preserve the original
jump structure implied by the source, thus helping source-to-object
traceability, and facilitating certification and coverage analysis at
the object level.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The `-gnaty' compiler switches direct the compiler to enforce style consistency checks, which can be useful in ensuring a uniform lexical appearance (and easing program readability) across a project.
Annex H in the Ada Reference Manual defines a set of restrictions
identifiers, many of which are relevant for code that needs to be certified.
If you provide a pragma Restrictions with any of these identifiers,
the compiler will prohibit your program from using the corresponding construct.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
For the most part, you use the GNAT Pro tools in the High-Integrity edition in the same way, and with the same set of switches, as in a full Ada environment. However, certain switches are not relevant for the High-Integrity Profiles. This section lists this set of switches; a complete description of the compiler switches appears in the GNAT Pro User's Guide and, in the case of general gcc switches, the Using GNU GCC manual.
2.13.1 Compiler Switches 2.13.2 gnatbindSwitches
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The following switches are not relevant in certain High-Integrity profiles, since they are associated with features that are outside these profiles:
Assert, but is subject to exception
propagation and handling restrictions in ZFP and Ravenscar SFP.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
gnatbind Switches The following switches are not relevant in Zero Footprint, Cert or Ravenscar modes:
In addition, the `-t' switch overrides standard Ada unit consistency checks and would generally not be used for high-integrity applications.
The `-f' switch for elaboration order control should not be used; see the discussion of elaboration order issues in GNAT Pro User's Guide.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |