AdaCore Release Notes¶

GNAT Pro 26 Release Notes ¶

We present here a few highlights of the new features in GNAT Pro 26 You can access the complete list in the GNAT Pro 26 feature file.

GCC back-end update ¶

The GNAT Pro for Ada, C and C++ compilers have now been updated to GCC 14. See the GCC 14 changes for the corresponding capabilities as well as updates to C and C++.

GNAT Pro compilers targeting 32-bit Linux and Windows are now 64-bit executables.

LLVM back-end update ¶

The GNAT Pro LLVM for Ada compiler has now been updated to LLVM 19. See the LLVM 19 release notes for the corresponding capabilities.

New targets ¶

GNAT Pro LLVM for Ada now supports Arm 64-bit VxWorks 7, starting with release 26.1
GNAT Pro for Ada for Arm 64-bit bare-metal platforms now supports the Xilinx ZynqMP Arm Cortex-R5 processor
GNAT Pro now supports x86 64-bit cross Linux hosted on Linux
GNAT Pro now supports Arm 64-bit LynxOS-178 MfA 2025.08

In this release, we’re introducing GPRbuild2, the successor to our build orchestration tool GPRbuild. GPRbuild2 supports user-defined actions. Actions have their own signatures and provide a generic system to identify build trigger conditions.

Currently, GPRbuild remains the default for the 26 release. GPRbuild2 is considered beta but will be the default in the 27 release. We encourage you to give GPRbuild2 a try by setting an environment variable like this:

export GNAT_GPR_ENGINE=2

To reset to GPRbuild, simply set the environment variable to:

export GNAT_GPR_ENGINE=1

You can find additional details about GPRbuild2 in the User Guide.

Mixed-language applications ¶

Improve mixed Ada/C++ support for bare-metal Ada runtimes ¶

Bare-metal Ada runtimes support the execution of C++ global object initialization and destruction.

New System.C_Time and GNAT.C_Time run-time units ¶

The System.C_Time and GNAT.C_Time units are now available in the run-time library units of native and selected cross platforms. They provide the time_t, timeval, and timespec types corresponding to the C types defined by the OS, as well as various conversion functions. The latter unit is a mere renaming of the former under the GNAT hierarchy.

CCG support for AArch64 target triplets ¶

When describing the target to CCG, you can now also use AArch64 triplets like “aarch64-unknown-elf” in addition to the already supported x86 and x86_64 variants.

StdCall calling convention support in CCG ¶

On Windows, the StdCall convention can now be specified for functions. This is usually the case for Win32 runtime functions. This calling convention, if set in Ada code, is emitted in C. The modifier can be specified by -c-target-modifier-stdcall=<modifier>, and by default is set to __stdcall on the MSVC compiler. When not specified, all functions with StdCall calling conventions will be emitted with __attribute__((stdcall)).

VxWorks ¶

VxWorks 7 Ada Bindings ¶

This release documents how to generate an Ada API that allows direct access to the VxWorks 7 C APIs, using h2ads.

GNATColl Support for VxWorks 7 ¶

This release includes GNATColl for all supported VxWorks 7 architectures.

LLVM capabilities ¶

Better debug information in GNAT Pro LLVM ¶

The LLVM back-end of the GNAT Pro for Ada compiler will emit better debug information to improve the debugging experience with GNAT Pro LLVM.

Shared Ada runtimes for Linux GNAT Pro LLVM ¶

GNAT Pro for Linux will include shared Ada runtimes for use with the LLVM back-end.

Native GNAT Pro LLVM includes the light runtime ¶

Native GNAT Pro LLVM now includes the light and light-tasking runtimes alongside the native one. It can be selected by passing the –RTS flag to gprbuild, or configured in the .gpr file.

GNAT Pro LLVM now links with lld ¶

The GNAT Pro LLVM compiler now uses the LLVM linker lld instead of the GNU linker for all targets.

Windows additions ¶

Addition of Win32 Ada Interlocked methods ¶

The Win32.Winbase API has been augmented with some interlocked methods based on GCC intrinsics that support 32-bit and 64-bit words.

