Development Log in March 2017.

  • SPARK Pro
    Mar 30th, 2017

    Globals of renamed subprograms in code not-in-SPARK
    GNATprove now synthesizes more precise Global contracts for subprograms annotated with SPARK_Mode => Off that make calls via subprogram renamings. Such calls happen, for example, in instances of generic units with formal subprogram parameters.

  • GNAT Pro | GPS | GNATbench
    Mar 28th, 2017

    GPS: Auto fix for prefix of Result attribute
    GPS provides auto fix to help with compiler errors of the form 'incorrect prefix for attribute "Result", expected "Incr2"'.

  • GNAT Pro | GPS | GNATbench
    Mar 27th, 2017

    GNATDOC: Documentation for concurrent constructs
    Detailed information is generated for task and protected objects, including their subprograms and entries.

  • CodePeer
    Mar 27th, 2017

    Better messages for null statements
    CodePeer flags both dead null statements and predetermined test conditions which govern the possible execution of null statements.

  • GNAT Pro
    Mar 27th, 2017

    GNATdoc can now extract documentation from bodies
    GNATdoc has a new capability, activated by the command-line switch '-d'; in this mode, GNATdoc processes bodies and extracts documentation for library-level entities.

  • SPARK Pro
    Mar 24th, 2017

    Empty “others” alternative in Case statement
    Flow analysis now detects when an "others" alternative of a Case statement corresponds to an empty range and effectively considers its sequence of statements as unreachable. This helps to avoid spurious messages about variables not being referenced or initialized within that sequence of statements.

  • GNAT Pro
    Mar 24th, 2017

    Automatic reordering of components in record types
    The compiler can now reorder components in record types with convention Ada in order to fix blatant inefficiencies that the layout of components in textual order would bring about. The reordering is automatic and silent by default, but both characteristics can be toggled: pragma No_Component_Reordering disables it either on a per-record-type or on a global basis, while -gnatw.q gives a warning for each affected component in record types.

  • GNAT Pro
    Mar 23rd, 2017

    Relax alignment constraint for record extensions
    On x86 and, more generally, architectures that do not require strict alignment for memory accesses, the compiler now accepts size clauses on record type extensions that effectively lower the alignment of the type, if there is also a representation clause on the type.

  • SPARK Pro
    Mar 21st, 2017

    Simplified translation of simple private types
    Untagged private types with no discriminant whose full view is not in SPARK are now translated in Why3 as clones of the predefined __private abstract type. This should allow users of interactive proof assistants to more easily map these private types to a logic type of their choice.

  • GNAT Pro | GPS | GNATbench
    Mar 20th, 2017

    GPS: The Window menu now contains icons
    Icons were added in the Window menu for editors. This allows displaying which editors are currently modified.

  • SPARK Pro
    Mar 20th, 2017

    Theories for conversion of discrete types realized
    The Why3 theories used by GNATprove to model conversions between discrete types have been realized in Coq. This increases confidence in their correction.

  • GNATCOLL.Traces performance improvements
    Performance has been significantly enhanced: streams no longer flush after each message by default (though this is now configurable in the configuration file), locking is done at the stream level, and can often be avoided altogether since the system provides its own locking, messages are created as a whole line and then sent once to the stream, which provides more flexibility when writing streams, and other various enhancements. In a single threaded application, we now output 6 million messages per second to a file.

  • GNAT Pro
    Mar 16th, 2017

    GNAT includes a ZFP runtime for Linux and Windows
    The native ZFP (Zero Footprint) runtime for Linux and Windows is now part of the base GNAT package. It is now also available with 64-bit compilers. This runtime is similar to the ZFP runtimes that are delivered with our bare metal products and can be used to test an embedded project in a native environment.

  • CodePeer
    Mar 15th, 2017

    Better messages for .scil file creation failure
    If CodePeer unsuccessfully attempts to create a .scil file, then generate an additional error message which includes the full name of the file which could not be created. If it appears likely that the source of the problem is a Windows-specfic restriction on filename lengths, then that is also noted in a message.

  • GNATCOLL.Mmap: support files larger than 2Gb
    This package now supports mapping files up to 1 petabyte, on 64 bits systems. This is backward compatible, although to access such large files you will need to use some different functions. This package also includes support for the madvise() system call on Unix systems, which might provide a 5% performance improvements when accessing files sequentially.

  • GNATCOLL.Strings: new package
    This package, and the generic implementation in GNATCOLL.Strings_Impl, provide a new string type. A XString is similar to an unbounded string, but more efficient (up to 10x for strings 23 characters or less, or when manipulating substrings, and up to 1.4 for larger strings), and with a more extensive API.

  • GNATCOLL.Promises: new package
    This package provides a promise type, also known as a future in some language. This is a way to perform background computation, then chain a series of callbacks which can themselves perform asynchronous computation.

  • GNAT Pro
    Mar 13th, 2017

    Option to treat run-time exception warnings as errors
    The compiler supports a new switch -gnatwE that treats warnings that run-time exceptions will occur as compile-time errors.

  • Ada Web Server
    Mar 11th, 2017

    Add support for type/subtype in ada2wsdl
    The tool ada2wsdl will now generate proper WSDL out of Ada specs using types or subtypes to derived from other Ada specs.

  • SPARK Pro
    Mar 9th, 2017

    New switch produces header in gnatprove.out
    The new switch --output-header produces a header in the generated file gnatprove.out, with useful information about the run of GNATprove, such as the version number, date, host platform and switches used.

  • GNAT Pro | GPRbuild
    Mar 7th, 2017

    Extending a package from a project being extended
    In an extending project A, it is now possible to extend a package P from the project being extended B, when project B is extending another project C and package P is not declared in project B but has only been inherited from project C.

  • Ada Web Server
    Mar 7th, 2017

    Add support for xsd:dateTime in ada2wsdl
    The ada2wsdl tool will now generate a SOAP xsd:dateTime for references to the standard Ada.Calendar.Time.

  • GNAT Pro
    Mar 4th, 2017

    Ceiling locking on Linux without root privileges
    Ceiling locking on Linux no longer requires root privileges. Instead, you can run "sudo /sbin/setcap cap_sys_nice=ep exe_file" to set the relevant capability on the executable file, and then that program can use ceiling locking without running as root.

  • Ada Web Server
    Mar 4th, 2017

    Add support for selecting encoding in ada2wsdl
    The ada2wsdl tool has a new option to select the encoding to be used by the SOAP services.