Development Log    See All »

  • GNAT Pro
    Jul 24th, 2017

    Efficient array reset for all elementary types
    The compiler now generates efficient code to reset a large array of any elementary component type to zeros, or an equivalent value for the component type, so now includes arrays of floating-point and access values instead of being limited to arrays with a discrete component type.

  • GNAT Pro
    Jul 21st, 2017

    Pragma Ada_2020
    Pragma Ada_2020 can be used to enable Ada 2020 features that have been implemented in GNAT. Ada_2020 is a configuration pragma. This is in addition to the -gnat2020 command-line switch.

  • SPARK Pro
    Jul 19th, 2017

    Automatically unroll static loops w/o loop invariant
    Loop invariants are a known difficulty for beginners to use formal program verification. At the same time, many loops written in exercises and to familiarize oneself with the technology have static bounds and a small range. This enhancement implements loop unrolling for such loops with static bounds and not too many iterations (current threshold is at 20 iterations maximum). This way, simple loops with static bounds are proved without requiring a loop invariant. We let the user decide if she wants to use this feature or not: - by only unrolling FOR loops that have no loop (in)variant. - by disabling this feature when the switch --no-loop-unrolling is used.

Documentation    See All »

  • AUnit Cookbook

    This is a short guide for using the AUnit test framework. AUnit is an adaptation of the Java JUnit (Kent Beck, Erich Gamma) and C++ CppUnit (M. Feathers, J. Lacoste, E. Sommerlade, B. Lepilleur, B. Bakker, S. Robbins) unit test frameworks for Ada code.

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