AdaCore Release Notes¶
GNAT Pro 24 Release Notes¶
We present here a few highlights of the new features in GNAT Pro 24. You can access the complete list on the GNAT Pro 24 feature file.
Vulnerability report¶
From 24.2, you can download the GNAT vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
GCC Back-End Update¶
The GNAT Pro Ada, C and C++ has now been updated to GCC 12. See the GCC 12 changes for the corresponding capabilities as well as updates to C and C++.
AWS and GNATColl Support for Cross Linux¶
GNATcoll is a library of Ada capabilities, and AWS (Ada Web Server) is a library that allows an Ada application to interact through a web interface and services. They have both been ported to cross linux products, targeting ARM architecture.
Jorvik support for light-tasking run-time¶
Jorvik is an extension of the Ravenscar profile introduced in Ada 2022, relaxing some restrictions such as a single entry per queue. The light tasking run-time provided for bare metal and some cross ports now supports Jorvik. For more information see our Jorvik blogpost
Ada Support¶
String Interpolation¶
String interpolation allows to easily introduce expressions to be computed directly in a string literal. For example:
procedure Test_Interpolation is
X : Integer := 12;
Y : Integer := 15;
Name : String := "Leo";
begin
Put_Line (f"The name is {Name} and the sum is {X + Y}.");
end Test_Interpolation;
See the String Interpolation RFC for more details.
Variables in Sequences of Statements¶
It is now possible to declare variables outside of sequences of statements, for example:
if X > 5 then
X := X + 1;
Squared : constant Integer := X**2;
X := X + Squared;
else
X := X - 1;
Cubed : constant Integer := X**3;
X := X + Cubed;
end if;
See the Local Vars RFC for more details.
Storage_Model¶
Storage_Model is an experimental Ada capability that allows an Ada access type to point to a non-native memory area. A typical example is a mixed CPU / GPU application where the memory residing on the GPU can be allocated, deallocated and accessed through specific functions. A pointer associated with a storage model will have user-defined function for allocation, deallocation, copy from the foreign memory to native memory and back.
See the Storage Model RFC for more details.
Platforms¶
GNAT Pro for CUDA¶
CUDA is a platform provided by NVIDIA to develop general purpose code on their hardware. The GNAT for CUDA product is relying on NVIDIA CUDA to allow Ada users to write Ada code running directly on NVIDIA GPU. It offers a binding to NVIDIA C API as well as an Ada compiler targetting directly the NVIDIA GPU intermediary machine language PTX. See the GNAT for CUDA webinar for more details.
C++ for Bare Metal¶
C++ support will be added to bare metal products targeting PowerPC, x86, RISC-V, LEON3 and ARM. Customers currently supported on C on these targets will get C++ support at no extra cost. This port will be provided with a reduced version of the standard C++ library, fit for development on small bare metal target with no OS support.
Platform Status Changes¶
Hosts¶
GNAT Pro now supports Windows 11, both as a host and a target.
GNAT Pro no longer support Windows 8.1, Windows Server 2012 and 2012 R2
GNAT Pro 24 is the last release supporting RedHat Enterprise 7 and Ubuntu 18.04
Targets¶
GNAT Pro now supports VxWorks 7 versions released in 2023 (23.03 and 23.09).
GNAT Pro now supports VxWorks Helix on x86_64 targets, with VxWorks 7 Cert as a GuestOS.
GNAT Pro Ada for QNX ARM 32 is baselined, the last release is 23.
Detailed New Feature List¶
Optimizations¶
More efficient slice assignments in packed records¶
The object code generated for assignments from and to slices of unpacked arrays that are components of packed records is more efficient.
Improved extended return for nonlimited by-reference¶
Extended return statements present in functions returning a nonlimited by-reference type no longer incur a copy operation.
Improved efficiency of slice-of-component assignment¶
The efficiency of slice assignment is improved when the left- or right-hand side is a slice of a component or a slice of a slice. Previously, the optimization was disabled in these cases, just in case there might be a volatile or independent component lurking. Now we explicitly check all the relevant subcomponents of the prefix for volatility and independence.
Optimize 2**N¶
A redundant check is now avoided in the case of exponentiation by a power of 2 (which are normally turned into shifts).
Better stack usage estimates for packed arrays¶
The compiler now gives better estimates of the stack storage used by arrays using the Pack pragma.
Avoidance of duplicated streaming subprograms¶
In some common cases, a reference to a streaming attribute for an untagged type caused the compiler to generate the needed subprogram “on demand”. When there are multiple such references, (for example, two calls to Some_Untagged_Record_Type’Write), then it is better to avoid generating multiple essentially-identical subprograms; instead, a subsequent attribute reference can now “reuse” an already-generated subprogram (at least in some cases). Due to this optimization, a generated streaming subprogram may now have multiple call sites. This means the compiler can no longer use the source position information from the (one and only) call site. If an exception is raised during a streaming operation, this can affect the reported raise location.
Optimized CW objects initialized by function calls¶
Stand-alone and return objects of a class-wide type that are initialized by a function call are now implemented more efficiently.
Diagnostics¶
Warnings suppressed on derived True/False¶
GNAT no longer gives an “always True” or “always False” warning if the expression in question is the literal True or False of a type derived from Boolean that has convention C or Fortran. Previously, such cases caused a warning that was deemed to be unhelpful.
New warning for ineffective static predicate tests¶
The compiler now emits a warning if a static predicate tests for a value that does not belong to the parent subtype. For example, in “subtype S is Positive with Static_Predicate => S not in 0 | 11 | 222;”, the 0 is ineffective because Positive already excludes that value. Generation of this new warning is controlled by the -gnatw_s switch, which can also be enabled via -gnatwa.
Better selectivity of warnings on deleted code¶
When passing the switch -gnatwt to track deleted code, GNAT now only issues warnings on branches that are not under a “statically disabled condition” as defined in SPARK User’s Guide, section 7.3.2. This avoids spurious warnings on code deactivated through the use of a global configuration constant.
New warning about noncomposing user-defined “=”¶
The new switch -gnatw_q enables a warning for a user-defined “=” that does not compose as might be expected (i.e. is ignored for predefined “=” of a containing record or array type). For example, if an access type has a user-defined primitive “=”, then the default “=” for a record type containing a component of that access type ignores the user-defined “=”. This switch warns in such cases. See RM-4.5.2(14/3-15/5, 21, 24/3, 32.1/1) for the exact Ada rules on composability of “=”.
Documentation¶
Improved documentation for -gnatw.h compiler switch¶
The -gnatw.h option enables warnings about “gaps” in record layout specifications. In the case of a “partial” layout specification, where the locations of some components are left unspecified, the resulting warnings may be incomplete or incorrect, and this behavior is now documented.
Memory allocation and type conversions¶
Truncate for conversion from floating to fixed point¶
Dynamic conversions from floating-point types to ordinary fixed-point types now truncate the value (toward 0) instead of rounding it (to the nearest number) if it is not exactly representable. This makes them consistent with both static conversions between these types and the value of the Machine_Rounds attribute, which is False for all fixed-point types. Rounding is still available either under the debug switch -gnatd.N or by explicitly using the Round attribute.
Ensure minimum primary default stack size¶
The gnatbind -d switch allows setting the default primary stack size for new tasks. The value set with this switch was formerly not checked to be at least the minimum stack size required by the target platform, but now the minimum required stack size will be used when the value passed to the binder is too small.
Conversions from Big_Integer to large integer types¶
In Ada 2022, the generic packages Signed_Conversions and Unsigned_Conversions of Ada.Numerics.Big_Numbers.Big_Integers now support conversions to large integer types, for example Long_Long_Unsigned, as well as Long_Long_Long_Integer and Long_Long_Long_Unsigned on 64-bit platforms.
Default stack size for tasks on Aarch64 QNX¶
The default primary stack size for native threads on Aarch64 QNX is 256 KB. The QNX runtimes now use the same default value for newly created tasks.
Use large type in membership test of universal value¶
The actual type used to perform a membership test applied to a nonstatic expression of a universal type, for example an attribute whose type is universal_integer and whose prefix is not static, is now large enough to avoid a range check failure in almost all cases.
Dependencies¶
Drop OpenSSL dependency for the mold linker¶
The mold binary distributed in the GNAT Pro toolchain no longer has a run-time dependency on OpenSSL: users no longer have to provide libcrypto in order to call this linker.
Tunability¶
Addition of gnatpp layout switch¶
A –layout switch was added to gnatpp, which controls the general formatting style. The switch has the following options: default, minimal, compact, and tall. The default layout follows a compact style, but adds alignment and puts some keywords on a separate line. The minimal layout avoids changing the source layout by keeping all line breaks from the original source. The compact layout avoids adding line breaks and alignment by packing as many subexpressions on the same line as possible. Finally, the tall layout favors adding lines breaks and alignment.
Exact real values used in JSON output with -gnatRj¶
The output generated by the compiler when the -gnatRj switch is specified now contains exact real values instead of decimal approximations.
Finer control of GNAT-defined Ada extensions¶
The -gnatX switch (and the related Extensions_Allowed pragma) was previously a two-valued all-or-nothing option. Now the compiler supports enabling a curated subset of the GNAT-defined Ada extensions without enabling others via the -gnatX switch, and will enable all of the language extensions via the new -gnatX0 switch. Similarly, the existing “ON” argument for the Extensions_Allowed pragma now only enables the curated subset; the new argument “ALL” enables all language extensions. The subset of language extensions currently includes prefixed-view notation with an untagged prefix, fixed-low-bound array subtypes, casing on composite values, and static intrinsic functions. Users of other GNAT-defined extensions may have to update switch settings (replacing “-gnatX” with “-gnatX0”) or pragma arguments (replacing “On” with “All”).
New switch -gnatyz and improvements to -gnatyx¶
The -gnatyx switch now checks for case statements and ranges. In addition, a new switch -gnatyz is introduced to check for unnecessary parentheses according to operator precedence rules. The switch -gnatyg enables -gnatyz by default.
New switch to set reverse Bit_Order threshold to 64¶
The switch -gnateH has been implemented to set the threshold of reverse Bit_Order clauses, as defined by RM 13.5.1(13.3/2), to 64.
Packaging¶
PIE enabled by default on Native Linux¶
GNAT now generates Position Independent Executable (PIE) code by default. PIE binaries are loaded into random memory locations, introducing an additional layer of protection against attacks. With previous versions, it was possible to build PIE executables, but this feature had to be enabled explicitly during both the compilation and the link.
Runtimes¶
CCG: Interfaces.C.Strings added to the runtime¶
GNAT CCG now includes the predefined package Interfaces.C.Strings in its runtime.
Ada.Iterator_interfaces added to the CCG runtime¶
The CCG compiler now provides the Ada.Iterator_interfaces unit, to allow user-specified iteration.
Handle pthread errors in LynxOS-178 tasking rt¶
The Delay_Until implementation of the light-tasking runtime on LynxOS-178 now raises an exception if pthread_cond_timedwait returns an unexpected error.
Language features¶
Extend Round attribute to ordinary fixed point types¶
The Round attribute specified by the Ada RM for decimal fixed point types is now also available for ordinary fixed point types.
Atomic store primitives in System.Atomic_Primitives¶
The System.Atomic_Primitives unit now exposes atomic store primitives alongside the existing atomic load primitives.
User-defined literal aspects for derived untagged¶
The subprograms named in Ada 2022 user-defined literal aspects of untagged types can now be overridden by their derived types.
GNAT Dynamic Analysis Suite (previously known as GNATcoverage) 24 Release Notes¶
We present here a few highlights of the new features in GNAT DAS 24. You can access the complete list here.
Vulnerability report¶
From 24.2, you can download the GNAT DAS vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
Platform Status Changes¶
GNAT Dynamic Analysis Suite depends on GNAT Pro toolchains; as such, changes to GNAT Pro-supported host platforms are equally applicable to the GNAT Dynamic Analysis Suite. For detailed information on platform status changes to the GNAT Pro suite, see the GNAT Pro Release notes.
C++ support¶
GNATcoverage now support C++ code when compiler with GNAT Pro C/C++, up to MC/DC.
Coverage Criteria for Ada 2012 Contracts¶
GNATcoverage now provides coverage criteria for Ada 2012 contracts, including pre-conditions, post-conditions, invariants and predicates, for up to MC/DC.
Initial Support for Ada 2022¶
Initial support for constructions introduced by Ada 2022 has been introduced at all levels.
Integrated instrumentation¶
GNATcoverage now offers an alternative instrumentation process that seamlessly integrates into the build workflow. Instead of instrumenting the entire source closure before building, we configure the build process to utilize a specialized compiler generated by GNATcoverage. This compiler wrapper performs on-the-fly instrumentation and subsequently delegates the compilation task to the original compiler. This feature is currently available as a prototype for C/C++ languages, using gcc/g++ on a Linux host.
GNATfuzz and GNATtest integration¶
GNATfuzz will be able to take an existing GNATtest testuite as a seed of fuzzing. It will also be able to generate a testsuite containing a subset of significant tests discovered through the fuzzing campaign, to re-import to GNATtest. See the GNAT DAS user’s guide for more details.
Improvement of test generation heuristics with value substitution¶
GNATfuzz will locate constant values within equality conditions in the binary code and analyze the data to see if there is a correspondence to the input state. It will then look in the input corpus and try to locate matching values with the values being compared against the constants. These matching input values will be substituted by the constants as a means to improve the quality of the test case generation and solve branch conditions with a clear input to state correspondence. This is done through the integration of an AFL++ feature known as CMPLOG.
GNAT Static Analysis Suite (previously known as CodePeer) 24 Release Notes¶
We present here a few highlights of the new features in GNAT SAS 24. You can access the complete list here.
Vulnerability report¶
From 24.2, you can download the GNAT SAS vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
Redesign of GNAT SAS User Experience¶
The product is now called through a new command line tool gnatsas. This tool now stores results and reviews in files that can be placed under version control, as opposed to an SQL database. Other aspects of the command line interface are simplified (such as CodePeer levels). This will improve overall user experience, in particular when interacting with CI pipelines or when supporting project architectures involving reused components or multiple versions.
Redesign of Levels¶
CodePeer / GNAT SAS –level option is discontinued. Instead, we now provide two modes, –mode=fast which is default, and –mode=deep intended for offline analysis that can spare larger amount of resources.
Incremental results in Infer¶
GNAT SAS now supports incremental analysis in Infer: after an entire project is analyzed, local changes results in partial analysis related to these local changes. Together with the (pre-existing) incremental analysis features of Inspector, this will allow developers to have rapid feedback on their current changes.
Production of SARIF format¶
GNAT SAS now produces outputs compatible with the Static Analysis Results Interchange Format (SARIF) industry standard. SARIF specifies a format for storing messages generated by static analysis tools that is supported by a set of widely used viewers.
Platform Status Changes¶
GNAT Static Analysis Suite depends on GNAT Pro toolchains; as such, changes to GNAT Pro-supported host platforms are equally applicable to the GNAT SAS. For detailed information on platform status changes to the GNAT Pro suite, see the GNAT Pro Release notes.
Libadalang 24 Release Notes¶
We present here a few highlights of the new features in Libadalang 24. You can access the complete list here.
Vulnerability report¶
From 24.2, you can download the Libadalang vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
Support for Data Representation Queries¶
Libadalang now supports queries to allow to access to the binary representation of data types. This representation depend on the compiler and switches used, and will be derived from the output of the compilation process. This is similar to ASIS DDA.
Improved performances of LKQL¶
Performances of LKQL (LanKit Query Language) have been improved, both from a memory footprint standpoint and speed of execution, notably thanks to the introduction of a just-in-time compiler.
Introduced Error Diagnostic¶
Libadalang is able to provide additional error diagnostics on syntax errors, name resolution errors, and legality rule violations.
- orphan:
SPARK 24 Release Notes¶
We present here a few highlights of the new features in SPARK 24. You can access the complete list here.
Vulnerability Report¶
From 24.2, you can download the SPARK vulnerability report from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
Improved Support of Language Features¶
Conditional Termination¶
Previously, GNATprove was designed to support primarily programs that always return normally. For SPARK 24, we extended the SPARK language and GNATprove to make termination explicit, by allowing fine-grained annotation of subprograms that propagate exceptions (see below) or that failing to terminate.
The new Always_Terminates
aspect allows users to specify procedures that
only terminate (return normally) or that raise an exception conditionally, in a
fine-grained manner. This aspect can be used to specify a boolean condition on
procedure inputs such that, if the condition evaluates to True, then the
procedure must terminate.
procedure P1 (...) with Always_Terminates;
-- P1 shall terminate on all its inputs
procedure P2 (...) with Always_Terminates => False;
-- P2 might terminate on some of its input, but it does not need
-- to.
procedure P3 (...) with Always_Terminates => Condition;
-- P3 shall terminate on all inputs for which Condition evaluates
-- to True.
Functions in SPARK should still always terminate and therefore cannot be annotated with this aspect.
Handling and Propagation of Exceptions¶
Previously, SPARK allowed exceptions to be raised but did not allow exceptions to be propagated or handled. GNATprove thus attempted to verify that raise statements could never be reached - i.e., that they were dead code.
For SPARK 24, we extended the SPARK language and GNATprove to support
propagation of exceptions to outer secope and local handling of exceptions.
Procedures that might propagate exceptions need to be annotated with the new
Exceptional_Cases
aspect, which allows the exceptions that might be
propagated to be listed and associated with an exceptional postcondition.
This postcondition is used both to restrict the set of inputs on which the
exception might be propagated and to verify callers when the exception is
handled in outer scopes.
procedure P1 (...) with
Exceptional_Cases => (others => False);
-- P1 cannot propagate exceptions. It is the default.
procedure P2 (...) with
Exceptional_Cases => (others => True);
-- P2 might propagate an unspecified exception
procedure P3 (X : T; Y : out T) with
Exceptional_Cases =>
(E1 => Cond1 (X),
E2 => Cond2 (Y));
-- P3 might propagate E1 or E2. The exceptional postconditions are
-- used both to:
-- * specify in which cases the exception might be raised - E1
-- can only be propagated on inputs on which Cond1 evaluates to
-- True.
-- * describe the effect of the subprogram when the exception is
-- propagated - when E2 is propagated, Cond2 (Y) evaluates to True.
-- A mix of the two is also possible.
Functions in SPARK still cannot propagate exceptions, so the aspect cannot be specified for them.
Enhanced Support for Relaxed_Initialization¶
The Relaxed_Initialization
aspect can now be used to relax the
initialization policy of SPARK on a case-by-case basis. The support for this
feature has been extended to support types annotated with subtype predicates.
Checks for Parameters of the Container Library¶
The formal parameters of the container library of SPARK are subject to requirements. For example, the provided equality function shall be an equivalence relation (symmetric, reflexive, and transitive). Previously, these requirements were treated as assumptions by the tool; the user was required to verify them by other means. The container library has been modified so these properties are now verified by the tool on every instance. If the verification is complex, users can provide lemmas to help the tool as additional parameters of the generic packages.
Program Specification¶
Functional Multisets in the SPARK Library¶
Functional multisets have been added to the SPARK Library. They are particularly useful in modeling permutations, e.g., when verifying sorting routines.
GNAT-specific Aspect Ghost_Predicate
¶
Ghost functions cannot be used in subtype predicates for non-ghost types: the
predicates may be evaluated as part of normal execution during, e.g.,
membership tests.To alleviate this restriction, it is now possible
to supply a subtype predicate using the Ghost_Predicate
aspect, making it
possible to use ghost entities in its expression. Membership tests are not
allowed if the right operand is a type with such a predicate.
Tool Automation¶
New Prover Versions¶
The Z3 prover shipped with SPARK was updated to version 4.12.2. The cvc5 prover shipped with SPARK was updated to version 1.0.5.
Better Provability with Containers¶
The container library of SPARK has been modified to improve provability. In particular, contracts on procedures used to modify these containers now use logical equality instead of Ada equality. This is notably more efficient when both equalities do not coincide because the logical equality, unlike the Ada one, is handled natively by the underlying solvers.
Better Provability when Using Size Attributes¶
GNATprove now calls GNAT to generate data representations in order to support more precisely size and alignment attributes in proof.
Tool Interaction¶
Explain Codes¶
GNATprove now has an option
gnatprove --explain
that prints to standard output a short explanation for
emitted messages, similar to rustc --explain
. This can be used for error
messages, warnings, or check messages. When a message has a corresponding
explanation, it includes an explanation code, such as [E0001]
, in the
message. Using the command --gnatprove --explain E0001
, users can display
the corresponding explanation. Note that while the GNAT compiler may also
issue messages with an “explain code” for messages related to the use of SPARK,
the command to get the explanation is always gnatprove --explain
.
Fine-grained Specification of Analysis Mode¶
For customers who are migrating large bodies of code to SPARK, having to choose
between disabling analysis entirely (i.e., setting the SPARK_Mode
to
Off
) or committing to proof at Silver level (proof of absence of runtime
errors) may not always be satisfactory. Previously, the analysis level could be
set only at the project level, which is too coarse in such cases.
To help customers who are migrating large bodies of code to SPARK, we
introduced two new ways to set a more fine-grained analysis level. First, users
can select the analysis level for each unit, by setting the --mode
switch
for specific units in the GPR project file. Second, users can annotate their
subprograms with one of two new annotations:
pragma Annotate (GNATprove, Skip_Proof, Name_Of_Subprogram);
pragma Annotate (GNATprove, Skip_Flow_And_Proof, Name_Of_Subprogram);
These annotations disable proof on a per-subprogram basis. The annotation
Skip_Proof
allows users to benefit from flow analysis on a subprogram,
without having to go to full proof.
Counterexamples for Floating Point Values¶
Counterexample checking now supports floating-point numbers, so that counterexamples computed by a prover can be checked before being displayed to the user, when a proof does not pass.
Better Messages for Initialization and Incomplete Data Dependency¶
Messages emitted for reads of uninitialized data and incomplete Global and Depends contracts have been improved. Redundant messages are removed, initialization checks are condensed, and more errors are reported at once in case of incomplete contracts.
Incompatible Changes¶
Termination Annotations¶
The Annotate
pragmas that used to be defined for termination are no longer
supported. This includes Always_Return
, Might_Not_Return
, and
Terminating
. The Always_Terminates
aspect should be used instead on
procedures. Termination of functions is now checked by default.
Command-line Switches¶
The switch --checks-as-errors
now needs an argument on
or off
.
Previous usage of the switch should be replaced by --checks-as-errors=on
.
IDE 24 Release Notes¶
We present here a few highlights of the new features in IDE products for the 24 release.
Vulnerability Report¶
From 24.2, you can download the vulnerability report for each IDE product from the Release Download section. It will provide you the list of the CVEs that can impact this product and the corresponding impact analysis describing whether the product is concerned by each CVE.
VS Code Extension for Ada¶
The VS Code Extension for Ada is now officially supported.
This extension is based on the Ada Language Server, communicating with VS Code through the LSP protocol. It provides all the basic IDE features such as completion, syntax highlighting, tooltips, navigation and many others. The extension also provides automatic debug configurations to quickly debug your applications with GDB.
You can have a look to the extension’s guide for more information about the extension, including a more exhaustive list of available features and current limitations. A tutorial is also available to discover the extension in a more interactive way.

