- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jan 31st, 2017
New switch—no-inlining prevents inlining for proof
The special inlining used in GNATprove to increase the precision of proof may be harmful in some cases, as it increases precision at the cost of longer running time and greater memory usage. GNATprove now supports no inlining under switch --no-inlining.
GNATCOLL.SQL.SQLITE: support for URI filenames
Support for sqlite's URI filename has now been added, via a new parameter to GNATCOLL.SQL.Sqlite.Setup
GNATCOLL.Traces add support for prefix decorators
These decorators can be used to add information at the beginning of each log line, before the indentation and the name of the trace handle. Such information will always be aligned, so it might be convenient to display timestamps for instance.
Jan 25th, 2017
SPARK tools produce more information about VCs
Previously, it was hard to see which VCs were produced for a given check, and which prover was used to attempt to prove it. Now, this information is stored in the .spark files that are produced by GNATprove. The content of these files is now documented.
Jan 23rd, 2017
New lemmas on monotonicity of float operators
The SPARK lemma library includes six new lemmas on the monotonicity of the float addition, substraction, multiplication and division.
Jan 20th, 2017
Ability to check removal of Ghost code in executables
The names of Ghost entities in the objects and executables are now uniquely prefixed with "___ghost_" (three leading underscores). This makes it possible to independently check the removal of Ghost code by the compiler when generating the final executable with Ghost assertion policy of Ignore (the default).
Jan 18th, 2017
Better warnings for suspicious postconditions
Postconditions (and consequences of contract cases) that do not refer to the post-state of the subprogram are suspicious, as they should either be preconditions, or another expression was meant to be checked. Originally only full postconditions were checked, now all conjuncts in a conjunction of Boolean sub-expressions are individually checked for such issues.
Jan 17th, 2017
Relaxed and strict secondary stack management
The compiler now employs two different schemes of managing the secondary stack - relaxed and strict. In relaxed mode, a context which uses the secondary stack will no longer manage it if there exists an enclosing construct which already does that. This behavior cannot propagate beyond packages and subprograms. Relaxed mode is the default mode of secondary stack management. In strict mode, any context which uses the secondary stack will manage it unconditionally. This behavior can be enabled by switch -gnatd.s.
Jan 13th, 2017
Reduce -Wstack-usage false positives with strings
The number of false positives reported by the compiler for the -Wstack-usage warning on strings or arrays has been reduced.
Jan 12th, 2017
Check default of private types at declaration
GNATprove now checks that no runtime error can occur during the default initialization of private types once and for all at the declaration of the type. This enforces a cleaner separation of library code from user code, allowing for an easier integration of proof with other verification means (tests, review...).
Jan 9th, 2017
Do not emit unit version on bare board platforms
On bare board platforms, units versions for Version and Body_Version attributes are not emitted anymore when not needed.
Jan 6th, 2017
Support for arbitrary lengths of entry queues
GNATprove now supports arbitrary lengths of entry queues (which are specified by the Max_Queue_Length and Max_Entry_Queue_Length pragmas). This feature is only applicable when the GNAT Extended Ravenscar profile is active.
Add message on proved termination
When GNATprove is able to prove a Terminating annotation an info message is issued.
Support of caching using memcached server
The SPARK tools now support caching large parts of the analysis via a memcached server. If a memcached server is available to store analysis results, and this server is specified to GNATprove via the command line option --memcached- server=hostname:portnumber, then subsequent invocations of the tools, even across different machines, can store intermediate results of the tools. The user-visible effect is that GNATprove can produce results faster.
New GPRname switch—ignore-duplicate-files
GPRname has a new switch --ignore-duplicate-files which will ignore identical basenames when scanning for sources. In addition, a warning is now emitted by default when not using this switch to warn about potential conflicts when duplicate filenames are found.
Jan 3rd, 2017
Improved debug information for enumeration types
In its DWARF output, GNAT now generates DW_AT_encoding attributes for all DW_TAG_enumeration_type DIEs. These describe the signedness of the corresponding enumeration types, allowing precise interpretation of subranges.
Jan 2nd, 2017
No_Inline is a legal aspect name
The GNAT-specific pragma No_Inline is now accepted as a legal aspect name, in analogy with the Ada aspect No_Return.