New API routines added to Win32.Winbase ¶

A set of new standard Win32 routines has been implemented in Win32Ada. The added set comprises OpenThread, QueryThreadCycleTime, SetFilePointerEx, GetSystemTimeAsFileTime, ReadDirectoryChangesW, CancelIo, and HasOverlappedIoCompleted.

Ada support ¶

Extended_Access aspect ¶

A new aspect Extended_Access has been added as a GNAT-specific extension supported by the GCC backend. This extension enables the creation of accesses to array slices, and simplifies the use of objects of unconstrained arrays when they are allocated by a foreign language.

Extension for resource management via “finally” part ¶

A GNAT-specific extension has been added (enabled via -gnatX0) that allows a “finally” part in statement sequences, providing additional control over resource management within scopes. See the GNAT Reference Manual for details.

Optimizations ¶

Improved allocation of iterated container aggregates ¶

For a container aggregate of a bounded container type with a container_element_association given by an iterator_specification that iterates over a container object V (for example, “[for E of V => E]”), the compiler now determines the length of V and uses that as the size to allocate for the container aggregate. Prior to this enhancement, the compiler would typically use the default value of the Empty function’s Capacity parameter when allocating space for the aggregate, which could easily lead to Capacity_Error being raised for the aggregate. Note that this enhancement is only used for aggregates of container types coming from instantiations of the predefined bounded container generics, and not for user-defined container types, and it currently only applies when the object being iterated over is a simple object (in particular, the object is not an indexed name, selected component, explicit dereference, or function call).

More efficient Unchecked_Conversion for array types ¶

The compiler now implements calls to instances of Unchecked_Conversion more efficiently when the target type is a large array type whose bounds are not static in the Ada sense, but can nevertheless be computed at compile time.

Improved nonlimited by-reference calls as default ¶

The compiler generates more efficient object code for default values of record components that are a call to a function returning a result of a nonlimited by-reference type, which includes controlled and tagged types.

Improved efficiency of very large shift counts ¶

For a call to an intrinsic shift function (Shift_Left, Shift_Right, or Shift_Right_Arithmetic), if the value is known at compile time, and the shift count is very large (for example Shift_Right(X, Amount => 10**9), where the value of X is known), the compiler would take a long time to compute the value. This change improves the compile-time speed for such computations.

Improved nonlimited by-reference calls as components ¶

The compiler generates more efficient object code for components of aggregates that are assigned a call to a function returning a result of a nonlimited by-reference type (which includes controlled and tagged types).

Faster aggregate return for nonlimited by-reference ¶

Simple return statements whose expression is an aggregate present in functions returning a nonlimited by-reference type no longer incur a copy operation.

Improved nonlimited by-reference calls in allocators ¶

The compiler generates more efficient object code for allocators whose qualified expression is a call to a function returning a result of a nonlimited by-reference type, which includes controlled and tagged types.

GNAT Pro for Rust 26 Release Notes ¶

We present here a few highlights of the new features in GNAT Pro for Rust 26.

Rust Version ¶

This release of GNAT Pro for Rust is based on Rust version 1.85.0, which introduces support for Rust Edition 24.

Vulnerability report ¶

You can download the GNAT Pro for Rust 26.0 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.

Platforms ¶

New Platforms ¶

GNAT Pro for Rust 26.0 is now available on the following new platforms:

Aarch64 Linux, hosted on Windows
Aarch64 QNX 8.0, hosted on Linux
Aarch64 VxWorks 7 version 25.03, DKM (no_std), hosted on Linux and Windows
Aarch64 VxWorks 7 version 25.03, RTP, hosted on Linux and Windows

Existing Platforms ¶

GNAT Pro for Rust 26.0 is already available on the following platforms:

Hosts ¶

x86_64 Linux
x86_64 Windows 11

Targets ¶

Aarch64 Bare Metal (no_std), hosted on Linux and Windows
Aarch64 Linux, hosted on Linux
x86_64 Linux
x86_64 Windows 11

Tools ¶

