Development Log    See All »

  • SPARK Pro
    Jun 6th, 2016

    Support optional refinement in private part/child
    SPARK Reference Manual now allows refinement through the user of pragma or aspect Refined_Global and/or Refined_Depends in scopes where the full refinement of an abstract state is not visible, like the private part of the package defining the abstract state, or one of its child packages. The special rules in SPARK RM 7.2.4 for this so-called optional refinement are now supported in GNAT and GNATprove.

  • SPARK Pro
    Jun 6th, 2016

    Global variables known to be initialized in loops
    GNATprove now knows that in out global variables and parameters that are modified in loops are always initialized and thus are in their types. In particular, variables are in their range for scalars and their dynamic predicate is true if they have one.

  • SPARK Pro
    Jun 3rd, 2016

    Suppressed wrong warning message for X’Address
    SPARK does not look at X in X'Address as a used variable anymore and therefore it does not emit a warning message in case X is not initialised.

Documentation    See All »

  • GNATbench for WRS Workbench User’s Guide

    This User’s Guide describes how to use the GNATbench Ada plug-in for Windriver Workbench . Specific help is provided for configuring projects, building systems, and debugging.

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