Development Log in April 2015.

  • SPARK Pro
    Apr 30th, 2015

    Improve tracking of values of constants
    The SPARK toolset now tracks better the values of constants defined outside of the analyzed unit. This should result in better proofs, in particular for constants with a nonstatic value or aggregates containing real literals.

  • SPARK Pro
    Apr 30th, 2015

    Improved messages about illegal usage of input
    Formal and global parameters of mode out that are fully default initialized but incorrectly have their input value used have a more accurate message.

  • SPARK Pro
    Apr 29th, 2015

    Better messages for initialization of constituents
    Flow-related messages about constituents now explicitly refer to names of the refined abstract state variables.

  • GNAT Pro
    Apr 29th, 2015

    Speed improvements for controlled types
    The implementation of controlled types is optimized so that in simple cases, they are just as efficient as noncontrolled types where initialization and cleanup is done by hand. For short Initialize/Finalize routines, this can double the speed of object creation and destruction.

  • CodePeer
    Apr 28th, 2015

    New switch -no-presumptions
    CodePeer supports a new switch -no-presumptions to suppress generation of presumptions on unanalyzed subprogram calls. Use of this switch will generally result in additional messages being reported in the vicinity of unanalyzed calls, since assumptions about the result of such calls are no longer made. This option is implied by -level 4.

  • GNAT Pro
    Apr 27th, 2015

    Pragma Abort_Defer respects Restrictions
    Pragma Abort_Defer does nothing in the presence of Restrictions that prevent abort, thus avoiding the overhead of abort deferral. The idea is that you might write some reusable code that is used in programs with abort, and needs Pragma Abort_Defer, but is also used in programs without abort. For the latter, use these restrictions:

      pragma Restrictions (No_Abort_Statements);
      pragma Restrictions (Max_Asynchronous_Select_Nesting => 0);
    
    
    and there will be no overhead for abort deferral.

  • GNAT Pro
    Apr 26th, 2015

    Elaboration Warning for Finalize can be suppressed
    The warning that Finalize (or Initialize or Adjust) might cause a possible elaboration problem can now be suppressed by using Warnings (Off, T) where T is the controlled type involved.

  • SPARK Pro
    Apr 24th, 2015

    Better support for expression functions
    The SPARK toolset now deals better with non-recursive expression functions returning real types.

  • GNAT Pro
    Apr 24th, 2015

    Static elab—internal calls to instances
    The static elaboration model is necessarily conservative, leading to elaboration cycles in cases that would in fact not fail at run time. However, in certain obscure cases of a call to a subprogram in an instance of a generic package that is within this same unit as the call, the compiler is now less conservative, avoiding elaboration cycles in those cases.

  • GPRbuild
    Apr 21st, 2015

    —create-map-file for cross targets
    This is now supported on cross platforms that use GNU ld to link.

  • GPS | GNATbench
    Apr 20th, 2015

    GPS: Ability to provide fonts under UNIX
    GPS comes with a mechanism for adding custom fonts. (This does not work on Windows, where the fonts need to be installed at the system level). GPS 6.2 also comes with better default fonts out-of-the-box.

  • GNAT Pro
    Apr 20th, 2015

    Improve consistency of floating-point **
    This enhancement ensures on all targets that A**B = A**C when B is a small static constant in the range 0 .. 4 and C is a variable with the same value. Previously for Float and Long_Float on some targets, this was not the case. The results given were both within the error bounds that are allowed by the Ada standard, but it is desirable not to have this discrepancy. This also aids formal verification of such operations.

  • GNAT Pro
    Apr 18th, 2015

    New restrictions pragmas recognized in System
    Only certain restriction pragmas are recognized in package System, and now No_Specification_Of_Aspect, No_Use_Of_Attribute, and No_Use_Of_Pragma have been added to the recognized list, allowing more flexibility in configuring new versions of the System package.

  • SPARK Pro
    Apr 14th, 2015

    support for ‘Address Attribute
    The SPARK toolset now supports the 'Address attribute for objects.

  • GPRbuild
    Apr 12th, 2015

    GPRbuild distributed environment variables
    gprbuild and gprslave now accepts slaves to be specified using environment variables. Either GPR_SLAVES which contains a coma separated list of host names or GPR_SLAVES_FILE with specify a file whose content must be an host name per line.

  • GNAT Pro
    Apr 11th, 2015

    New aspect Disable_Controlled
    A new aspect Disable_Controlled is defined for controlled record types. If active, this aspect causes suppression of all related calls to Initialize, Adjust, and Finalize. The intended use is for conditional compilation, where for example you might want a record to be controlled or not depending on whether some run-time check is enabled or suppressed.

  • GPS | GNATbench
    Apr 10th, 2015

    GPS: Python to configure views
    The settings from the local configuration menus of the views can now be toggled via python commands, using the GPS.Preference API.

  • SPARK Pro
    Apr 9th, 2015

    Improve support for Size attributes
    The SPARK toolset now fully supports the Size attribute, which was supported only for prefixes that are constrained types.

  • GNAT Pro
    Apr 7th, 2015

    Improve speed of Append for Vectors
    The speed of Ada.Containers.Vectors.Append has been improved. Simple benchmarks show that in common cases, Append is over 3 times faster than it was.

  • GNAT Pro
    Apr 6th, 2015

    Improve speed of “for ... of” loops for containers
    The speed of "for ... of" loops over predefined containers has been improved substantially. Simple benchmarks show that the overhead of such loops has been cut by a significant factor, up to 30.

  • GNAT Pro
    Apr 6th, 2015

    Improved warning for misused trailing array idiom
    Some packages implementing interfaces to C/C++ libraries, for example Win32, use the trailing array idiom, whereby a trailing array in a record type is intended to be safely overrun to access a larger buffer. The compiler now warns in more cases where this idiom is used in an incorrect manner on the client side in conjunction with aggressive loop optimization (-O2 or above).

  • GNAT Pro
    Apr 3rd, 2015

    Avoid surprising failure of fpt postcondition
    When operating on a machine with extended precision intermediate results, such as the x86 with traditional floating-point, then a postcondition of the form X'Result = Expr may unexpectedly fail due to extra precision in the calculation of Expr. An implicit 'Machine operation is now introduced in this specific case to avoid this surprise.

  • GNAT Pro
    Apr 2nd, 2015

    The visium-elf port produces GR6 code by default
    The visium-elf toolchain now produces code for the latest variant (GR6) of the architecture by default and the associated RTS libraries are compiled in this mode as well.

  • SPARK Pro
    Apr 2nd, 2015

    Improve handling of discrete types
    The SPARK toolset now handles discrete types in a way closer to the underlying model for arithmetic operations. This results in more discharged verification conditions.

  • GNAT Pro
    Apr 1st, 2015

    gnatmake -P invokes gprbuild when available
    When gnatmake [gnatclean] is invokes with -P, if gprbuild [gprclean] is available, then gnatmake [gnatclean] invokes gprbuild [gprclean] with the same arguments.

  • Ada Web Server
    Apr 1st, 2015

    Add support pattern in WebSocket registry
    It is now possible to use regular expression to register WebSocket constructors.