GNAT Pro for Rust 26.0 includes the following tools:

Toolchain ¶

cargo
rustc
rustfmt
gcc (for linking only)
binutils
gdb

Multi-Language Build Support ¶

gprbuild
gprclean
gprconfig
gprinstall
gprinspect
gprname

IDE and Analysis ¶

rust-analyzer
clippy

ZynqMP BSP ¶

GNAT Pro for Rust 26.0 includes a Board Support Crate for the AMD Zynq UltraScale MPSoC. See the documentation for more information.

GPRbuild Integration ¶

GNAT Pro for Rust 26.0 provides initial, beta integration with GPRbuild. This support allows you to include Rust library crates in your Ada projects. See the documentation for more information.

GNAT Dynamic Analysis Suite 26 Release Notes ¶

We present here a few highlights of the new features in GNAT Dynamic Analysis Suite 26. You can access the complete list in the GNAT DAS 26 feature file.

New ports ¶

GNATcoverage now supports coverage analysis for Rust
GNATfuzz now supports native Windows

Code coverage reports ¶

Allow consolidation of units with varying SCOs ¶

When instrumenting code that may be preprocessed differently according to the configuration, the source-coverage obligations may vary across configurations. GNATcoverage now accepts consolidation of coverage results for units with varying source-coverage obligations, as long as they are not intertwined.

Overriding browser search in GNATcov HTML report ¶

As the GNATcoverage HTML report uses virtual scrolling, it does not render the whole source, but only the part that is visible on screen. This made native browser search difficult, as it only worked on the rendered HTML. Searching in the HTML report is now improved by overriding the native search feature to search the whole document.

Add keyboard shortcuts to GNATcov html report ¶

Add keyboard shortcuts to navigate between violations in GNATcoverage html report.

Allow generation of a coverage report without traces ¶

GNATcoverage now generates a report with only coverage violations and issues a warning when no traces are specified.

GNATcoverage enhancements ¶

External annotations for C/C++ coverage analysis ¶

GNATcoverage supports coverage annotations in an external file for C and C++.

Function and call coverage for C/C++ in GNATcoverage ¶

The function and call coverage level that was introduced in release 25 for the Ada language is extended to the C/C++ languages.

Similarly to Ada, function coverage analysis considers a function covered if its body is entered at least once. Note that for C++, lambda functions are analyzed as well as templated functions, class methods, and overloaded operators. However, class constructors and destructors are ignored.

Call coverage analysis considers a function call covered if it was evaluated at least once. Note that this includes function pointer calls and overloaded operator calls.

This new coverage level can be activated alongside any preexisting coverage level combination, through the use of the “fun_call” option of the “–level” switch.

See section 1.5.8 of the GNAT DAS user manual for more details.

Guarded expression coverage for Ada in GNATcoverage ¶

Guarded expression coverage analysis provides insight on the evaluation of sub-expressions nested within conditional expression constructs.

The analysis processes 3 categories of sub expressions nested within conditional constructs, specifically:

for If expressions, each dependent expression (if Cond then <dept_expr> else <dept_expr>);
for Case expressions : each dependent expression (when X => <dept_expr>);
for Quantified expressions : the predicate expression (for all/some I in V => <predicate_expr>)

Guarded expressions coverage analysis is only available for Ada 2022, as it uses Ada2022 features under the hood. Also, the coverage level is only available through source instrumentation.

See section 1.5.9 of the GNAT DAS user manual for more details.

Support in GNATcov for –no-stdlib configuration ¶

GNATcoverage now simplifies support for Ada applications which are not linked against the Ada runtime library. The gnatcov setup command now supports a –no-stdlib switch to generate a coverage runtime in which all the units are compatible with the –no-stdlib builder switch. In such situation, the user is responsible for providing a function through which the coverage trace will be emitted at the end of the program execution.

See section “Coverage runtime setup for configurations with no Ada runtime” of the GNAT DAS user manual for more details.

GNATtest enhancements ¶

Ada preprocessing directives support ¶

