Development Log    See All »

  • SPARK Pro
    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 Pro
    Apr 14th, 2014

    Warn on postconditions for No_Return Subprograms
    The only postcondition that makes sense for a subprogram labeled as being No_Return (using the pragma of that name) is an explicit False test. Any other postcondition is useless and suspicious. A warning (under control of -gnatw.t/-gnatw.T) is now given for such useless postconditions.

  • GNAT Pro
    Apr 13th, 2014

    gnatcheck:—incremental mode
    gnatcheck now supports the --incremental switch, similarly to gnat2xml and gnatpp. --incremental invokes incremental processing on a per-file basis. Source files are only processed if they have been modified, or if files they depend on have been modified. This is similar to the way gnatmake/gprbuild only compiles files that need to be recompiled.

Documentation    See All »

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

  • GNATemulator documentation

    This page gives access to the main GNATemulator documentation. GNATemulator is an efficient and flexible tool that provides integrated, lightweight target emulation.