AdaCore Release Notes¶

GNAT Pro 24 Release Notes
GNAT Dynamic Analysis Suite (previously known as GNATcoverage) 24 Release Notes
GNAT Static Analysis Suite (previously known as CodePeer) 24 Release Notes
Libadalang 24 Release Notes
SPARK 24 Release Notes
IDE 24 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.

GCC Back-End Update
AWS and GNATColl Support for Cross Linux
Jorvik support for light-tasking run-time
Ada Support
- String Interpolation
- Variables in Sequences of Statements
Storage_Model
Platforms

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.

New Targets ¶

GNAT Pro now supports Windows 11, both as a host and a target.
GNAT Pro now supports VxWorks 7 versions released in 2023 (23.03 and 23.09).

Platform Status Changes ¶

GNAT Pro Ada for QNX ARM 32 is baselined, the last release is 23.
GNAT Pro 24 does not 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

GNAT Dynamic Analysis Suite (previously known as GNATcoverage) 24 Release Notes ¶

C++ support
Coverage Criteria for Ada 2012 Contracts
Initial Support for Ada 2022
Integrated instrumentation
GNATfuzz and GNATtest integration
Improvement of test generation heuristics with value substitution

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 ¶

Redesign of CodePeer User Experience
Redesign of Levels
Incremental results in Infer

Redesign of CodePeer User Experience ¶

CodePeer is now called through a new command line tool gnatsas. This tool will now store 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 ¶

CodePeer / 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.

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.

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.

VS Code Extension for Ada
Refactorings
Editing and Completion
GNATdoc

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.