GNATtest now supports Ada projects with preprocessing directives by ensuring preprocessing symbols can be passed to GNATtest and invoked through an integrated preprocessor. This enhancement streamlines the workflow for projects using conditional compilation, eliminating the need for manual preprocessing steps before test generation and execution.

Support for libraries defining an interface ¶

GNATtest supports generating stubs and test harnesses for library projects which define an interface.

Support for aggregate library projects ¶

GNATtest supports generating stubs for project trees containing aggregate libraries.

Support for tagged types test generation ¶

GNATtest generates test inputs for tagged types.

Improved support for generics and private types for test generation ¶

Test input generation for types declared in the private part of a package, and types declared in an instantiation of a generic package is supported.

Execution of generated testcases on embedded runtimes ¶

The testcase decoding runtime is compatible with embedded runtimes.

Improve test runner output in GNATtest ¶

GNATtest now accepts a –include-subp-name option to include the name of the subprogram under test in the test_runner output log. The default output is formatted as:

<filename>:<line>:<col>: <message>

whereas adding –include-subp-name on the command line will result in the output looking like:

<filename>:<line>:<col>: (<subp_name>): <message>

Improve –exit-status and –passed-tests switches ¶

The output of GNATtest when using –exit-status=on is now more useful when there are failing tests. The tool no longer reports that no test driver exited successfully when using “–exit-status=on” along with “–passed-tests=hide”. The exit status of GNATtest now depends on that of the executed test drivers when running them through “gnattest test_drivers.list”.

Recursive stubbing capabilities in GNATtest ¶

GNATtest can now be instructed to recursively stub all units in the import transitive closure of the unit under test, instead of only the direct imports. This behavior can be enabled through the –recursive-stub command line option.

GNATfuzz enhancements ¶

Integration of libFuzzer ¶

GNATfuzz integrates libFuzzer, a highly efficient, in-process fuzzing engine to its existing suite of fuzzing engines (AFL++, CmpLog, and SymCC).

Automatic execution of all fuzzable Ada subprograms ¶

GNATfuzz analyzes an entire Ada project, to identify automatically all subprograms that can serve as fuzzing entry points, and launch the corresponding fuzzing campaigns.

Automatic regression testsuite generation from fuzzing ¶

During fuzzing campaigns, GNATfuzz stores specific tests that trigger new paths and conditions, and provides these tests as a corpus for automatic regression testing. These tests can also seed future GNATfuzz fuzzing campaigns.

orphan:

GNAT Static Analysis Suite 26 Release Notes ¶

We present here a few highlights of the new features in GNAT SAS 26. You can access the complete list in the GNAT SAS 26 feature file.

New analyses ¶

Taint analysis ¶

GNAT SAS now offers taint analysis. Taint analysis spots security defects that arise when data flows from external data sources (called _sources_) to vulnerable subprograms (called _sinks_). For example, input from a user might flow to a subprogram that executes an operating-system command. Without appropriate handling of the data (called _sanitization_), a user might exploit such a tainted data flow to execute an unexpected and dangerous operating-system command, breaching system security.

This release of GNAT SAS includes built-in identification of key sources and sinks from the Ada runtime, the GNATcoll library, and key parts of the Ada Web Server (AWS). GNAT SAS will report on dangerous data flows from these identified sources, through your code, and to identified sinks. GNAT SAS reports dangerous data flows with full path information, so you can follow the data flow and determine whether it should be considered safe or a sanitizer should be applied. Each sink is associated with a CWE; the CWE identifier is used in reporting to help you identify the vulnerability and assess its impact more easily. CWEs covered by taint analysis include: 20, 22, 77, 78, 79, 89, 94, 200, 918.

Taint analysis is driven by new annotations that identify taint sources, sinks and sanitizers. These new annotations allow you to extend the analysis to your own code: simply annotate sources and sinks, and GNAT SAS will report on dangerous data flows.

For more information, see the GNAT SAS Users Guide.

Type state analysis ¶

