GNAT Static Analysis Suite 25 Release Notes¶

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

More precise analysis ¶

Handle record initialization more precisely ¶

Record initialization is now always handled precisely in Inspector analyses. Before this improvement, record initialization was treated imprecisely when the file containing the record declaration and the file where a record was initialized ended up in different partitions: the fields of the record were treated by Inspector as fully initialized. Now, the record initialization function is used in each partition. This improves precision when the analysis is run in fast mode or on a single file, but potentially also in deep mode.

Improve precision of `use_for_of_loop` rule ¶

Prior to this change, this GNATcheck rule processed record component accesses very imprecisely, basically considering that X.Component (I) and Y.Component (I) were designating the same memory location no matter the context, which could introduce false positives. This change improves precision in that regard, by first checking whether the prefix of these accesses represent the same memory location.

Improved analysis of arrays and pointers ¶

The Inspector component of the GNATSAS static-analysis suite has been enhanced to provide a more precise, sound analysis of algorithms using array indexing and pointer dereferences. This new analysis is based on the notion of a “value history” that is maintained for each group of objects or object components that are mutually aliased, and tracks precisely all of the operations that might affect any member of a given aliasing group.

Handling uninitialized data ¶

Detection of uninitialized out parameters by Infer ¶

The Infer analysis backend is now able to detect an access to an uninitialized out parameter, even when it is of a record type. For an out parameter of an elementary type, Infer is also able to detect when it is not initialized at the end of a subprogram.

New analysis for initialization within Infer ¶

We have introduced a new Infer analysis to detect that values are properly initialized before being accessed. Currently, this analysis operates on an intraprocedural level, meaning that it does not track uninitialized data across subprogram calls. Instead, it assumes that any data potentially modified by a subprogram call is initialized. This new analysis has a broader scope, as it explores all execution traces, resulting in more messages about potential initialization errors. It has the capability of detecting issues that were previously overlooked, offering more systematic error detection. Infer is now running both analyses; the previous one emits messages with a high ranking while the new one generates medium messages.

Improved tracking of uninit record fields by Infer ¶

Infer is now able to track uninitialized record fields when copying records. As a result, it is able to better detect uses of uninitialized record fields.

Handling Ada constructs ¶

Improved handling of ‘for of’ loops on arrays ¶

The Infer backend for GNAT SAS now correctly understands the Ada “for of” iterator construct for arrays.

If_expressions support in redundant-Booleans rule ¶

The GNATcheck ‘Redundant_Boolean_Expressions’ rule now flags if_expressions as violations when they contain a redundant Standard.Boolean literal.

User interface ¶

No extra runtime needed ¶

GNATcheck can now run with the GNAT SAS runtime and use it by default. This allows users to run GNATcheck without another installed Ada runtime.

Extend support for filtering with –show ¶

Filtering with the “–show” switch is now supported for the GNAT Studio and HTML report formats. While the typical use case is that filtering is done directly by the user through filtering capabilities of GNAT Studio or WebUI (for the HTML report), adding this capability allows users to pre-filter the set of messages that will be available for GNAT Studio or WebUI. This can be useful in cases where there is a large number of messages or where the user wants to specifically view a subset of the messages without a strong need for dynamic filtering.

Displaying information about timelines ¶

A new –list-timelines switch is added to all GNAT SAS commands. The switch provides a short list of the available timelines for the project specified with -P, followed with additional information about each timeline, such as the date of the last analysis run, the date of the baseline, the names of the corresponding SAM files, and the command-line and project switches that were used during the analysis.

Allow classic and LKQL rule files for the same run ¶

You can now provide classic (“+R” style) and LKQL rule configuration files for the same GNATcheck run. This will combine the rules specified in each file.