2. AdaCore SPARK Pro 26 Roadmap

This roadmap represents the current stage of AdaCore plans for its technology. It is not binding, and can change without notice. Products marks as “Beta” can be made available to customers supported on the corresponding products by contacting AdaCore support (https://www.adacore.com/support). Customers interested in trying out capabilities that they don’t have access to yet, or who are interested in discussing a more detailed status update can contact info@adacore.com

2.1. SPARK

2.1.1. 64-bit ARM Linux Support

SPARK will be supported on 64-bit ARM Linux hosts.

2.1.2. Expanded Explain Codes

SPARK will offer expanded support for Explain Codes, focusing on issues most commonly reported by users over the course of the year.

2.1.3. Multiple Levels of Ghost Code

SPARK will allow multiple levels of Ghost code to be designated via user-extensible enumerated constants. SPARK will also allow execution policies to be associated with designated levels of Ghost code, allowing finer-grained control over which elements of Ghost code are retained at execution-time rather than being proof-only.

2.1.4. Notification of successful proof.

SPARK will provide an option whereby successful proof will be announced on the command line. Currently, successful proof is silent, resulting in no output and a zero exit status.

2.1.5. Output a SARIF document

SPARK will provide a SARIF-output option, facilitating its integration into IDEs and tools that support SARIF.

2.1.6. Support finally

SPARK will support the new finally block that was introduced as a new Ada feature in GNAT Pro 25.

2.1.7. Support contracts for early program exit

SPARK will support a new subprogram contract Program_Exit that will allow the user to describe the conditions under which the program will terminate early from within the given subprogram.

2.1.8. Support for invalid values

SPARK will offer a new aspect that designates a value that may be invalid. This aspect will be tracked via flow analysis.

2.1.9. Switch to suppress/enable warnings

SPARK will allow specific SPARK-specific warnings to be disabled or enabled via command-line switches, as GNAT does with -gnatw*.