Development Log in December 2015.

  • SPARK Pro
    Dec 23rd, 2015

    Fine-grain analysis of generic code in GPS
    It is now possible to use the submenus "Examine Subprogram", "Prove Subprogram", "Prove Line" and "Prove Check" (from the contextual menu in GPS) from within a generic unit, which has the effect of applying the desired analysis on all instances of the generic unit. The same effect can be obtained on the command-line by using switch -U in addition to the required switches --limit- subp and --limit-line, although the main benefit is expected to be for interactive use in GPS.

  • GNAT Pro | GPS | GNATbench
    Dec 22nd, 2015

    GPS: OS shell emits stty command automatically
    The "OS Shell" window sometimes need a "stty echo" command to properly display the keys typed on the keyboard. GPS now has a preference to automatically emit this command. The new shell also has a GPSSHELL environment variable set automatically, so that you can test it in your shell's configuration files to enable or disable specific behaviors.

  • GNAT Pro | GPS | GNATbench
    Dec 22nd, 2015

    GPS: OS shell emits stty command automatically
    The "OS Shell" window sometimes need a "stty echo" command to properly display the keys typed on the keyboard. GPS now has a preference to automatically emit this command. The new shell also has a GPSSHELL environment variable set automatically, so that you can test it in your shell's configuration files to enable or disable specific behaviors.

  • GNAT Pro | GPS | GNATbench
    Dec 22nd, 2015

    GPS: OS shell emits stty command automatically
    The "OS Shell" window sometimes need a "stty echo" command to properly display the keys typed on the keyboard. GPS now has a preference to automatically emit this command. The new shell also has a GPSSHELL environment variable set automatically, so that you can test it in your shell's configuration files to enable or disable specific behaviors.

  • GNAT Pro | GPS | GNATbench
    Dec 16th, 2015

    GPS: export the output of program runs
    A new button was added to the local toolbar of the Run view, to save the run command output to a file.

  • GNAT Pro | GPS | GNATbench
    Dec 16th, 2015

    GPS: export the output of program runs
    A new button was added to the local toolbar of the Run view, to save the run command output to a file.

  • GNAT Pro | GPS | GNATbench
    Dec 16th, 2015

    GPS: export the output of program runs
    A new button was added to the local toolbar of the Run view, to save the run command output to a file.

  • GNAT Pro
    Dec 16th, 2015

    -gnatmake -P and -gnatclean -P
    "<target>-gnatmake -P" now invokes "gprbuild --target=<target>". "<target>-gnatclean -P" now invokes "gprclean --target=<target>".

  • SPARK Pro
    Dec 15th, 2015

    Better support for use of Why3 IDE
    For advanced users and mainly in connection with manual proof using interactive proof assitansts such as Coq and Isabelle, it can be useful to use the Why3 IDE (not provided by AdaCore) to inspect and modify the session file. This use case is now better supported, mainly it is easier to see what SPARK check a VC corresponds to.

  • GNAT Pro
    Dec 15th, 2015

    More consistent layout beyond ASIS DDA with -gnatct
    The layout of some complex types not covered by ASIS DDA, in particular of discriminated tagged types, has been adjusted when -gnatct is specified.

  • SPARK Pro
    Dec 9th, 2015

    Generics’ formals can now appear on contracts
    The SPARK toolset now allows user provided contracts that are placed on generics to refer to the generics' formals.

  • GNAT Pro
    Dec 9th, 2015

    Enhanced debugger menu to select function overload
    When trying to evaluate an expression referencing an ambiguous function name in the debugger, a menu queries which function to use. This menu has been enhanced to display the argument types and the return type (if applicable) for all the overloaded functions to make the choice easier. This behavior can be disabled with the "set/show ada print-signatures" commands.

  • GNAT Pro
    Dec 9th, 2015

    Better message on illegal reference in aspect
    This patch improves on the error message for a reference to the current entity in an aspect for a type, when the reference freezes the type.

  • GPS | GNATbench
    Dec 9th, 2015

    GPS: update integration of gnattest for stubbing
    GPS support of gnattest is improved. GPS is able to navigate into stubs, stub setters and original subprogram bodies. Run button launches gnattest in execution mode when multiple test drivers are generated by gnattest.

  • GNAT Pro | GPRbuild
    Dec 5th, 2015

    Path names of duplicate unit sources
    In verbose mode, when a duplicate unit is found in two sources, the path names of the two sources are now output.

  • GNAT Pro | GPS | GNATbench
    Dec 4th, 2015

    GB: trailing space removal set to autodetect
    The default value of the "remove trailing spaces when saving" feature is set to Autodetect. When editing new files and Autodetect mode is selected, the trailing spaces are removed. In this mode they are preserved only if trailing spaces were detected in the file content when the file was opened.

  • GNAT Pro | GPS | GNATbench
    Dec 4th, 2015

    GB: trailing space removal set to autodetect
    The default value of the "remove trailing spaces when saving" feature is set to Autodetect. When editing new files and Autodetect mode is selected, the trailing spaces are removed. In this mode they are preserved only if trailing spaces were detected in the file content when the file was opened.

  • GNAT Pro | GPS | GNATbench
    Dec 4th, 2015

    GB: trailing space removal set to autodetect
    The default value of the "remove trailing spaces when saving" feature is set to Autodetect. When editing new files and Autodetect mode is selected, the trailing spaces are removed. In this mode they are preserved only if trailing spaces were detected in the file content when the file was opened.

  • GNAT Pro
    Dec 3rd, 2015

    Obj’Image is implemented
    AI12-0124-1 extends the semantics of attribute 'Image so that the prefix can be an object of a scalar type, following the semantics of the GNAT-specific attribute 'Img.

  • GNAT Pro | GPRbuild
    Dec 2nd, 2015

    New Library_Kind “static-pic”
    A new library kind "static-pic" is introduced. static-pic libraries are static libraries, but their code is compiled with the PIC option, if it exists.

  • CodePeer
    Dec 2nd, 2015

    New switch: -compiler-mode
    A new CodePeer switch -compiler-mode is provided to replace the use of codepeer-gprbuild -gnateC, allowing more flexiblity and in particular support for other CodePeer switches (on the command line or in the project file).