Development Log in March 2016.

  • GNAT Pro | GPS | GNATbench
    Mar 31st, 2016

    GPS: width of omnisearch popup
    The width of the popup window for the omnisearch (at the top-right corner of the main window) is now proportional to that of the search field itself. And the width of the latter can be set by changing the settings, which is useful if you have long file names in your application.

  • SPARK Pro
    Mar 31st, 2016

    Deterministic proof by default with no timeout
    GNATprove is now deterministic by default, so it does not use timeouts unless explicitly instructed by the user to do so. Instead, a steps limit is used to bound the effort made by automatic provers to find a proof. This new design is based on a few changes: the proof level (switch --level) is 0 by default, proof level sets a value of steps but no value of timeout, switch --timeout takes a new value "auto", in addition to a possible time in seconds. The semantics of --timeout=auto is that it adjusts to the value of the proof level.

  • SPARK Pro
    Mar 31st, 2016

    Always generate axiom for expression function
    Previously, no axiom was generated for an expression function in a part of code with no explicit SPARK_Mode, which prevented proofs of client code that relied on the implicit postcondition of the expression function. Now, an axiom is generated in such a case.

  • GNAT Pro | GPS | GNATbench
    Mar 31st, 2016

    GPS: width of omnisearch popup
    The width of the popup window for the omnisearch (at the top-right corner of the main window) is now proportional to that of the search field itself. And the width of the latter can be set by changing the settings, which is useful if you have long file names in your application.

  • GNAT Pro | GPS | GNATbench
    Mar 30th, 2016

    GPS: listvars.py plugins shows reference type
    The optional listvars.py plugin (which adds a contextual menu "Variables used in ...") now also shows the type of reference for those variable (read, write, dispatching call,...)

  • GNAT Pro | GPS | GNATbench
    Mar 30th, 2016

    GPS: listvars.py plugins shows reference type
    The optional listvars.py plugin (which adds a contextual menu "Variables used in ...") now also shows the type of reference for those variable (read, write, dispatching call,...)

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

    GPS: revamp the debugger Breakpoints view
    This view shows the current list of breakpoints set in the debugger. Its layout has been modified so that it is now smaller and can more easily be a permanent fixture of the desktop. Clicking on a breakpoint will display all its properties (both basic like file and line, exception name,... and advanced like the condition to be met for the debugger to stop).

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

    GPS: revamp the debugger Breakpoints view
    This view shows the current list of breakpoints set in the debugger. Its layout has been modified so that it is now smaller and can more easily be a permanent fixture of the desktop. Clicking on a breakpoint will display all its properties (both basic like file and line, exception name,... and advanced like the condition to be met for the debugger to stop).

  • GNAT Pro
    Mar 29th, 2016

    Ada.Execution_Time implemented on Darwin
    The standard package Ada.Execution_Time is now supported on Mac OS X.

  • CodePeer
    Mar 25th, 2016

    Improved unchecked conversion analysis
    CodePeer now knows about unchecked type conversions between signed and unsigned integer types if the target subtype has basetype bounds and the source type's size is no larger than that of the target type.

  • GNAT Pro
    Mar 24th, 2016

    Multiprocessor support (SMP) on leon3-elf
    The ravenscar runtimes supports multiple processors on leon3-elf platform.

  • CodePeer
    Mar 23rd, 2016

    Improved support for System.Address as pointer
    CodePeer now supports 'null' as a valid value when dealing with System.Address, to support legacy Ada compilers where System.Address is declared as a pointer.

  • GNAT Pro
    Mar 23rd, 2016

    Optimization of memory usage for array aggregates
    The compiler no longer generates an anonymous object for a declaration initialized by a qualified array aggregate.

  • GNAT Pro
    Mar 23rd, 2016

    Improved warnings on address clauses with offset
    The size warning issued for address clauses that cause a variable to overlay a component of another variable (e.g. "for X'Address use Y.Comp'Address;") now takes into account the offset of X within Y and prints its value.

  • SPARK Pro
    Mar 22nd, 2016

    Use stable names for aggregates used in definitions
    Aggregates used as initialization expressions in the declaration of objects now get transformed in Why3 into modules and functions with a stable name across versions in GNATprove, based on the name of the object they define. This eases maintenance of manual proofs done in interactive provers.

  • GNAT Pro | GPS | GNATbench
    Mar 21st, 2016

    WB: add VxWorks 653 3.1 support
    GNATbench is able to handle Wind River Workbench projects for VxWorks 653 3.1 target operating system.

  • GNAT Pro | GPS | GNATbench
    Mar 21st, 2016

    WB: add VxWorks 653 3.1 support
    GNATbench is able to handle Wind River Workbench projects for VxWorks 653 3.1 target operating system.

  • SPARK Pro
    Mar 21st, 2016

    Reproducible generation of VCs
    Previously, proof oblications (or VCs) generated by SPARK could be slightly different from one run of SPARK tools to the other. Now, if the source files have not changed, exactly the same VCs will be generated. This is useful if external tools are used to track or cache such VCs.

  • GNAT Pro
    Mar 21st, 2016

    More accurate C binding for qualified parameters
    The C and C++ bindings generated by means of the -fdump-ada-spec option now use a more accurate formal type for qualified pointer parameters.

  • GNAT Pro | GPS | GNATbench
    Mar 18th, 2016

    GPS: Preference for tab orientation
    New preference added to configure default tab orientation. This allows, for example, to put tabs horizontally at right side of a window.

  • GNAT Pro
    Mar 18th, 2016

    Debugger backtraces in exception frames on arm-elf
    GDB is now able to unwind and display backtraces after interrupt or hardware exception frames.

  • GNAT Pro | Libraries and Bindings
    Mar 18th, 2016

    Make notebook tabs orientation configurable
    New parameter in Gtkada.MDI.Configure allows controlling the orientation of the notebook tabs. Varians are Automatic, Horizontal, Bottom_To_Top and Top_To_Bottom.

  • GNAT Pro
    Mar 18th, 2016

    Remove superfluous calls to invariant checks
    Useless calls to empty type invariant procedures are not generated when assertion policy is set to Ignore.

  • GNAT Pro | GPS | GNATbench
    Mar 18th, 2016

    GPS: Preference for tab orientation
    New preference added to configure default tab orientation. This allows, for example, to put tabs horizontally at right side of a window.

  • CodePeer
    Mar 17th, 2016

    Improved access check messages
    CodePeer now generates more accurate messages related to access check (null dereference) messages.

  • GNAT Pro
    Mar 16th, 2016

    Spurious warning on useless assignment
    The compiler does not emit a warning on an assignment to a record when there is a previous reference to a subcomponent of the object (i.e. a reference of the form A.B.C) that makes use of an earlier assignment.

  • GNATCOLL.SQL: support ORDER BY in aggregates
    The Apply function now takes an additional optional argument allowing an optional ORDER BY clause to be specified for aggregates.

  • SPARK Pro
    Mar 15th, 2016

    Allow to disable steps limit
    The --level switch of GNATprove sets a steps limit, and it was previously impossible to disable this steps limit without removing the --level switch entirely. Now one can add the switch --steps=0 to the GNATprove command line invocation to keep all the settings of the --level switch and only disable the steps limit.

  • SPARK Pro
    Mar 15th, 2016

    Specific attributes as valid volatile context
    A reference to a volatile object with enabled properties Async_Writers or Effective_Reads can now safely appear as the prefix of attributes Address, Alignment, Component_Size, First_Bit, Last_Bit, Position, Size, Storage_Size.

  • GNAT Pro
    Mar 15th, 2016

    gnatpp:—no-end-id switch
    By default, gnatpp will insert the name of a program unit after "end" if it's not already there, and make sure the case matches that of the declaration. So for example, it might change "end;" to "end Some_Name;". A new switch --no-end-id disables this behavior.

  • GNAT Pro
    Mar 12th, 2016

    Improve efficiency of [de]allocation
    Efficiency of "new" and Unchecked_Deallocation is improved in simple cases (e.g. when controlled-type machinery is not needed).

  • GNAT Pro | GPRbuild
    Mar 10th, 2016

    GPRbuild supports response files during compilation
    GPRbuild, when the language is configured appropriately and the compilation command line is long, will invoke the compiler with a response file. This will avoid problems on platforms where the maximum length of the command line or of the value of an environment variable is not very high.

  • GNAT Pro
    Mar 9th, 2016

    Hardware user initialization on leon/leon3
    On leon-elf and leon3-elf, the __gnat_hw_initialize routine is called early to perform hardware initialization. The default behavior is to return immediately, but the user can redefine this routine.

  • Additions to Float_Child and Put in Gtkada.MDI
    New parameters allow controlling the position of the child as it is being put in the MDI or when it is being floated.

  • GNAT Pro
    Mar 8th, 2016

    ARM runtimes reorganization
    The ARM bareboard runtimes have been reorganized to ease their customization depending on the actual board they run on. In particular the runtime can now benefit from specs generated from CMSIS-SVD description files, and the constants depending on the MCU or the board are better identified.

  • GNAT Pro
    Mar 8th, 2016

    No_Elaboration_Code_All for Interfaces package
    To allow the safe use of Interfaces as well as System.Unsigned_Types in code executed prior to the elaboration of the runtime (such as bareboard initialization code), those packages now use pragma No_Elaboration_Code_All.

  • CodePeer
    Mar 7th, 2016

    Improved analysis of loops
    CodePeer will now, in some cases, unroll loops. This leads to generally more precise analysis and may also result in messages which refer to a specific iteration of loop as described in the CodePeer User's Guide's "Loop Unrolling" section.

  • GNAT Pro
    Mar 4th, 2016

    New metric added to gnatmetric
    New metric that counts the number of subprogram parameters is added to gnatmetric.

  • GNAT Pro
    Mar 2nd, 2016

    Relaxed restrictions on Scalar_Storage_Order
    A composite type that has an explicit attribute definition clause for Scalar_Storage_Order can now have a component that does not have such a clause, as long as the the resulting combination of scalar storage orders is valid. (In other words, confirming attribute definition clauses for Scalar_Storage_Order are no longer required in that case).

  • GNAT Pro | GPS | GNATbench
    Mar 1st, 2016

    GPS: New Python API to get Build Targets commands
    A new GPS.BuildTarget.get_command_line() method has been added in order to be able to retrieve the current command line of a specific Build Target.

  • GNAT Pro | GPS | GNATbench
    Mar 1st, 2016

    GPS: New Python API to get Build Targets commands
    A new GPS.BuildTarget.get_command_line() method has been added in order to be able to retrieve the current command line of a specific Build Target.

  • GNAT Pro | GPS | GNATbench
    Mar 1st, 2016

    GPS: New Pythin API to get Build Targets commands
    A new GPS.BuildTarget.get_command_line() method has been added in order to be able to retrieve the current command line of a specific Build Target.