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

[Jamie Ayre]

Dear GAP members,

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

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

- Generation of C headers from Ada specs
- Detection of invalid memory access via libsanitizer on Linux
- SSE floating point extensions enabled by default on all x86 native ports
- Performance improvements on Ada containers
- New pragmas to support low level programming on bare board targets
- New pragmas to ease porting legacy code
- Support for Windows 10

GNAT GPL 2016 for ARM has extended Ada runtime support for the STM32f429-disco, STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.

* ravenscar sfp/full for the stm32f429-disco board
* ravenscar sfp/full for the stm32f469-disco board
* ravenscar sfp/full for the stm32f7-disco board

GNAT GPL 2016 also comes with the latest version of the GPS IDE, GPS 6.2.1. that  includes the following:

- New C & C++ code intelligence engine based on libclang 
- HiDPI monitors support 
- Improved performance 
- Multiple color themes

SPARK GPL 2016 - the formal method verification toolset - includes the following new features:

- Support for concurrency with Ravenscar and type predicates
- Generation of counterexamples for unproved checks
- Better support of bitwise (modular) operations in proof
- Alt-Ergo 0.99.1, CVC4 and Z3 provers are now included
- Generation of global summary table

You will find documentation about the SPARK GPL 2016 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