GNAT SAS now offers type state analysis. Type state analysis spots problems that arise from incorrect adherence to API protocols, especially protocols that govern the use of resources. For example, a file resource should be opened once, read from or written to one or more times, and finally closed once. Opening a file multiple times, reading or writing from a file that has not been opened, or failing to close a file are all errors: they do not conform the protocol.

This release of GNAT SAS includes built-in type state analysis of the Ada.Text_IO API. Analysis is currently limited to within a given subprogram, but will be expanded to support interprocedural analysis will full path information in an upcoming release.

For more information, see the GNAT SAS Users Guide.

Parameter mode analysis ¶

GNAT SAS now reports when the use of a parameter in a subprogram is inconsistent with its specification. For example, if a parameter is marked in out but is never written, GNAT SAS will suggest that it be changed to in.

Aliasing between up-level variables and by-copy parameters ¶

GNAT SAS now reports on instances in which a global variable is modified directly from within a subprogram and also passed into the same subprogram as a pass-by-copy in out or out parameter. This situation is potentially dangerous and difficult to spot, as the pass-by-copy parameter will (silently) overwrite the value of the global that was set within the subprogam.

User interface ¶

GNAT Metrics integration ¶

GNAT Metrics can now be launched from the gnatsas tool using gnatsas metrics. All GNAT Metrics command-line options are suppored by this integration. Results from gnat metrics are output as before.

Improved performance of GNAT Check ¶

GNAT Check now executes rules up to 30% faster. On generic code, GNAT Check is up to 200% faster.

Introduce LKQL Rule Composition ¶

It is now possible to combine multiple LKQL rule sets with the new combine method. This lets users compose multiple LKQL rule file when using this in conjuction with the import statements. This makes LKQL rule file features equivalent to the legacy rule option format.

Qualification of the new LKQL Rule File Format ¶

The LKQL Rule File Format is now part of the GNATcheck qualification kit.

GNATcheck text report now displays each message’s category ¶

The GNATcheck text report now categorizes each message by prefixing it with appropriate identifiers to specify whether a message is a rule violation, a warning, or an error.

Libadalang 26 Release Notes ¶

We present here a few highlights of the new features in Libadalang 26. You can access the complete list in the Libadalang 26 feature file.

New properties ¶

Unified failsafe cross-reference properties ¶

This change unifies the P_Failsafe_Referenced_Decl and P_Failsafe_Referenced_Defining_Name into a single property named P_Failsafe_Referenced_Decl, and returns a data structure combining the information from the two previous properties: the precision of the result, the referenced declaration, and the specific defining name that is referenced.

Add property `is_abstract_type`¶

Add a property on BaseTypeDecl that returns whether the type is abstract or not.

Add `is_statically_constrained` properties ¶

These new properties can be used on BaseTypeDecl, TypeExpr, and ObjectDecl nodes, to know whether a type/subtype is statically constrained (and therefore, statically sized).

New properties for interpolated strings ¶

This change introduces two new properties for interpolated strings. Let’s consider the interpolated string Str below:

I   : Integer := 1;
J   : Float := 1.0;
Str : String := f"I: {I}, J: {J}";

First, FormatStringTokNode.p_denoted_value allows the user to get the string literal corresponding to a string token of an interpolated string chunk. In Str there is three FormatStringTokNode nodes:

"I: {",

"}, J: {",

and, "}".

Calling p_denoted_value on them will return:

'I: ',

', J: ',

and, ''.

Second, FormatStringChunk.p_image_subprogram can be used to get the Image subprogram that will be called to put the interpolated string’s chunk expression image. Here, Libadalang will return the Image subprograms defined in the Standard package for the types of I and J expressions, which are respectively, Integer and Float.

Target-aware Standard package ¶

Libadalang now takes into account target information to synthesize a coherent Standard package. This allows performing correct name resolution on attributes that depend on target information, such as Standard‘Max_Integer_Size.

Usability ¶

Support for rewriting in LAL ¶

Libadalang now offers public APIs that enable rewriting of Ada code. See chapter 6.6.8 of Libadalang’s documentation for more information.

Correctness improvements in generic code ¶

Name resolution correctness inside generic instantiations has been heavily improved.

Optimizations ¶

