Jul 30th, 2015
Generated Initializes contracts
The tools now internally generate Initializes contracts for packages that do not have user-provided Initializes contracts. This reduces the false alarm rate about uninitialized uses of variables.
Jul 29th, 2015
Support for all kinds of type predicates
The SPARK tool now handles all kinds of type predicates, in particular static predicates on floating-point types and dynamic predicates on any type. A dynamic predicate check is generated at every program point where the predicate associated to a value might be violated.
Jul 24th, 2015
Better support for quantification with Iterable
The SPARK proof tool now handles quantification using the Iterable aspect better, especially when cursors are record or private subtypes.
The GNU binary utilities
This is the documentation for GNU Binary Utilities.
The GNU linker
This is the documentation for GNU ld, the GNU linker, part of GNU Binutils.
This is the user manual for GAS, the GNU Assembler, part of GNU Binutils.
Debugging with GDB
This is the main documentation for GDB, the GNU source-level debugger.
This is the manual for administering and using GNATdashboard.