Product Roadmap

The GCC back-end of GNAT Pro will migrate to GCC-15.

The LLVM back-end of GNAT Pro will support 32-bit Linux and Windows.

The LLVM back-end of GNAT Pro will migrate to LLVM 21.

GNATcoll is a library of Ada capabilities. It will be ported to VxWorks 7 on all supported architectures.

GNAT Pro Ada will support 64-bit Arm Android targets.

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

Add support for Ada compilation on 32-bit x86-Windows using LLVM

GNAT Pro will include shared and static position-independent Ada runtimes for use with the LLVM back-end.

Support C compilation on 32-bit x86-Windows using LLVM

GNAT Pro for Rust will support Rust 1.93.0

GNAT Pro for Rust will support 32-bit Arm bare-metal as a no-std target. This new cross target is available on x86_64 Linux hosts.

GNAT Pro for Rust will support Rust debugging on VxWorks targets using vxlink and vxgdb, offering a seamless debugging experience for Rust developers.

Libtest-based testing will be available for no-std targets. This will make no-std embedded development much more similar to native Rust development, reducing development costs.

Rustc will generate coverage information up to and including Modified Condition / Decision Coverage (MC/DC). This support will integrate seamlessly with GNATcoverage, allowing Rust to be used for safety-critical software development at the highest levels.

All the CI/CD tool integrations will be included in the CodeSonar installation. This will make it easier for your tools administrator to find the integrations and configure your DevSecOps pipeline.

Analyze your Android code against the latest version.

CodeSonar will check C++ code for violations of all MISRA C++:2023 coding guidelines developed by the Motor Industry Software Reliability Association. The MISRA C++:2023 helps teams write C++ that is safer, more portable, and more maintainable, particularly where failure has serious consequences.

Enjoy the efficiency and cost-effectiveness of algorithmic static analysis with the power of an AI assisted workflow. We will be adding annotation and tool administration tasks to our powerful remediation and explanation capabilities.

GNATcoverage will be able to filter the report given a specific origin (e.g. report only coverage for a specific test).

GNATcoverage support of non-gpr build systems such as make and cmake will be expanded to include Windows hosts and cross-compilation configurations.

GNATcoverage will no longer re-generate instrumented sources which have not changed and for which the dependencies have not changed, thus improving incremental instrumentation and build times.

The integrated instrumentation process, which produces a wrapper to be used seamlessly instead of the original compiler in the build system, will support cross-target configurations and windows hosts.

GNATcoverage will allow defining of exemptions of specific conditions, outcomes, or branches of a decision when full MC/DC coverage cannot be achieved.

The GNATfuzz Adaptive Fuzzing Engine extends on-target fuzzing to hardware platforms that are typically unsupported by traditional fuzzing engines.

GNATfuzz will be re-shaped into a set of atomic commands
for greater modularity, which benefits power users who
need specific fuzzing setups.

GNATfuzz will be seamlessly integrated into Continuous
Integration (CI) and Continuous Delivery (CD) workflows.

GNATfuzz will fully support the automated fuzzing of C applications.

This feature will be made available as beta, not intended for production.

GNATfuzz was initially implemented for x86_64 Linux. It will be ported to x86_64 Windows.

Improved stability of the fuzz-everything workflow

The Hot-Spot workflow bridges the gap between static and dynamic analysis by using GNATfuzz to automatically validate SARIF reports (like those from GNAT SAS and SPARK).

GNATfuzz will integrate libFuzzer, a highly efficient, in-process fuzzing engine to its existing suite of fuzzing engines (AFL++, CmpLog, and SymCC). This enables the use of GNATfuzzer with GNAT Pro and LLVM.

GNATtest will be able to produce a test report in xUnit format, facilitating integration of GNATtest within CI/CD environments.

GNATtest will support ingesting external files describing full test case scenarios, including test inputs for the subprogram under test, expected outputs, and possibly stub configurations if applicable.

GNATtest will have support for stubbing subprograms imported from another language, such as thin bindings

GNATtest will be able to generate test reports in the jUnit format, allowing simpler integration within CI/CD environments

Limited support for test generation and test serialization for access types and class-wide tagged types will be available.

SPARK will allow calls to functions with side-effects in more contexts. In particular, it will be possible to call functions with side-effects:

• in the conditions of if statements and elsif branches;

• in case statements; and

• in return statements.

SPARK developers will be able to use the Finalizable aspect, a GNAT extension, to specify that a record type provides the same level of control on the operations of initialization and finalization of objects as the controlled types. Since controlled types remain unsupported in SPARK, developers will be able to implement automated reclamation for their record types.

