Development Log    See All »

  • SPARK Pro
    May 23rd, 2016

    SPARK lemma library for nonlinear int arithmetic
    SPARK now comes with a library of lemmas separately proved in Coq, that can be called in user code to automatically prove nonlinear integer arithmetic properties, i.e. properties involving multiplication, division, modulo. The lemmas are ghost procedures, hence they are removed from the final executable when compiling without assertions. This library of lemmas is meant to be extended based on user needs. It is documented in the SPARK User's Guide, in section 4.10 about SPARK Libraries.

  • CodePeer
    May 23rd, 2016

    Improved support for arrays with static bounds
    CodePeer now performs more accurate analysis of arrays with static bounds and has improved display of dynamically indexed array elements of such arrays.

  • GNAT Pro
    May 20th, 2016

    Elimination of more useless overflow checks at -O2
    The compiler now eliminates more overflow checks that can never fail when the optimization level -O2 or above is specified.

Documentation    See All »

  • QGen User Guide

    This is the user documentation for QGen, a qualifiable and tunable code generation and model verification tool for a safe subset of Simulink® and Stateflow® models.

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