Development Log in October 2014.

  • GNAT Pro
    Oct 29th, 2014

    Windows GNAT.OS_Lib.Wait_Process improvement
    On Windows the Wait_Process routine now follows the UNIX semantics more closely. The main improvement are:

     - It is possible to have multiple tasks waiting for a child process
       to terminate.
     - When a child terminates, a single wait call will receive the
       corresponding process id.
     - A call to wait will handle new incoming child processes.
    

  • CodePeer
    Oct 29th, 2014

    Suppressing analysis via Annotate pragmas
    By adding "pragma Annotate (CodePeer, Skip_Analysis);" at the start of the declaration list of a subprogram body or a package body, CodePeer's analysis of selected subprogram bodies can be suppressed. This is typically done in order to improve performance. For details, see CodePeer User's Guide section 2.4 ("Running CodePeer Faster").

  • SPARK Pro
    Oct 24th, 2014

    Better error locations for flow analysis
    Flow analysis used to point at the export (Something) when it issued messages like

      warning: incorrect dependency "Something => State"
    
    We now point at the incorrect dependency (State) instead.

  • GNAT Pro
    Oct 23rd, 2014

    Lower gnatls error code severity in some cases
    In some common use cases, gnatls used to return error code 4 (fatal), which was unfriendly for analysis. Calling gnatls with no arguments or arguments "-h" or "-v" has been changed to return 0 (success).

  • GPS | GNATbench
    Oct 23rd, 2014

    GPS:—version and—help no longer require GUI
    The switches are parsed before GPS attempts to connect to the GUI environment. As a result, it is possible to get the help or the version even when the environment is not setup for GUI.

  • GNAT Pro
    Oct 23rd, 2014

    Support for overriding keyword in Ada 95 mode
    For compatibility with some Ada 95 compilers which support only the overriding keyword of Ada 2005, the -gnatd.D debug switch can now be used along with -gnat95 to achieve a similar effect with GNAT.

  • GNAT Pro
    Oct 22nd, 2014

    Win32Ada has some WinCrypt support
    Some Windows WinCrypt routines has been added into the Win32Ada binding. They can be found into the Win32-WinCrypt unit.

  • SPARK Pro
    Oct 21st, 2014

    Mark Ghost functions in formal containers
    Functions First_To_Previous, Current_To_Last and Strict_Equal introduced in units of the formal container library should only be used in contracts and assertions, as they are very inefficient. They are now marked as Ghost functions, which prevents use outside assertions and ghost code.

  • GNAT Pro
    Oct 21st, 2014

    Use of floating-point in fixed-point operations
    In the presence of restriction No_Floating_Point, a multiplication of two fixed point quantities of the same fixed point type in an integer context does not generate conversions to floating-point for run-time evaluation.

  • SPARK Pro
    Oct 20th, 2014

    Raise, no-return and statically-false assertions
    Flow analysis now ignores all statements that inevitably lead to a raise statement, a statically-false assertion or a non-returning procedure. Additionally, all statements that follow a raise statement, a statically-false assertion or a non-returning procedure that are not otherwise reachable from the start of the subprogram are also ignored.

  • SPARK Pro
    Oct 20th, 2014

    New implementation of Ghost entities
    The SPARK toolset now implements the new semantic and legality rules of Ghost entities. This feature now encompasses objects, subprograms, packages and types. As a result, convention Ghost has been replaced with aspect Ghost.

  • GPS | GNATbench
    Oct 17th, 2014

    Support for Runtime & Target attributes in projects
    These two new attributes are now supported by GPS and should replace the use of the IDE'Gnatlist attribute to specify the same information.

  • GPRbuild
    Oct 15th, 2014

    GPRslave control of simultaneous responses
    A new option has been added to GPRslave to control the number of simultaneous responses (sending back object code and ALI files) supported. This was hard coded to 2, it is now possible to set this value between 1 and the maximum number of simultaneous compilations.

  • SPARK Pro
    Oct 14th, 2014

    Replay facility always reissue warnings
    When a unit or the units on which it depends have not changed, GNATprove detects it and avoids re-analyzing the unit. This caused some warnings to be issued only the first time a unit was analyzed. Now, a new replay facility is used in GNATprove to always reissue warning and check messages when a unit is considered, even when it does not require re-analysis.

  • PolyORB
    Oct 13th, 2014

    Extend fast-path CDR marshalling to nested arrays
    The fast-path CDR marsahlling circuitry, allowing efficient marshalling of common aggregates such as arrays of bytes or integers, has been extended to the case of nested arrays.

  • GPRbuild
    Oct 13th, 2014

    Runtime specific directories in the project path
    For each non default runtime, there are now two more directories in the project path: <runtime_root>/lib/gnat and <runtime_root>/share/gpr, where <runtime_root> is either:

      - <runtime> ifthe runtime is explicitly specified as an absolute path
      - <compiler_root>/<target>/<runtime> if the runtime is not explicitly
        specified as an absolute path
    

  • GPRbuild
    Oct 13th, 2014

    Project path depends on compilers
    For tools gprbuild, gprclean and gprinstall, the project path depends on the compilers, not the prefix of the tool. For each compiler driver in a "bin" subdirectory, the compiler root is the parent directory of this "bin" subdirectory and the directories in the project path are, in order:

       <compiler_root>/<target>/lib/gnat
       <compiler_root>/<target>/share/gpr
       <compiler_root>/share/gpr
       <compiler_root>/lib/gnat
    

  • GPRbuild
    Oct 13th, 2014

    New gprbuild option—complete-output
    A new option --complete-output is added to gprbuild, allowed only on the command line and incompatible with option --distributed=. When this option is used, the standard output and standard error of the compiler are redirected to text files. When these files exist for a source that is up to date, their content is output to stdout and stderr.

  • GNAT Pro
    Oct 13th, 2014

    New function Non_Blocking_Spawn
    A new function Non_Blocking_Spawn is added to GNAT.OS_Lib. This function redirects standard error and standard output to two different files.

  • GNAT Pro
    Oct 10th, 2014

    Inlining of renamed subprograms
    The compiler now supports inlining of renamed subprograms.

  • GNAT Pro
    Oct 10th, 2014

    Inlining of unchecked conversion instantiations
    Compiling with back-end inlining enabled the compiler supports implicit inlining of unchecked conversions defined in inlined subprograms (i.e. it is not necessary to add pragma Inline to instantiations of unchecked conversion defined in inlined subprograms).

  • GPS | GNATbench
    Oct 8th, 2014

    GB: better scenario variables support
    Scenario variables editor added capability to:

     * set the variable for all projects
     * unset the variable for all projects to use GNAT project default value
    
    Scenario variables changes are taken into account immediately without having to restart GNATbench.

  • GPS | GNATbench
    Oct 8th, 2014

    GB: add Ada/Environment preferences page
    New Ada/Environment preferences page allows the configuration of the environment used when GNATbench launch any command.

  • GNAT Pro
    Oct 7th, 2014

    Support for POSIX binding shared library
    Florist, the GNAT implementation of the standard Ada binding to the POSIX API, can now be built as a shared library by passing "--enable-shared" to its configure script.

  • SPARK Pro
    Oct 3rd, 2014

    Output of assumptions of verification results
    The SPARK toolset now supports the option --assumptions. With this option, the tool outputs for each verication result in the result file gnatprove.out, the assumptions it depends on. Assumptions are properties which should hold for the verification results to be true, but which the SPARK toolset could not verify by itself. This can happen because the corresponding code is not in the SPARK subset or the verification of that code was not finished. Currently, output assumptions only include the assumptions on called subprograms of analysed subprograms, but not assumptions about the calling context of analysed subprograms.

  • SPARK Pro
    Oct 3rd, 2014

    Support for list of provers to try
    The option --prover of the SPARK toolset has now been improved to allow a list of provers, e.g. the command line option --prover=altergo,cvc4 will first try to prove a VC with altergo, and if that fails, try again with CVC4. The same steps or timeout option applies to all provers.

  • GPS | GNATbench
    Oct 1st, 2014

    GB: add support for “On File Change” builder target
    A builder target having its launch mode set to "On File Change" will be automatically launched each time an ada file is saved. Wind River Workbench users can use this feature to have ada code analyzed as soon as it is saved. Builder target settings are accessible through Ada / Builder Targets preferences page.