Introduction

2025 is a new year of growth for the GNAT Pro family to help people develop safe, secure, and efficient code on a large variety of software and hardware platforms.

Check our live website documentation for more details about the GNAT Pro 25 release. If you are interested in what's next, the public roadmap for AdaCore products is available on our documentation platform.

New platforms

New software frameworks

The GNAT Pro 25 release introduces significant upgrades to enhance developer productivity and code quality. GCC-based compilers have been updated to GCC 13, offering improved warnings, optimizations, and support for the latest C23 and C++23 features. Additionally, compilers for Linux Arm 64-bit native platforms are now part of the GNAT Pro suite.

The set of LLVM-based compilers continues to grow, with the addition of GNAT Pro for Windows native platforms now available with the LLVM backend. The release also includes a Rust development environment for both Linux and Windows, extending the reach of GNAT Pro into modern systems programming.

New targets

On the cross-platform front, GNAT Pro 25 expands support with LLVM-based compilers for Arm 64-bit, targeting both bare-metal environments and cross-Linux platforms. These targets also include Rust support, providing developers with versatile options for building secure and efficient applications.

FreeRTOS, a widely used real-time operating system for microcontrollers and small processors, is now supported by GNAT Pro 25. This addition enables developers to build small-footprint embedded systems with Ada, catering to the growing demand for resource-efficient IoT and embedded applications.

GNAT Pro 25 also delivers enhanced support for bare-metal Morello platforms, advancing memory safety in modern systems. Arm Morello, featuring Capability Hardware Enhanced RISC Instructions (CHERI), offers fine-grained memory protection and hardware-level compartmentalization. The updated GNAT Pro GCC and LLVM bare-metal Ada runtimes introduce automated CHERI pure-capability memory allocators and innovative security features, enabling developers to adopt new security-by-design paradigms for systems development.

This release reaffirms GNAT Pro’s commitment to empowering developers with cutting-edge tools and platforms to tackle the challenges of safety-critical and high-integrity software.

Lightweight finalization

The GNAT Pro compiler continues to evolve, introducing new capabilities that simplify and enhance the developer experience, particularly for safety-critical embedded systems. One notable addition in GNAT Pro 25 addresses the complexities of controlled types in Ada.

Controlled types in Ada allow developers to define custom initialization, finalization, and assignment operations for objects, offering valuable flexibility. However, this capability often introduces significant complexity and runtime overhead, which can be prohibitive in embedded systems.

To address this, GNAT Pro 25 introduces a new implementation using the Finalizable aspect. This feature enables initialization and assignment operations to function similarly to controlled types but simplifies the semantics of finalization. The finalization procedure is invoked only when an object goes out of scope (for stack-allocated objects) or is explicitly deallocated (for heap-allocated objects). This eliminates the need to track heap-allocated objects, improving simplicity, efficiency, and predictability.

Moreover, the Finalizable aspect removes a key design constraint by allowing it to be applied to any record type, not just tagged types.

This flexibility opens up new design possibilities for developers working on resource-constrained systems. For example, creating a smart pointer (a pointer that automatically deallocates the referenced object when it is no longer needed) becomes straightforward. Here's how it can be defined:

The Initialize, Adjust, and Finalize procedures for the smart pointer type are designed to manage memory efficiently. Memory is allocated on the heap when a reference to the object is first declared and is automatically deallocated when no references remain. The use of Relaxed_Finalization further simplifies this process by eliminating the need for special exception handling in finalizers, reducing the complexity of the finalization infrastructure.

As demonstrated in the example, allocation and deallocation of objects are handled automatically, ensuring seamless memory management.

This approach significantly reduces the execution overhead associated with tracking object lifetimes, making it a practical and efficient solution for resource-constrained embedded systems.

Binding generation

GNAT Pro 25 introduces powerful binding-generation technology designed to streamline interoperability between Ada and C. The tool, h2ads, parses C header files and generates Ada package specifications that correspond directly to the header content. This process creates a thin binding—an Ada specification that is binary-compatible with the original C declarations—enabling seamless calls from Ada to C library subprograms.

The binding generation process accounts for the underlying compiler, incorporating standard header searches and compiler-defined macros. For instance, types like size_t are correctly mapped to different Ada types depending on whether a 32-bit or 64-bit compiler is used, ensuring compatibility across platforms.

Looking ahead, we are developing a more advanced multi-language binding technology to facilitate interoperability among Ada/SPARK, C++, and Rust. This will introduce thick bindings through a proxy/hourglass model, creating wrappers for different languages around a shared internal representation. This approach will enhance cross-language integration while maintaining type safety and performance, empowering developers to work efficiently across diverse programming ecosystems.

Rust

