Apr 16th, 2014
Contracts of recursive functions in assertions
An axiom is now also generated for contracts of recursive normal functions. As a consequence, the contracts of every normal functions is now available for proof even if the function is called in a contract or an assertion.
Apr 16th, 2014
Debugger support for variable length arrays in C
The debugger has been enhanced to print the value of C variable length arrays correctly. The sizeof operator now also prints the correct value.
Apr 15th, 2014
Support contextual analysis of local subprograms
GNATprove can now analyze local subprograms without contracts in the context of their calls, as if their body was inlined. This makes it possible to get a very precise analysis, without requiring that the user writes a contract on these subprograms.
GNAT User’s Guide for native platforms
This guide describes the use of GNAT, a compiler and software development toolset for the full Ada programming language.
It describes the features of the compiler and tools, and details how to use them to build Ada 95 applications.
GNAT Pro User’s Guide for OpenVMS
This guide describes the use of GNAT Pro, a compiler and software development toolset for the full Ada programming language, implemented on OpenVMS for HP's Alpha and Integrity server (I64) platforms. It documents the features of the compiler and tools, and explains how to use them to build Ada applications.
SPARK 2014 Toolset User’s Guide
This guide is aimed at getting new users up and running with the SPARK 2014 tools.
SPARK 2014 Reference Manual
This is the reference manual for the SPARK 2014 language and lists all evolutions to the language.
This page gives access to the main GNATemulator documentation. GNATemulator is an efficient and flexible tool that provides integrated, lightweight target emulation.