Development Log in May 2017.

  • GNAT Pro
    May 25th, 2017

    New function To_Ada in GNAT.Sockets
    A new function GNAT.Sockets.To_Ada supports converting externally created socket descriptors to type Socket_Type for use with other operations in package GNAT.Sockets.

  • GNAT Pro
    May 24th, 2017

    Debug information for imported entities
    GCC now produces debug information to describe Ada entities that are imported using the Import pragma or aspect.

  • GNAT Pro
    May 23rd, 2017

    Warning on potential C++ ABI mismatch on ARM
    With -Wpsabi on ARM, the compiler now warns in corner case situations where it knows it could possibly generate wrong code for complex C++ constructs involving method calls passing vectors of composite elements as arguments. The issue warned against is a possible caller/callee disagreement about what arguments-passing convention to use, leading to crashes at run time.

  • CodePeer
    May 22nd, 2017

    Better handling of ‘Length in preconditions
    Less false positives when dealing with a 'Length attribute

  • GNAT Pro
    May 22nd, 2017

    Minimize useless body compilations when inlining
    A filter has been added to the inlining / instantiation circuitry to recognize package bodies that do not contain bodies of inlined functions or generic bodies being instantiated, and that therefore do not need to be compiled, even though their declarations may appear in the context of other units that are needed for inlining.

  • SPARK Pro
    May 11th, 2017

    Added preconditions to standard numerical functions
    Preconditions have been added to functions from the standard numerical package Ada.Numerics.Generic_Elementary_Functions, in cases that may lead to Numerics.Argument_Error or Constraint_Error when called on actual parameters that are not suitable, like a negative input for Sqrt. This ensures that GNATprove generates corresponding precondition checks when such functions are called.

  • SPARK Pro
    May 10th, 2017

    Precise handling of dispatching calls with known tag
    GNATprove now precisely determines the subprogram called by a dispatching call when the tag is known. In particular, it is now able to use its more precise specific contract if any.

  • GNAT Pro
    May 6th, 2017

    Warning on potential C++ ABI mismatch on ARM
    With -Wpsabi on ARM, the compiler now warns in corner case situations where it knows it could possibly generate wrong code for complex C++ constructs involving method calls passing vectors of composite elements as arguments. The issue warned against is a possible caller/callee disagreement about what arguments-passing convention to use, leading to crashes at run time.

  • SPARK Pro
    May 5th, 2017

    Improve message for functions that could not return
    GNATprove used to emit a confusing check about initialization of functions when it could not determine if a function would return. We have now improved the message for this check. In addition, when encountering a potentially non returning function, GNATprove will now precise if the function may not return on some or on every path.

  • CodePeer
    May 4th, 2017

    Message text improved for double negations
    In some cases where CodePeer formerly generated messages mentioning conditions of the form "not (X /= Value)", CodePeer now avoids the double negative and generates "X = Value".

  • SPARK Pro
    May 3rd, 2017

    Use unique names for private record parts
    GNATprove now generates unique names for the Why3 translation of private parts of distinct record types. This should facilitate mappings of these parts to distinct types in interactive theorem provers.

  • GNAT Pro
    May 3rd, 2017

    Enhanced -gnatR3 output for simple dynamic records
    The representation information given by the compiler when the -gnatR3 switch is specified now includes size information for simple dynamic record types without discriminants.

  • SPARK Pro
    May 2nd, 2017

    Use unique names for simple private types
    For simple private types (untagged private type with no discriminants and full view out of SPARK) we now use unique names in Why3 so that they can easily be mapped to distinct existing types in interactive provers.