Rust is one of the fastest-growing programming languages, celebrated for its performance, safety, and modern features. AdaCore is committed to supporting the high-integrity software community by developing a robust Rust ecosystem tailored to their demands for stability, security, long-term support, and certifiability.

With GNAT Pro 25, developers gain access to native Rust compilers for both Linux and Windows, as well as Rust cross-compilers targeting Arm 64-bit platforms. These include support for bare-metal environments and cross-Linux development, broadening Rust’s applicability in critical embedded systems.

Our roadmap focuses on advancing Rust’s capabilities for high-integrity applications. Key initiatives include certifying language libraries (such as a subset of libcore), conducting source-to-object traceability studies, qualifying the Rust compiler, and introducing code coverage analysis tools that support standards like MC/DC. These efforts ensure Rust can confidently address the rigorous requirements of safety-critical and secure systems.

Static analysis

GNAT SAS continues to enhance the precision of its analysis while expanding its coverage of critical software vulnerabilities identified in the Common Weakness Enumeration (CWE) list.

The tool integrates seamlessly with popular continuous integration frameworks like Jenkins and GitLab, streamlining its adoption in modern development pipelines. Its reports are compatible with widely recognized formats, including the Static Analysis Results Interchange Format (SARIF) and Code Climate, ensuring compatibility with a variety of commonly used viewers and tools for effective issue tracking and resolution.

Dynamic analysis

GNATtest was initially designed to automate the creation and maintenance of harness code and test skeletons. It can now also automatically generate test inputs based on the structure of subprogram parameters, using the option --gen-test-vectors.

Testing a sort algorithm like the following:

GNATtest can automatically generate tests to cover the implementation. When invoked with the switch --minimize (to minimize the generated testsuite), it will create two test cases: one with an empty array and another with an unordered array.

Note that the postcondition is good enough to ensure that the result is correct, and putting everything together means that you can write your complete unit testing campaign without writing a single line of code!

GNATfuzz extends the capabilities of traditional unit testing by uncovering unexpected vulnerabilities that conventional methods can miss. In the 25 release, GNATfuzz supports a wider range of subprograms and parameter types, bolstered by the integration of the symbolic execution engine, SymCC. This advanced engine solves complex branch conditions, significantly increasing test coverage and enabling deeper exploration of the codebase.

I tested GNATfuzz on an implementation of the floating-point sine function using Hart’s approximation, which has a cyclomatic complexity of 22. Within moments, it generated a set of eight test cases that fully covered the implementation. More impressively, it identified a subtle vulnerability in the code that triggered an exception, an issue that would have been extremely challenging to uncover through code review alone.

GNATfuzz and GNATtest now complement each other by sharing test inputs in a unified JSON format. This integration allows GNATfuzz to use GNATtest's unit-test campaigns as an initial input corpus, while GNATtest benefits from GNATfuzz-generated test cases to improve code coverage. This synergy enhances the overall effectiveness of both tools.

Talking about code coverage, GNATcoverage introduces new flexibility. Users can now disable coverage analysis for specific regions using Ada pragmas or C/C++ comment markers. It indicates regions where coverage analysis is fully disabled (similar to a no-code region).

For scenarios where source modifications are undesirable, GNATcoverage 25 also supports companion annotation files. These files provide the same annotation capabilities as direct source modifications, enabling fine-grained control over the instrumentation process without altering the original code.

Enhanced libraries and precision in SPARK

SPARK 25 introduces new SPARK-compatible libraries to broaden its utility and flexibility. The Ada.Strings.Unbounded package now includes a complete set of contracts, building on the robust implementations already available in Ada.Strings.Fixed and Ada.Strings.Bounded. Additionally, a new SPARK-compatible library of wrappers for Interfaces.C.Strings has been added to SPARKlib as SPARK.C.Constant_Strings, making it easier to work with constant C-style strings in a safe and verifiable manner. The Ada.Generic_Elementary_Functions package also benefits from newly added Global contracts, improving its compatibility with SPARK's rigorous verification model.

SPARK 25 also enhances the analysis of low-level code, providing more precise handling of critical constructs like Ada.Unchecked_Conversion. These conversions are now checked to ensure they cannot generate invalid values and consistently produce the same result for identical inputs. The analysis verifies that the source and target types have the same size, while accounting for type alignment and representation data generated by the compiler for the specified hardware target. This includes checks on bit patterns in representation clauses for both the source and target types, ensuring safe and predictable behavior even in low-level programming scenarios.

Conclusion

This post highlights some of the exciting new capabilities coming to GNAT Pro in current and future releases. For a more comprehensive view of AdaCore's plans, including long-term developments, refer to the publicly available roadmap for AdaCore products.

We encourage AdaCore customers to explore the upcoming GNAT Pro releases and reach out with any questions about their features and tools. Your feedback is invaluable, let us know what you enjoy and share your suggestions for enhancing the AdaCore ecosystem.