- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jul 30th, 2015
Generated Initializes contracts
The tools now internally generate Initializes contracts for packages that do not have user-provided Initializes contracts. This reduces the false alarm rate about uninitialized uses of variables.
Jul 29th, 2015
Support for all kinds of type predicates
The SPARK tool now handles all kinds of type predicates, in particular static predicates on floating-point types and dynamic predicates on any type. A dynamic predicate check is generated at every program point where the predicate associated to a value might be violated.
Avoid unprovable LSP checks on untagged private
Visible primitive operations of untagged private types whose full view is tagged previously lead to unprovable checks related to the verification of Liskov Substitution Principle, as Pre'Class cannot be specified on such operations. Dispatching on such subprograms is now forbidden in SPARK and LSP checks not needed anymore on such subprograms as a result.
Better support for quantification with Iterable
The SPARK proof tool now handles quantification using the Iterable aspect better, especially when cursors are record or private subtypes.
Jul 23rd, 2015
Summary table for proved and unproved checks
The gnatprove output file "gnatprove.out" now contains a summary table which summarizes the verification results. It shows the number of proved checks, to which category they belong (like initialization checking, runtime errors, or functional contracts) and how various provers contributed to it. Unproved checks are also counted.
Jul 22nd, 2015
Style checks for record components
Style checks now apply to the alignment of record component declarations.
Jul 16th, 2015
Scalar_Storage_Order and Complex_Representation
The Scalar_Storage_Order attribute now works in conjunction with record types subject to aspect/pragma Complex_Representation.
Jul 15th, 2015
Create_Temp_File now using mkstemp on Android
GNAT.OS_Lib.Create_Temp_File now uses mkstemp instead of mktemp to create the temporary file. The former is considered a safer alternative that avoids all possible race conditions when creating the temporary file.
Symbolic tracebacks on unhandled exceptions
When a program is terminated by an unhandled exception, the information in Exception_Information is printed, which can include a symbolic traceback. See NF-74-J408-043 for how to enable such symbolic tracebacks.
Symbolic tracebacks in Exception_Information
The Exception_Information can now include a symbolic traceback when available. It is available on native platforms that use DWARF-format debugging information, which includes Linux, Windows, Solaris, FreeBSD, and AIX. To enable this feature, use the gcc switch "-g" and the binder switch "-Es", as in "gprbuild -g ... -bargs -Es".
Jul 13th, 2015
Better error reporting with premature instantiation
When a package is instantiated before its body is seen, the compiler creates a dummy body for it to complete the compilation. The dummy function bodies created within the package bodies have no legal return statements, but no cascaded error should be generated for these.
Jul 13th, 2015
Membership tests in tagged type hierarchy
The GNATprove tool now supports testing for membership of an expression in a tagged type hierarchy.
Jul 10th, 2015
gnatname -P now invokes gprname
As the project support is phased out of the GNAT tools, a new GPR tool gprname has been introduced to replace "gnatname -P" and "gnatname -P" will silently invoke it for now.
Jul 9th, 2015
Better support for if expressions on real types
The SPARK proof tool now handles if expressions better, which results in more automatic proofs on programs using if expressions, especially when they have a floating point type.
GPS: new plugin closeold
A new optional plugin is provided. It automatically closes the least recently accessed editors when new editors are opened, thus limiting the number of opened editors to a maximum limit. Editors can be pinned to prevent their automatic closing.
Jul 6th, 2015
New tool gprname
A new GPR tool, gprname, is now available. It is the replacement of "gnatname -P".