In SPARK's modular analysis, an in/out parameter of or global modifed by a called subprogram is assumed to be completely and unconditionally modified by the call; developers must therefore state explicitly everything that is not modified and when, whenever greater precision is desired.

In the Modifies aspect, developers will be able to state when a parameter or global is modified and which parts, for composite types. For example:

   type R is record
      F1, F2 : Boolean;
   end record;
   type RR is record
      G1, G2 : R;
   end record;

   procedure Write_G1_F1 (B : Boolean; X : in out RR) with
     Modifies => X.G1.F1 when B;

   procedure Write_G1_F1 (B : Boolean; X : in out RR) is
   begin
      if B then
         X.G1.F1 := False;
      end if;
   end Write_G1_F1;

Objects that share the same underlying memory region are referred to as overlays. SPARK will handle these objects precisely, in simple cases. As an example, we will be able to prove the following code:

with Interfaces; use Interfaces;
procedure Test with SPARK_Mode is
   type Four_Small_Ints is record
      F, G, H, I : Unsigned_8;
   end record;
   for Four_Small_Ints use record
      F at 0 range 0 .. 7;
      G at 0 range 8 .. 15;
      H at 0 range 16 .. 23;
      I at 0 range 24 .. 31;
   end record;
   
   X : Unsigned_32 := 256;
   Y : Four_Small_Ints with Import, Address => X'Address;
begin
   pragma Assert (Y = (0, 1, 0, 0));
end;

This feature will help to enable zero-copy provable parsing of binary data into simple record types.

Ada provides array component iterators and container element iterators using the for .. of syntax, which yields cleaner loop bodies than for .. in without the need to capture the current element in a constant declaration inside the loop. However, since SPARK uses induction to prove loops, for .. of generally cannot be used as the loop index is typically required for induction.

SPARK and Ada will offer a new attribute 'Loop_Index that allows the current loop iteration to be retrieved from array component or container element. This allows induction to be performed while using for .. of.

For example, it will be possible to write:

   for E of S loop
      if E = 0 then
        C := C + 1;
      end if;
      pragma Loop_Invariant (C <= E'Loop_Index);
   end loop; 

where previously the loop would have required for .. in, instead, to establish the bound on C using induction.

SPARK (and Ada) developers will be able to use 'At refer to the value of an object at a previous program point. Currently, Ada provides 'Old and 'Loop_Entry, which allow the initial value of a subprogram parameter or the initial value of an object at the time a loop was entered to be referenced, respectively. Using 'At, a developer will be able to refer to the value of an object at a specific label, like this:

X := 1;
<<My_Label>>
X := 2;
pragma Assert ((X-1)'At (My_Label) = 0);

which is equivalent to

X := 1;
declare
   Compiler_Generated_Unique_Name : constant Integer := (X-1);
begin
   X := 2;
   pragma Assert (Compiler_Generated_Unique_Name = 0);
end;

Access-type conversions, like overlays, can be used to reinterpret a value of a given type as a value of another type. This is especially useful for providing a typed reinterpretation of binary data with zero copies. While overlays provide an effective means to accomplish this within a subprogram, access-type conversions allow the resulting typed reinterpretation to be exported for use by the rest of the program.

SPARK will support access-type conversions safely via the SPARKlib. The result of the conversion is a borrow or an observe.

SPARK will provide information about why its provers stopped working on unproved checks.

Broadly speaking, provers stop working checks for one of two reasons:

1. The provers reached configured resource limits. SPARK limits its provers with timeouts, step limits and memory limits. If a prover stopped working because a given limit was reached, increasing that limit might result in a proved check.

2. The provers stopped working on the check even though resource limits were not reached. SPARK's provers have internal heuristics that sometimes cause the provers to stop work early. This does not necessary mean the check is proved false; it does mean that increasing timeout or step limit, for example, will not help.

SPARK will provide this information via new information appended to the check message:

• [provers reached <limit> limit before completing the proof], where <limit> is one or more of time, step, and memory (e.g. [provers reached time and step limit before completing the proof]), or

• [provers gave up before completing the proof]

In both cases, following the guidance in the section "How to Investigate Unproved Checks" of the SPARK User Guide remains our strong recommendation.

SPARK will offer insight into whether a proved check was (re)proved by the solvers on the current run or served from a cache (local or file-based memcached). This can help explain situations in which SPARK results appear to be nondeterministic and can aid in debugging memcached-based CI deployments of SPARK.

The SPARKlib will provide formal and functional generic trees. Like the other containers in the SPARKlib, developers can use these containers in their code and prove properties about the containers and the elements contained therein.