Development Log in November 2016.

  • CodePeer
    Nov 30th, 2016

    Better messages for access-to-subprogram uses
    In some cases a dereference of an access-to-subprogram value could result in a CodePeer message like "... requires Ptr >= 1" which is inappropriate for a non-numeric value. Instead, we now generate "... requires Ptr /= null" .

  • GNAT Pro | GPS | GNATbench
    Nov 29th, 2016

    WB: run quickfix from Ada editor left ruler
    Quickfix process can be initiated clicking Ada markers in Ada editor left ruler. Initiating quickfix from problems view is still supported.

  • GNAT Pro | GPS | GNATbench
    Nov 29th, 2016

    WB: run quickfix from Ada editor left ruler
    Quickfix process can be initiated clicking Ada markers in Ada editor left ruler. Initiating quickfix from problems view is still supported.

  • GNAT Pro
    Nov 28th, 2016

    Non-blocking wait for child process termination
    A new procedure Non_Blocking_Wait_Process is added to GNAT.OS_Lib. It is the same as Wait_Process, except that if there are no completed child processes, it returns immediately without blocking.

  • CodePeer
    Nov 26th, 2016

    Better handling of data modified by unknown calls
    Data that can possibly be modified by a call to a subprogram not analyzed by CodePeer are computed more precisely. In particular, bounds of arrays that are passed as out or in out parameters in a call to an unanalyzed subprogram are no longer considered as possibly modified by the call.

  • GNAT Pro | GPS | GNATbench
    Nov 25th, 2016

    WB: add support of ppc64-vx7 target
    Wind River Workbench projects for powerpc64-wrs-vxworks7 platform can be converted to Ada project and then built through Workbench builder.

  • GNAT Pro | GPS | GNATbench
    Nov 25th, 2016

    WB: add support of ppc64-vx7 target
    Wind River Workbench projects for powerpc64-wrs-vxworks7 platform can be converted to Ada project and then built through Workbench builder.

  • GNAT Pro
    Nov 25th, 2016

    New warning on late dispatching primitives
    Compiler provides a new warning (enabled by means of switches -gnatw.j or -gnatwa) that warns on public primitives of a tagged type defined after some private extension of it.

  • GNAT Pro
    Nov 24th, 2016

    Support for vxWorks 653 2.5.0.2
    GNAT Pro for vxWorks 653 now supports 2.5.0.2 on both PowerPC and e500v2.

  • SPARK Pro
    Nov 23rd, 2016

    Improved error message
    In case of a subprogram having an output global which is used as an input of the subprogram in its body we now provide more information on the error message.

  • GNATCOLL.SQL easier to add new field types
    It is now easier to add new field types. GNATCOLL used to have enumeration types internally, which meant that adding new types had mostly to be done by modifying GNATCOLL itself. See the package GNATCOLL.SQL_Fields for an example. The JSON and XML field types now use this new framework, as an example. This means that if you are using these in applications currently, you will likely need to add a 'with GNATCOLL.SQL_Fields;' to keep your code compiling.

  • SPARK Pro
    Nov 22nd, 2016

    Better interval analysis of int to float conversions
    Interval analysis is a simple analysis that allows proving range checks and overflow checks simply by computing the worst-case bounds of expressions based on the types of subexpressions. This analysis now also deals precisely with conversions from integers to floating-point types, which improves provability of programs with such conversions.

  • SPARK Pro
    Nov 22nd, 2016

    Remove trivial checks on float-to-int conversions
    Range checks on float-to-int conversions that can be proved to be always passing by trivial interval analysis of the types of subexpressions are not emitted anymore. This improves provability of programs where such conversions are used, as automatic provers sometimes had difficulty proving range checks on such conversions.

  • SPARK Pro
    Nov 21st, 2016

    New lemma on array ordering
    We have added a new lemma for sorted arrays in the SPARK lemma library. This lemma allows proving ordering between arbitrary elements of the array using transitivity of the order.

  • CodePeer
    Nov 21st, 2016

    Improved CodePeer handling of tagged types
    CodePeer encounters fewer capacity limitations (timeouts, too many value numbers) for examples which declare tagged types, including examples which instantiate Ada's predefined container generics.

  • GNAT Pro | GPRbuild
    Nov 19th, 2016

    SAL projects and -bargs
    When gprbuild is invoked with a main project that is a Stand-Alone Library project and with binding options specified on the command line after switch -bargs, a warning is displayed indicating that command line binding options are not taken into account when the main project is a SAL project.

  • GNAT Pro
    Nov 17th, 2016

    Static intialization with pragma Linker_Section
    If an array object has a pragma Linker_Section with a compile- time-known initial value, the object is statically initialized in place in the appropriate section, as opposed to being initialized by elaboration code at run time.

  • GNAT Pro
    Nov 17th, 2016

    More compact code for concatenation at library level
    The compiler generates more compact code for concatenation operations performed on strings within the initialization expression of an object declared at library level.

  • CodePeer
    Nov 17th, 2016

    Support for -gnatxxx switches
    CodePeer now supports the -gnatxxx compiler switches directly, either from the command line, or from the Switches attribute in the CodePeer package in project files, giving more flexibility in particular coupled with the -compiler-mode switch. This also allows specifying CodePeer-specific compiler switches (such as -gnatI) without impacting compilation.

  • GNAT Pro
    Nov 16th, 2016

    Specifying an address clause on controlled objects
    It is now possible to specify an address clause on objects which are either derived from Ada.Finalization.Controlled or Limited_Controlled, or contain controlled components.

  • GNAT Pro
    Nov 11th, 2016

    More efficient trigonometric functions on x86
    The implementation of the sin, cos, and tan functions in children of Ada.Numerics is now more efficient on the x86 architecture.

  • GNAT Pro | GPS | GNATbench
    Nov 10th, 2016

    GPS: speed up Project and Files views
    Creating either views is now much faster, in particular on large projects where a directory contains several thousands of files.

  • GNAT Pro | GPS | GNATbench
    Nov 10th, 2016

    GPS: speed up Project and Files views
    Creating either views is now much faster, in particular on large projects where a directory contains several thousands of files.

  • SPARK Pro
    Nov 10th, 2016

    Loop invariant generation for preserved components
    GNATprove can automatically generate loop invariants specifying the preservation of array and record components that are not modified during a loop. This generation is a heuristic which only works in the most common cases.

  • GNAT Pro | GPS | GNATbench
    Nov 9th, 2016

    GPS: Number of replacements reported
    GPS now reports in the Messages window the number of occurrences that have been replaced when 'Replace All' button of the Search view is clicked.

  • GNAT Pro | GPS | GNATbench
    Nov 9th, 2016

    GPS: Number of replacements reported
    GPS now reports in the Messages window the number of occurrences that have been replaced when 'Replace All' button of the Search view is clicked.

  • SPARK Pro
    Nov 9th, 2016

    Types with partial default initialization allowed
    Types with partial default initialization were previously not allowed in SPARK, which made it difficult to analyze some existing codebases. They are now allowed.

  • SPARK Pro
    Nov 8th, 2016

    Improve provability of checks in loops
    Checks whose proof depends on assuming the loop invariant at the current iteration of the loop could be unprovable due to part of the loop invariant being simplified to True or False. This simplification is now disabled in assertions to improve provability of checks in loops.

  • GNAT Pro | GPS | GNATbench
    Nov 7th, 2016

    GPS: new setting to preserve build messages
    The local configuration menu of the Locations view now contains an item "Preserve message" to control whether to keep build messages for files that are not being recompiled.

  • GNAT Pro | GPS | GNATbench
    Nov 7th, 2016

    GPS: new setting to preserve build messages
    The local configuration menu of the Locations view now contains an item "Preserve message" to control whether to keep build messages for files that are not being recompiled.

  • GNAT Pro
    Nov 7th, 2016

    New pragma No_Heap_Finalization
    This pragma may be used as a configuration pragma or as a type- specific pragma. In its type-specific form, the argument of the pragma must denote a library-level named access-to-object type. The pragma suppresses calls to Finalize for heap-allocated objects created through the argument type in cases where the designated type requires finalization actions.

  • Ada Web Server
    Nov 7th, 2016

    Add support for GZip content-encoded messages
    AWS now supports messages sent from a client with the GZip content encoding. In this case the actual message is automatically inflated by AWS.

  • GNAT Pro | GPS | GNATbench
    Nov 4th, 2016

    GPS: hidden files in the Files view
    The Files view now reuses the same preference as the Project view to hide some files (those starting with "." by default, although this can be configured in the preferences dialog).

  • GNAT Pro | GPS | GNATbench
    Nov 4th, 2016

    GPS: hidden files in the Files view
    The Files view now reuses the same preference as the Project view to hide some files (those starting with "." by default, although this can be configured in the preferences dialog).

  • Ada Web Server
    Nov 3rd, 2016

    Add support chunked client messages
    AWS now supports messages sent from a client with the chunked transfer encoding.

  • SPARK Pro
    Nov 3rd, 2016

    more precise volatility for protected objects
    A new rule 7.1.2(16) was added to SPARK RM, along with SPARK tool updates, to better control the volatility of protected objects. Previously they were fully volatile, now they have only Async_Readers and Async_Writers. If a separate volatile variable is a Part_Of such a protected object, the protected object inherits any volatility aspects (i.e. Effective_Reads or Effective_Writes) of its Part_Of constituent.

  • SPARK Pro
    Nov 2nd, 2016

    Division checks now proved by CodePeer integration
    Division by zero checks can now be proved by the CodePeer integration in SPARK, which was not the case previously.

  • SPARK Pro
    Nov 2nd, 2016

    Assertion checks now proved by CodePeer integration
    Assertion checks (pragma Assert, Loop_Invariant, Assert_And_Cut) can now be proved by the CodePeer integration in SPARK, which was not the case previously.

  • GNATCOLL.SQL.Upper new aggregate function
    A mapping to SQL's UPPER function was added