Optimize logic for determining ghost code ¶

This change optimizes the number and the nature of the queries performed internally by Libadalang to determine whether a given statement is ghost code or not. In particular, for a call to a procedure declared in a specification unit, determining whether the call is ghost or not will never trigger parsing and analysis of its corresponding body unit, whereas it previously did. Hence, performance and memory footprint are both improved.

Performance improvements in generic code ¶

Name resolution inside generic instantiations has been completely reworked to share resolution results across all instances. This leads to significant performance improvements when resolving all names in a project.

Performance improvements of the unparser ¶

The unparsing engine has been made faster and use less memory, allowing it to format big codebases in a reasonable amount of time.

orphan:

SPARK 26 Release Notes ¶

We present here a few highlights of the new features in SPARK 26. You can access the complete list here.

Language Extensions ¶

Multiple Levels of Ghost Code ¶

SPARK now offers multiple levels of ghost code. Ghost entities, assertion expressions, and specification pragmas can be associated with named assertion levels. Assertion levels, defined using the Assertion_Level pragma can then be enabled or disabled through an Assertion_Policy pragma.

Two levels of ghost code are predefined: Runtime and Static. Ghost code marked Runtime is always enabled; ghost code marked Static is never enabled.

Assertion Levels for SPARKlib Containers ¶

The SPARK library introduces several assertion levels that are used in the container libraries.

The assertion level SPARKlib_Defensive` allows enabling preconditions on container operations. This level is useful in particular if these operations are called from unproved code.

The assertion level SPARKlib_Logic` is for models of formal containers. It can be enabled in the full runtime. In the light runtime, it is also used for the ghost versions of the big numbers library and functional Containers library. As these libraries require finalization, the assertion level SPARKlib_Logic` cannot be enabled in the light runtime.

New Program_Exit Aspect for Abrupt Program Termination ¶

SPARK now offers a new Program_Exit aspect for specifying that the subprogram will terminate the whole program abruptly. The boolean expression given with this aspect, if any, shall be true when the program is terminated, which permits reasoning about intended program termination.

New Exit_Cases for Termination Conditions ¶

SPARK now offers a new Exit_Cases aspect for specifying subprogram termination conditions.

A subprogram can terminate by returning normally, by propagating an exception or by abruptly terminating the program. If a subprogram does not always terminate normally, then it can be annotated with an Exit_Cases aspect. This aspect allows partitioning the input state into cases and specifying for each case what the expected termination kind is:

Normal_Return, the subprogram shall return normally;

Program_Exit, the subprogram shall abruptly terminate the program;

Exception_Raised, the subprogram shall raise an (unspecified) exception; or

(Exception_Raised => E), the subprogram shall raise the exception E.

Support for Invalid Values ¶

SPARK now supports invalid values via a new Potentially_Invalid aspect. The Potentially_Invalid aspect can be used to annotate standalone objects, subprogram parameters, function result, and instances of Ada.Unchecked_Conversion to specify that they might have values that do not abide by the constraints of their type. A validity check is introduced whenever such objects are evaluated. The ‘Valid and ‘Valid_Scalars attributes can be used to assess their validity both in the code and in contracts.

Support for the finally Construct ¶

SPARK now supports the finally` keyword, a GNAT extension, which makes it possible to have a sequence of statements be executed when another sequence of statements is completed, whether normally or abnormally.

User Experience ¶

Success Message After Full Verification ¶

Previously, when all checks were proved (or annotated), GNATprove exited quietly with no explicit success message. Now, SPARK outputs a success message and prints the number of checks that were proved.

Support for Generics when Using –limit Switches ¶

Similar to the –limit-subp switch, the switches –limit-line and –limit-region now also support prefixing the location by a generic instantiation. The same is true for locations specified in a file passed to the –limit-lines switch.

No Resource-Leak Checks in Nonexecutable Ghost Code ¶

Taking advantage of the new support for multiple levels of ghost code, GNATprove no longer emits checks for resource leaks inside assertion pragmas, specification aspects, and ghost code that is associated with an assertion level that cannot be enabled at run time.