Refactorings¶
Auto Import and Sort Dependencies refactorings have been added to the Ada Language Server, and thus are available in both GNAT Studio and the VS Code Extension for Ada.

You can find a list of all the Ada-specific refactorings provided by the Ada Language Server, with some GIFs showing how they work here.
All these refactorings are available through what the LSP calls Code Actions. They are available via the light-bulb that appears on the left-side of the current editor when placing the cursor on a place where these refactorings can work (e.g: within a subprogram declaration for the Add Parameter refactoring).
The UI for refactorings has also been improved: GNAT Studio now displays a pulsating progress bar at the top of the current editor when renaming an entity, which disappears once the renaming is complete, and errors occuring during refactorings are reported in the Locations view.
Editing and Completion¶
Editor tabs for files that do not belong to the currently loaded project are displayed in Italic, allowing the user to quickly distinguish between files that belong to the project and those that do not.

You can now quickly create bookmarks very quickly by doing ctrl-clicks on editor line numbers.

Completion now proposes the corresponding use-clause when being immediately after a with-clause. You can trigger it by executing the complete identifier (advanced) action (ctrl+space by default) immediately after a with-clause.

GNATdoc¶
GNAT Studio now includes a new version of GNATdoc, based on Libadalang. This new GNATdoc has the big advantage to be able to generate documentation without having to rebuild your application. A number of bugs present in the old tool have been fixed too.
Please find more information about GNATdoc by reading its user’s guide.
