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. 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.2. More detailed feedback on proof failures

SPARK will provide additional output in cases where the underlying provers stop because they have reached their memory limit or timeout.

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 annotations for non-blocking subprograms

SPARK will offer a SPARK-specific annotation that designates a subprogram as non-blocking.

2.1.8. 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.9. 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.10. Support limiting analysis to a generic instance inside GNAT Studio

SPARK will allow the user to limit the analysis to a specific generic instance when working inside of GNAT Studio. Currently, this capability is offered only via the command line.

2.1.11. 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*.

2.1.12. SPARK_Mode support for static Boolean expressions

SPARK will support static Boolean expressions in the SPARK_Mode pragma. This will allow the user to enable / disable SPARK_Mode using, e.g., a qualifier from a GPR file.