Warning Management via the Command Line ¶

In addition to the existing warning management capabilities, such as pragma Warnings and the –warnings switch, GNATProve now supports three switches -W, -A and -D, which allow users to enable warnings, suppress them, and promote them to errors, respectively. This can be done for predefined warning categories, which are identified by names appended to the warnings by default.

SARIF Output ¶

GNATProve now generates a gnatprove.sarif file at the same location as the gnatprove.out file that contains a summary of the run in SARIF format.

Improved Message with the –info Switch ¶

Previously, the –info switch could be used to enable a number of additional info messages, mostly related to proof. Now, a small number of these messages have been enabled by default (the messages related to inlining and loop unrolling), and the other info messages have been promoted into warnings that are disabled by default. Being warnings, they can be controlled by the -A, -W and -D switches and pragma Warnings (Off). The –info switch remains available to enable these warnings collectively.

Revised –no-global-generation Switch Behavior ¶

In previous versions of SPARK, the –no-global-generation switch prevented flow analysis from automatically generating Global contracts for subprograms without explicit global contracts. In this version of SPARK, the –no-global-generation switch has been modified to emit warnings when non-null Global contracts are generated for a subprogram with no explicit Global contracts. This change improves the stability of the feature, making it usable in more contexts.

Improved Documentation of Proof Limitations ¶

The section on proof limitations in the SPARK User’s Guide has been extended to include cases where the verification might fail due to the tool imprecision. The GNATprove tool has also been extended to detect more of these cases and to emit warnings when the –info switch is used.

Incompatible Changes in the SPARK Library ¶

Renaming of Insertion Primitives in Formal Vectors ¶

Similarly to Ada standard containers, the Containers.Formal.Vectors and Containers.Formal.Unbounded_Vectors packages of the SPARK library provide versions of the Append, Insert, and Prepend primitives taking a vector as a new item. These primitives have been renamed Append_Vector, Insert_Vector, and Prepend_Vector to match what has been done for the standard vector packages of Ada.

Simplification of Reference Function in Formal Containers ¶

The mode of the first parameters of the Reference functions declared in the Containers.Formal.Vectors, Containers.Formal.Doubly_Linked_Lists, Containers.Formal.Hashed_Maps, and Containers.Formal.Ordered_Maps packages of the SPARK library has been modified to simplify its usage. It is now an aliased parameter of mode IN OUT instead of an access parameter.

Similarly, the mode of the first parameters of the Reference functions declared in the Containers.Formal.Unbounded_Vectors, Containers.Formal.Unbounded_Doubly_Linked_Lists, Containers.Formal.Unbounded_Hashed_Maps, and Containers.Formal.Unbounded_Ordered_Maps packages of the SPARK library is now a parameter of mode IN instead of an access parameter.

Change in Generic Instances for Models of Formal Containers ¶

The actual parameter supplied for equality over elements of functional sequences and maps has been changed in the generic instances introduced for the various models of all formal containers. It is now the user-supplied equality function over keys or elements instead of a non-executable function standing for the logical equality. It makes it possible to enable these ghost models at run time, but it changes the meaning of comparison operators ("=", "<=", and "<") over these models, since they make use of this equality function. This change cannot modify the execution of a SPARK program in any way, as this is non-executable ghost code. However, it might affect the provability of user code if it uses these operators in its contracts. The ghost functions Equal, and Equal_Prefix on sequences, and Equal and Elements_Equal on functional maps are used as a replacement for these operators in the contracts of the container library so as to avoid degrading provability. User code might need to be changed in a similar way.

Executable Ghost Code in Containers ¶

It is now possible to execute most preconditions in the functional and formal container library. Ghost models in the formal container library are also executable in the full runtime. As a result, enabling all assertions and ghost code, for example using -gnata, now has the result of enabling these preconditions and ghost models as well. It is possible to disable them globally by adding pragma Check_Policy (SPARKlib_Defensive => Ignore); and pragma Check_Policy (SPARKlib_Logic => Ignore); to the global configuration switch of the user project.