4. The Predefined Profiles¶
This chapter describes what is prohibited and what is permitted in the different predefined profiles.
4.1. Choosing a Predefined Profile¶
You choose a particular profile through either of two approaches:
Runtimeattribute in a project file (the recommended technique); or
Set the GNAT configuration mode, via the
Both approaches specify the run-time library.
You need to specify the run-time library to the compiler, to gnatbind, to gnatlink, to gnatmake, and in general to any tool that needs to be aware of the run-time configuration.
Here is an example showing how to specify the run-time library in a project file (note the necessary inclusion of the language name as index):
project Demo is ... for Runtime ("Ada") use "ravenscar-cert"; ... end Demo;
For platforms with an underlying operating system (e.g., VxWorks), the
values for the attribute/switch are
ravenscar-cert-rtp, corresponding to the establishment of Zero
Footprint, Cert, Ravenscar Cert Kernel, and Ravenscar Cert RTP
Depending on the targeted environment, there may be other supported full Ada alternatives. These are not described here; see the GNAT User’s Guide Supplement for Cross Platforms. The switch settings are not case sensitive.
The set of available profiles depends on the target.
Bareboard and PikeOS Configurations
The Zero Footprint, Ravenscar SFP and Ravenscar Full profiles are supported. Conceptually, the run-times could be ordered in terms of size, capabilities, and complexity like so: ZFP (Zero Footprint) < Ravenscar SFP < Ravenscar Full.
There are various criteria for choosing (and they may be contradictory):
If you don’t plan to use tasking, your best choice may be ZFP, but note that the Ravenscar-based run-time libraries provide more than tasking. In particular, many language-defined packages are included that are not included in the ZFP run-time.
If you plan to certify your software, choose either ZFP or Ravenscar SFP. These two run-time libraries are specifically intended for that purpose.
If you need tasking, the choice is between Ravenscar SFP or Ravenscar Full (ZFP doesn’t support tasks). Note also that “tasking” includes protected objects, the language-defined mechanism for interrupt handling.
If you need exception handlers, choose Ravenscar Full (ZFP and Ravenscar SFP don’t support exception propagation).
The Ravenscar Full run-time library provides many features over Ravenscar SFP but it is possible to import some features from Ravenscar Full into Ravenscar SFP. The math library is a prime example.
The Ravenscar Full run-time library provides two tasking profiles: Ravenscar and Jorvik. See The Ravenscar Profiles, for details.
The Zero Footprint and Ravenscar SFP run-time libraries only provide a simple implementation of memory allocation (Gnat_Malloc).
The allocation mechanism relies on the
__heap_endsymbols to delimit the memory area that can be allocated. Those symbols are defined by the linker script used for the specific board being targeted.
Memory deallocation is a no-op, the rationale being that with certifiable software, dynamic memory allocation is performed at most once, at startup, so freeing the memory is unnecessary. This restriction allows a simple, efficient, and predictable behavior for memory allocation.
VxWorks Cert 6.x
Zero Footprint, Ravenscar Cert and Full Profiles are supported. The Cert profile is also supported when VxWorks Cert is used as a Guest Operating System under VxWorks 653 3.x.
Zero Footprint, Cert, Ravenscar Cert and Full Profiles are supported.
Zero Footprint, Ravenscar SFP and Ravenscar Full are supported.
A native version of the Zero Footprint run-time library is provided for all high-integrity development hosts to facilitate native platform testing. It is selected as described above, using either the
Runtimeattribute or the
4.2. The Zero Footprint Profile¶
With the Zero Footprint Profile the generated object modules usually contain no references to a GNAT run-time library. There are a few references related to floating point attributes or for support of software emulated floating point operations. The absence of references to the run-time allows the construction of a standalone program that has no code other than that corresponding to the original source code, together with the elaboration routine generated by the binder. The elaboration routine generated by the binder also avoids any reference to run-time routines or data.
4.2.1. The -nostdlib Switch¶
In a certification context, it may be important to guarantee the enforcement of a strict Zero Footprint Profile where one can ensure that no external library is linked with the final image. This can be achieved by using the builder switch -nostdlib. The GNAT builders (gnatmake, gprbuild) will pass this switch to the binder and to the linker, with the effect of removing the libraries such as libgnat.a and libgcc.a from the link path.
In order to use the -nostdlib switch, the program must meet a number of restrictions in addition to those listed in Ada Restrictions in the Zero Footprint Profile:
No references to entities from run-time packages, e.g.,
No use of pragma
No use of the following floating-point attributes: -
Unbiased_Rounding(with nonstatic arguments), and -
Unaligned_Valid(with any argument);
No use of a secondary stack (this can be enforced by including pragma
No use of floating-point or other arithmetic operations that are too complex for inline expansion and that therefore require calls to a support library.
4.2.2. Ada Restrictions in the Zero Footprint Profile¶
The following features are excluded from the Zero Footprint Profile:
All constructs defined in Section 9 (Tasks) and C.3 (Interrupt Support) of the Ada Reference Manual.
Exception propagation. See Exceptions; note that
raisestatements and local exception handling are permitted.
Packed arrays with a component size other than 1, 2, 4, 8 or 16 bits; if a packed array has static bounds and the overall size of the array is 64-bits or less, all component sizes are allowed. Note that the restriction applies to accessing or setting elements of such an array (it is permissible to declare a packed array with any component size).
The exponentiation operator, unless one of the following conditions is met:
The exponentiation expression is a static expression as defined in the Ada Reference Manual, section 4.9
The right operand is a static expression as defined in the Ada Reference Manual, section 4.9, and is an integral value in the range
0 .. 4
On 32-bit platforms: 64-bit integer and fixed-point types.
On 64-bit platforms: 128-bit integer and fixed-point types.
Boolean operations on packed arrays (individual elements may be accessed)
Imagefor types other than modular integers, signed integers, and
Unrestricted_Accesswhen applied to a non-library-level subprogram
Tagged types declared at other than library-level
Annex E features (Distributed Systems)
Note that explicit
withs of library units are still permitted but
the programmer needs to ensure that the GNAT library modules that
come with the compiler that is being used in Zero Footprint mode satisfy the
requirements of the target hardware.
In particular, in an environment where the code will be certified, the user is responsible for ensuring that the referenced library unit meets the certification conditions.
4.2.3. Predefined Packages in the Zero Footprint Profile¶
In general, the predefined Ada environment (Annex A),
the interfacing packages (Annex B), and the units in the Specialized Needs
Annexes may be implemented with the full Ada language and thus will not be
appropriate in applications that need to adhere to the Zero Footprint Profile.
The only predefined Ada units that are permitted (i.e., that may be
withed) in a Zero Footprint Profile program are as follows:
Interfaces, except that references to the types
Interfaces.C.Extensions, except that references to
Additionally, the following GNAT packages are permitted since all their subprograms are either intrinsic or are expanded inline:
GNAT.IO, which provides basic input / output capabilities
A sample implementation of the secondary stack is provided that can be
used and tailored (in the file
s-secsta.adb). However, as a sample,
no certification material is provided for this implementation. Therefore,
the user is responsible for certifying this, or any other, implementation.
See Functions Returning Unconstrained Objects, for further details.
s-memory.adb is not provided. If you want to use allocators
and unchecked deallocation, you will have to define __gnat_malloc
and __gnat_free. See Allocators,
for further details.
4.2.4. Thread Registration Issues¶
The Zero Footprint profile does not provide run-time facilities that require per-thread data. Therefore, thread registration is not relevant to this profile.
4.2.5. Pragmas Automatically Enabled in the Zero Footprint Profile¶
The following pragmas are automatically enabled when the Zero Footprint Profile is in effect:
pragma Restrictions (No_Exception_Propagation)
pragma Restrictions (No_Exception_Registration)
pragma Restrictions (No_Implicit_Dynamic_Code)
pragma Restrictions (No_Finalization)
pragma Restrictions (No_Tasking)
4.2.6. Exceptions and the Last Chance Handler - ZFP and Ravenscar SFP¶
In the ZFP profile, all applications are treated as though
Restrictions (No_Exception_Propagation) has been applied. As a result,
it is possible to raise predefined and user-defined Ada exceptions but
they must be handled locally, within the same units that raise them.
When an exception is raised and not handled locally, a function with the following C-convention prototype is called (note that the function name begins with two underscore characters):
void __gnat_last_chance_handler (char *source_location, int line);
The corresponding Ada subprogram declaration is:
procedure Last_Chance_Handler (Source_Location : System.Address; Line : Integer); pragma Export (C, Last_Chance_Handler, "__gnat_last_chance_handler");
Source_Location parameter is a C null-terminated string representing
the source location of the
raise statement, as generated by the
compiler, or a zero-length string if
Line parameter, when nonzero, represents the line number in the
Line is zero, the line number information is provided
See the Exceptions for the details of providing an application-specific last chance handler.
4.3. The Cert Profile¶
The Cert profile is a superset of the Zero Footprint Profile, and thus
Predefined Packages in the Zero Footprint Profile, is
relevant. This section describes the additional capabilities
provided by the Cert profile. The Cert profile also provides
The Cert profile is based on an implicitly threaded run-time library. The current implementation of this profile is for use on Wind River Systems VxWorks 653 2.x vThreads partition OS and the VxWorks 653 3.x VxWorks 6 Cert Guest OS with APEX processes. Although there are no Ada tasks, there are different threads (VxWorks 653 vThreads or VxWorks 6 tasks) executing the code and accessing data structures. For example, the following data items must be per-thread:
thread-accessible pointer to jump buffer,
thread-accessible pointer to secondary stack location.
By “thread-accessible”, we mean that a thread-specific data item is needed to implement the behavior defined by the subset.
4.3.1. Exceptions and the Last Chance Handler - Cert and Ravenscar Cert Profiles¶
In these profiles the full semantics of Ada 83 exceptions is supported; limited support for Ada 95 / Ada 2005 / Ada 2012 exception occurrences is included. The run-time library supports propagation of exceptions and handlers for multiple threads, provided that the threads have been registered with the Ada run-time library: see Thread Registration, for details.
The run-time libraries provided by these profiles (both available in
GNAT Pro for VxWorks 653, and
Ravenscar Cert in GNAT Pro for VxWorks Cert 6.x)
support limited Ada 95 / Ada 2005 exception occurrences,
and a non-symbolic stack trace capability
The declaration of the default last chance handler in these profiles is:
procedure Ada.Exceptions.Last_Chance_Handler (Except : Exception_Occurrence); pragma Export (C, Last_Chance_Handler, "__gnat_last_chance_handler"); pragma No_Return (Last_Chance_Handler);
The formal parameter
Except is an Ada 95 / Ada 2005 / Ada 2012
exception occurrence that can be used to identify the exception and the
circumstances under which it occurred. (The formal parameter profile is
different from the last chance handler’s profile in the ZFP run-time
A default body is provided in the
rts-cert/adainclude directory of the restricted run-time library
a-elchha.adb. Its object module
rts-cert/adalib/libgnat.a along with a partially
linked object module
libgnat.o containing the remainder of the
Cert profile run-time library. This example handler generates a
non-symbolic traceback that can be used on the development host to
obtain a symbolic traceback via the vxaddr2line utility. It also
propagates an event to the VxWorks 653 health monitor on VxWorks 653.
The last chance handler for the Cert profile on VxWorks 653 is expected to suspend the vThread or VxWorks task that calls it.
As with the ZFP case, the developer may provide an application-specific replacement for the last chance handler. If you do not supply a last chance handler the default version will be linked into your application.
See the Exceptions for the details of providing an application-specific last chance handler.
4.3.2. Secondary Stack¶
The secondary stack supports functions returning objects of unconstrained types (e.g., unconstrained array types) and of variant record types. The default secondary stack size (for the environment task) can be set using the gnatbind ‘-D’ switch, that specifies the value in Kbytes. For APEX processes, the value defaults to 1/4 the requested primary stack size, and is added to the requested allocation from APEX. The size can also be specified in the Apex_Processes.Create_Process routine.
4.3.3. Thread Registration¶
The thread registration mechanism allows applications to use system threads with Ada code. Specifically, the mechanism supports the Ada exception semantics outside of an Ada tasking context, so that Ada code that uses exceptions can be called by a non-Ada thread. The mechanism is also necessary to support unconstrained function results in Ada code called by system threads.
The Ada/APEX bindings provided with GNAT Pro for VxWorks 653 take care of all thread registration issues when using APEX processes. The bindings are provided as part of the source and object paths, just like the remainder of the Ada run-time library.
Ravenscar Cert does not support the use of foreign threads (e.g., APEX processes).
4.3.4. Dynamic Allocation¶
A limited dynamic allocation model is supported by this profile. The
System.Memory is provided, as described in
Allocators. The package provides
a simple version of function
gnat_malloc that simply calls the
malloc routine. Deallocation is prohibited on VxWorks 653 in
certified partition operating system (POS) application partitions.
Note that in VxWorks 653 partitions that use APEX facilities, dynamic allocation is prohibited once the partition has been set into normal mode.
The cert subset supports all standard Ada forms of exponentiation.
4.3.6. 64-bit Numeric Types¶
64-bit fixed point and integer types are fully supported.
4.3.7. Utility Routines¶
The following are provided in addition to the library packages available with the Cert Profile:
GNAT.Debug_Utilitiesprovides formatting routines for use in I/O.
Ada.Exceptions.Exception_Tracesprovides a non-symbolic traceback capability that can be used with
vxaddr2lineto generate symbolic tracebacks. See The GNAT User’s Guide Supplement for Cross Platforms.
Pragma Assertis supported.
4.4. The Ravenscar Profiles¶
The Ravenscar profile defines a subset of tasking features suitable for use in applications having extremely demanding requirements. The profile is a part of the Ada programming language and is defined by the language standard in section D.13 of the Real-Time Systems annex.
The profile is intended to support four application domains:
hard real-time applications requiring predictability,
safety-critical applications requiring formal certification,
high-integrity applications requiring formal verification, and
embedded applications requiring small memory footprint and low execution overhead.
The resulting tasking subset is designed to be small enough to allow efficient and analyzable run-time libraries, but large enough to permit programming styles needed in practice for all these domains.
For details of using the Ravenscar profile, including what the subset allows and excludes, see Guidance for the use of the Ada Ravenscar Profile in high integrity systems, ISO/IEC Technical Report 24718.
The Ravenscar Profile is silent about the Ada language’s sequential features. GNAT Pro provides a number of run-time libraries with the standard Ravenscar tasking subset and differing parts of the remaining sequential language supported. The following sections describe these run-times.
In the context of GNAT Pro, the term Ravenscar Profile means not only the tasking subset defined by the language standard, but also the sequential feature subset defined either by the Zero Footprint Profile (Ravenscar SFP) or the Cert Profile (Ravenscar Cert). Thus the Ravenscar SFP Profile is a proper superset of the Zero Footprint Profile and the Ravenscar Cert Profile is a proper superset of the Cert Profile (excepting packages Ada.Calendar and Calendar, which are prohibited by the Ravenscar profile).
A user specifying
ravenscar-sfp as the
will therefore be able to use the permitted features in the
Zero Footprint Profile.
A user specifying
ravenscar-cert-rtp as the
--RTS= option will be able to use the permitted features in the
4.4.1. Pragmas Automatically Enabled in the Ravenscar Profiles¶
The same pragmas automatically enabled in the Zero Footprint profile (see Pragmas Automatically Enabled in the Zero Footprint Profile) are also automatically enabled in the Ravenscar SFP profile:
The Ravenscar SFP Profile uses the same last chance handler scheme as the Zero Footprint Profile. The Ravenscar Cert Profile uses the same scheme as the Cert Profile. The last chance handler is expected to terminate the whole application in both cases.
This pragma is enabled for both Ravenscar profiles.
4.4.2. Non-tasking Predefined Packages in the Ravenscar Profiles¶
The Ravenscar SFP Profile is a superset of the Zero Footprint Profile. So
Predefined Packages in the Zero Footprint Profile, is
still relevant to the Ravenscar Profile, with one difference:
s-secsta.adb is provided.
See Functions Returning Unconstrained Objects for further details.
The Ravenscar Cert Profile is a superset of the Cert Profile. It provides the
same packages as the Cert Profile, except for
Calendar, which are disallowed by the Ravenscar profile definition.
The Ravenscar Cert profile also provides attributes
'Value as does the Cert profile.
4.4.3. Interrupt Handling in the Ravenscar Profiles¶
Interrupt handling is supported in the Ravenscar Profiles except for the
VxWorks 653 target, LynxOS-178 and in VxWorks 6 Cert.
The mechanism is as defined in Annex D of the
Ada Reference Manual;
the handler is supplied as a parameterless protected procedure,
Attach_Handler provides static attachment, and
Interrupt_Priority establishes the priority of the handler.
In GNAT Pro for VxWorks DO-178B and in VxWorks 6
Cert SKM’s, you can use the
intConnect() routine directly, for
dynamic attachment of handlers to interrupts.
In either case there is no task switching; the interrupt handler is executed
at the priority given by the
Interrupt_Priority pragma, on the
stack of the task that was running when the interrupt occurred (for
VxWorks) or on a dedicated interrupt stack (for bareboard platforms).
4.5. The Jorvik Profile¶
In addition to the Ravenscar tasking profile, GNAT supports the Jorvik (pronounced “yourvick”) profile, a new tasking profile in the Ada 202x language standard. Jorvik is the standardization of the older GNAT_Extended_Ravenscar profile. The latter profile name remains in GNAT as an alias to the Jorvik profile for compatibility with existing applications.
The Jorvik profile relaxes certain Ravenscar profile restrictions in order to increase expressive power for applications in the hard real-time and embedded system domains. Applications exclusively in these two domains typically do not require the formal certification and verification analyses imposed by the other Ravenscar domains. As a result, the new profile allows an underlying tasking run-time library implementation that, although somewhat more complex, remains small and efficient. However, for those applications requiring the most rigorous forms of analysis, i.e., those required for certification, the Ravenscar profile remains the best choice.
GNAT Pro provides a number of run-time libraries providing the Jorvik tasking subset, with differing subsets of the remaining sequential language supported. The following sections describe the Jorvik profile included in these run-times. Anything not specified as removed or altered from the Ravenscar profile remains unchanged in the Jorvik profile.
4.5.1. Number of Entries Per Protected Object¶
The Jorvik profile does not specify a value for Max_Protected_Entries. As a result, multiple entries per protected object are allowed.
Note that this change also allows entry families to have more than one member.
4.5.2. Number of Queued Callers per Entry¶
The Jorvik profile does not specify Max_Entry_Queue_Length. As a result, multiple callers can be queued on any given protected entry, rather than only one at a time. Task entries remain disallowed.
Note that any protected object containing protected entry declarations can specify, for each entry, the maximum number of callers allowed. This maximum number is checked at runtime, if specified, and can be used to compute a less pessimistic WCET off-line. Specification of the maximum value is optional.
The maximum value is specified via the language standard aspect or pragma Max_Queue_Length applied to that entry. (Max_Queue_Length is defined independent of Jorvik.) The value must be a static (positive) integer value. For example:
protected type P is entry A (Item : Integer) with Max_Queue_Length => 2; entry B (Item : Integer); pragma Max_Queue_Length (X); private ... end P;
4.5.3. Entry Barriers¶
The Jorvik profile does not specify Simple_Barriers. Instead, the new language-standard restriction “Pure_Barriers” is applied automatically. As a result, in addition to simple Boolean local variables, more complex Boolean expressions are allowed.
However, these expressions are still limited in content so that side effects, exceptions, and recursion are impossible. Removing the possibility of side effects is important because the language does not specify the number of times a given barrier is evaluated. Allowing exceptions would complicate the implementation, whereas the goal is an efficient and predictable run-time library implementation that minimizes barrier evaluation cost.
Specifically, “Pure_Barriers” allows the following:
References to components of the protected object
References to discriminants of the protected object
Enumeration (and thus character) literals
Predefined relational operators
Predefined logical operators (“and”, “or”, “xor”, “not”)
Short-circuit control forms (“and then”, “or else”)
The Count attribute
The list above is a general description intended to give an idea of the enhancements. Several of the above have restrictions. See the Ada 202x draft Reference Manual description for precise details (section D.7 “Tasking Restrictions” specifically.)
Note that the Count attribute is allowed in the barriers for protected entries (and protected entry families), not just within entry bodies as in Ravenscar.
4.5.4. Relative Delay Statements¶
The Jorvik profile does not specify No_Relative_Delay. As a result, both relative and absolute delay statements are allowed.
Although relative delay statements are not appropriate for expressing cyclic behavior, there are cases in which a relative delay has precisely the required semantics. For example, a relay may have a requirement that it not be actuated more than N times per second. A relative delay after each actuation directly implements that requirement.
4.5.5. Additional Non-Tasking Restrictions Removed¶
Some Ravenscar restrictions are not related to tasking and can be relaxed without affecting timing analysis and space/speed performance.
The Jorvik profile does not specify No_Implicit_Heap_Allocations. This restriction is in the standard Ravenscar profile for the sake of the other domains and need not be applied when focusing on real-time and embedded systems. (Note that users can specify this restriction in their application code if they want the restriction to apply.)
No_Implicit_Heap_Allocations restriction has been
18.104.22.168. No Dependence on Ada.Calendar¶
The Jorvik profile removes the restriction prohibiting use of the Ada.Calendar package. This restriction is present in standard Ravenscar because the Ada.Real_Time package has more appropriate semantics for real-time/embedded applications. However, not all usage of Ada.Calendar is unreasonable, for example time-stamping log messages.
4.5.6. Default Profile¶
The Jorvik profile is active by default on those platforms that support it. Users can instead specify the Ravenscar profile by applying pragma Profile, with Ravenscar as the parameter.