[GAP] Announcing the immediate availability of GNAT and SPARK GPL 2015

[Jamie Ayre]

Dear GAP member,

We are pleased to announce the availability of the GNAT and SPARK GPL 
2015 toolsets.

GNAT GPL 2015 includes support for the Raspberry Pi 2 allowing Ada 
development using all Ada features on this popular educational computer
running embedded Linux.

GNAT GPL 2015 incorporates upgraded technology for the back end 
(GCC 4.9) and debugger (GDB 7.8) and many new features, including the
following:

- improved diagnostic messages
- fine-grained control over the treatment of warnings
- extended support for non-default endianness
- support for large files on 32-bit systems
- improved handling of inlining
- overflow checks enabled by default
- enhanced code generation and debugging capabilities
- support for aggregate projects in all tools 
- support for stubbing of units in GNATtest

It also comes with the latest version of the GPS IDE, GPS 6.1.1. that 
includes better support for Ada 2012 and SPARK 2014 and a simplified
workflow and project templates for bare board platforms.

GPL editions of GNATbench, AJIS, and PolyORB will be released at a 
later date.

SPARK GPL 2015 - the formal method verification toolset - includes a 
number of major enhancements. New language features include in
particular support for Object-Oriented programming and "ghost code"
used for proof only, with no impact on the generated code.

Proof capability has been significantly improved with the integration
of two provers by default (Alt-Ergo and CVC4), additional automatic
generation of contracts, more precise analysis of modular (bitwise) 
operations, and improved support for manual provers.

Usability has also been enhanced through better categorization of 
messages and output of assumptions made for each verification result.

SPARK GPL 2015 also ships with additional examples, in particular a 
standalone TCP/IP stack implementation. You will find documentation
about the SPARK GPL 2015 toolset here:
http://libre.adacore.com/developers/documentation 

Both toolsets can be downloaded from the "Download" section on
GNAT Tracker:
http://www.adacore.com/academia