- 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.
GNATCOLL.SQL: SQL_Parameter from Unbounded_String
Text parameters to SQL queries can now be set from an unbounded string, in addition to the existing support for String_Access. This can be more efficient in some cases.
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.
GNATCOLL.SQL: support for “between” SQL keyword
Support "BETWEEN" and "NOT BETWEEN" SQL syntax generation.
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.
install through gprinstall
The install is now done via gprinstall, instead of depending on complex shell commands in the Makefiles. This makes the system more robust, allows uninstalling and will work better on Windows machines.
UNIQUE keyword in database schema description
The unique constraints and indexes could be defined in the SQL database schema description file.
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".