- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jul 27th, 2012
Serial port flow control setting support
GNAT.Serial_Communication.Set now allows the specification of no flow control, hardware (RTS/CTS) flow control, or software (Xon/Xoff) flow control. The default is no flow control. Note that for Linux, the previous behaviour was to always enable RTS/CTS flow control. This must now be specified explicitly if desired. On Linux, the CLOCAL flag (ignore all modem control signals) can also be specified.
Jul 26th, 2012
Efficient handling of packed 2-D arrays
Aggregates with static components for packed matrices whose component size is 1, 2, or 4 are now handled fully by the compiler front-end and generate no elaboration code. Very large matrices (with more than 5000 components) can be handled by applying pragma Static_Elaboration_Desired to package.
GPS: Improvements to the GNATcoverage support
Several improvements to GNATcov support have been made:
- Modification of the Coverage preference is no longer required. - A new Build Mode "gnatcov" has been introduced. - New project attributes have been implemented to control the behavior of tools launched during the GNATcoverage development cycle. - The Coverage View is automatically reloaded after an analysis.
ECL: gprbuild use of cross compilers via makefiles
GNATbench for Eclipse now directly supports the use of makefiles and gprbuild to invoke cross compilers. The --target switch is passed to the makefile when invoked.
Jul 20th, 2012
Addition of SPARKSkein to SPARK Library
A new package, SPARK.Crypto, has been added to the SPARK library. The top level package contains basic type definitions. The child package SPARK.Crypto.Hash.Skein contains a SPARK implementation of the Skein secure cryptographic hash algorithm. The implementation has been proved free from runtime exceptions, and the proof artefacts are included with the code in the library. For more information see http://www.skein-hash.info.
Jul 19th, 2012
Large file support in POSIX binding on Linux
Florist, the GNAT implementation of the standard POSIX Ada binding, now supports access to large files (larger than 2 gigabytes, which was the previous limit).
Jul 19th, 2012
The Riposte counter-example generator
We will now ship Riposte (https://forge.open-do.org/projects/riposte) as an experimental feature as part of the next SPARK Pro release.
GB: Choice of Ada versions in New Project wizard
When using the New Project wizard to create GNATbench projects, the user can choose among the Ada 95, 2005, and 2012 revisions of the language.
ECL: Specific “Build Main” menu for each Main file
All units containing an application entry point appear in the Project's "Build Main" menu.
GPS: experimental Mercurial plugin
Experimental support for the Mercurial VCS has been added to GPS.
ECL: makefiles can now use gprbuild
When GNATbench for Eclipse project builds are driven by makefiles, the builder name is passed as a macro. In the past this builder name was always passed as "gnatmake" but it can now be set to "gprbuild" instead.
Jul 13th, 2012
Improved array proof in Simplifier
The internal rules for performing proofs involving arrays have been improved. This addresses a specific case where showing that two elements of an array have been swapped depended on the order in which the elements were given (when in fact the order makes no difference to the validity of the proof). Users may notice that some additional VCs are discharged by the Simplifier as a result of this change.
Jul 11th, 2012
User-defined indexing with multiple indices
The compiler now supports Ada 2012 user-defined indexing aspects that include more than one index, e.g. to model non-standard representations for matrices.
GB: Eclipse 3.8 and 4.2 (Juno) support
Eclipse 3.8 and 4.2 are supported by GNATbench 2.7.0 Note: Eclipse 3.8 requires JRE 1.6 (Java Runtime Environment).
Jul 9th, 2012
Aspects on subprogram bodies
The compiler now supports Ada 2012 aspect specifications that appear on subprogram bodies, including Inline, Priority, and CPU.
Jul 6th, 2012
Accept warnings relating to hide annotations
Previously, it was not possible to use the accept annotation to justify warnings relating to use of the hide annotation. This restriction has now been lifted. Users may wish to require that all uses of hide are justified in this way as part of their SPARK coding standard. Note that, due to grammar restrictions, if you wish to accept a warning regarding a hidden private part you must place the accept annotation before the word private.
GPS: Clear locations action for key shortcuts
GPS provides a new action to assign a key shortcut to the 'Clear locations' capability of the Locations View.
Support for PyGObject
PyGObject is the replacement for pygtk for more recent versions of gtk+. GNATCOLL is now able to detect it automatically (unless --disable-pygobject was specified) and use it when appropriate. This provides support for gtk+ in the python interface.
Support for gtk3
A new configure switch (--with-gtk) was added to specify which version of gtk+ should be detected. It replaces --disable-gtk, which has been removed.