Development Log    See All »

  • SPARK Pro
    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.

  • SPARK Pro
    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.

  • SPARK Pro
    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.

Documentation    See All »

  • 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.

  • Using as

    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.

  • GNATdashboard

    This is the manual for administering and using GNATdashboard.