Development Log in July 2015.

  • 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

    Avoid unprovable LSP checks on untagged private
    Visible primitive operations of untagged private types whose full view is tagged previously lead to unprovable checks related to the verification of Liskov Substitution Principle, as Pre'Class cannot be specified on such operations. Dispatching on such subprograms is now forbidden in SPARK and LSP checks not needed anymore on such subprograms as a result.

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

  • SPARK Pro
    Jul 23rd, 2015

    Summary table for proved and unproved checks
    The gnatprove output file "gnatprove.out" now contains a summary table which summarizes the verification results. It shows the number of proved checks, to which category they belong (like initialization checking, runtime errors, or functional contracts) and how various provers contributed to it. Unproved checks are also counted.

  • GNAT Pro
    Jul 22nd, 2015

    Style checks for record components
    Style checks now apply to the alignment of record component declarations.

  • GNAT Pro
    Jul 16th, 2015

    Scalar_Storage_Order and Complex_Representation
    The Scalar_Storage_Order attribute now works in conjunction with record types subject to aspect/pragma Complex_Representation.

  • GNAT Pro
    Jul 15th, 2015

    Create_Temp_File now using mkstemp on Android
    GNAT.OS_Lib.Create_Temp_File now uses mkstemp instead of mktemp to create the temporary file. The former is considered a safer alternative that avoids all possible race conditions when creating the temporary file.

  • GNAT Pro
    Jul 14th, 2015

    Symbolic tracebacks on unhandled exceptions
    When a program is terminated by an unhandled exception, the information in Exception_Information is printed, which can include a symbolic traceback. See NF-74-J408-043 for how to enable such symbolic tracebacks.

  • GNAT Pro
    Jul 14th, 2015

    Symbolic tracebacks in Exception_Information
    The Exception_Information can now include a symbolic traceback when available. It is available on native platforms that use DWARF-format debugging information, which includes Linux, Windows, Solaris, FreeBSD, and AIX. To enable this feature, use the gcc switch "-g" and the binder switch "-Es", as in "gprbuild -g ... -bargs -Es".

  • GNAT Pro
    Jul 13th, 2015

    Better error reporting with premature instantiation
    When a package is instantiated before its body is seen, the compiler creates a dummy body for it to complete the compilation. The dummy function bodies created within the package bodies have no legal return statements, but no cascaded error should be generated for these.

  • SPARK Pro
    Jul 13th, 2015

    Membership tests in tagged type hierarchy
    The GNATprove tool now supports testing for membership of an expression in a tagged type hierarchy.

  • GNAT Pro
    Jul 10th, 2015

    gnatname -P now invokes gprname
    As the project support is phased out of the GNAT tools, a new GPR tool gprname has been introduced to replace "gnatname -P" and "gnatname -P" will silently invoke it for now.

  • SPARK Pro
    Jul 9th, 2015

    Better support for if expressions on real types
    The SPARK proof tool now handles if expressions better, which results in more automatic proofs on programs using if expressions, especially when they have a floating point type.

  • GPS | GNATbench
    Jul 8th, 2015

    GPS: new plugin closeold
    A new optional plugin is provided. It automatically closes the least recently accessed editors when new editors are opened, thus limiting the number of opened editors to a maximum limit. Editors can be pinned to prevent their automatic closing.

  • GPRbuild
    Jul 6th, 2015

    New tool gprname
    A new GPR tool, gprname, is now available. It is the replacement of "gnatname -P".