Development Log

  • CodePeer
    Apr 28th, 2016

    Further improved unchecked conversion analysis
    CodePeer now knows more about unchecked conversions involving fixed point types and enumeration types.

  • GNAT Pro
    Apr 26th, 2016

    pragma Implicit_Packing for composite components
    Pragma Implicit_Packing now works for record types that contain components of small composite types, in particular small record types.

  • GNAT Pro
    Apr 26th, 2016

    pragma Implicit_Packing for byte-packed array types
    Pragma Implicit_Packing now works for array types whose component type is a scalar with a size multiple of the storage unit but not a power of 2.

  • GNAT Pro
    Apr 25th, 2016

    Task switching while debugging a core file
    It is now possible to switch between Ada tasks when debugging a core file.

  • GNAT Pro
    Apr 25th, 2016

    Faster access to small byte-packed array types
    The code generated for accessing packed array types whose component type is a small record with a size multiple of the storage unit has been improved.

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

    GPS: proposed value of message review status
    In CodePeer message review dialog proposed value of message review status has been changed to current status of the message.

  • CodePeer
    Apr 21st, 2016

    Better default for GPS message review dialog box
    When the "CodePeer message review" dialog box comes up in GPS, the default value for the "New status" field is no longer unconditionally "Unclassified", but is instead equal to the "Current status" field. In the case of a subsequent review of an already-classified message, this means that the default action is to preserve the current status of the message as opposed to setting the status back to "Unclassified".

  • GNAT Pro
    Apr 20th, 2016

    New pragma Unused
    When applied to an entity, pragma Unused causes each read or write attempt of the entity to be flagged as a warning.

  • GNAT Pro
    Apr 20th, 2016

    Added GNATcheck usage example
    An example demonstrating the use of GNATcheck coding standard verifier has been added to the distribution.

  • SPARK Pro
    Apr 17th, 2016

    More flexible elaboration rules with static model
    GNATprove now implements a more flexible enforcement of SPARK elaboration rules, that does not always requires Elaborate_All for calls and reads of subprograms and variables defined in other units during elaboration. Specifically, when the static elaboration model of GNAT is used (i.e. when neither switch -gnatE nor pragma Elaboration_Checks (Dynamic) are used), the more powerful mechanism of the compiler is used to compute a safe elaboration order for calls across units during elaboration, and GNATprove only requires the use of Elaborate_Body on units that modify the value of library-level variables defined in the spec during the elaboration of the unit body (SPARK RM rule 7.7.1(5)).

  • GNAT Pro | GPS | GNATbench
    Apr 15th, 2016

    GPS: use Gtk dialog for open/save files
    GtkFileChooserDialog used instead dialog of GPS if system doesn't have own dialog or this forbidden in a preferences and it is local file system. It is possible to use a dialog of GPS by turn off gtk_file_selector trace setting.

  • GNAT Pro | GPS | GNATbench
    Apr 15th, 2016

    GPS: automatic fix for adding Elaborate_All pragma
    The GPS code fixing capability was enhanced to handle compiler messages such as "Elaborate_All pragma required for NAME". To fix this GPS will add pragma Elaborate_All (NAME) after corresponding with-clause in the spec or body of given compilation unit.

  • GNAT Pro | GPRbuild
    Apr 13th, 2016

    Temporary config project with autoconfiguration
    The Project Manager now creates a temporary configuration project file when in auto-configuration. This file is deleted when the tool terminates. This allows several project-aware tools invocations to work in parallel with the same object directory.

  • GNAT Pro
    Apr 13th, 2016

    Tighter array packing for small record component
    The packing of array types subject to aspect/pragma Pack and whose component type is a small record, either that contains another small record component, or that has a size in the range 33 .. 63 bits, has been improved.

  • CodePeer
    Apr 12th, 2016

    Exclude source directories from analysis
    A new project attribute Excluded_Source_Dirs in package CodePeer is available to easily exclude entire source directories from analysis.

  • CodePeer
    Apr 7th, 2016

    Creating baseline from previous runs
    It is now possible to set a previous run as the default baseline review by allowing the -baseline or -set-baseline-id switches in -output-only mode.

  • CodePeer
    Apr 7th, 2016

    Improved handling of baseline reviews
    A project now has a single baseline review, which will be used by default for all review comparisons. It can be set to the current review using the -baseline switch or set to a previous review using -set-baseline-id. Note that the default review can still be temporarily overwritten by using the -cutoff switch.

  • SPARK Pro
    Apr 7th, 2016

    More options for reporting of results
    The --report switch of the gnatprove tool now provides one more option to select from. If the option --report=provers is selected, gnatprove will show information about which provers have contributed to the proof of each check.

  • GNAT Pro | GPS | GNATbench
    Apr 5th, 2016

    GPS: different icon for disabled breakpoints
    The icons that are displayed on the side of editors to show where breakpoints are now have a different color when the breakpoint is disabled or is conditional.

  • GNAT Pro | GPS | GNATbench
    Apr 5th, 2016

    GPS: speed up search and replace
    The "search and replace all occurrences" has been sped up by a factor of seven in some cases.

  • GNAT Pro | GPS | GNATbench
    Apr 5th, 2016

    GPS: do not highlight occurrences of keywords
    The plug-in auto_highlight_occurrences.py highlights all occurrences of the word under the cursor in the whole file (possibly using smart cross reference information to only highlight the specific entity and not its homonyms). This plug-in has now learned not to highlight the language's keywords ("constant", "begin",...) which is useless and might be slow since these keywords generally occur often.

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

    GPS: Home goes to beginning or first-non-blank
    When using the Home key while in an editor (or any key bound to the action "beginning of line"), GPS will first go to the first column (as it has always done), but if you do it a second time it will then go to the first non-blank character of the line). This is a feature available in other code editors.

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

    GPS: Support for arm-sysgo-pikeos
    GPS now supports the arm-sysgo-pikeos toolchain.

  • GNAT Pro
    Apr 4th, 2016

    Optimization of Unbounded_Priority_Queues
    The efficiency of Ada.Containers.Unbounded_Priority_Queues has been improved, especially in the case where many same-priority items are enqueued.

  • GNAT Pro
    Apr 4th, 2016

    Improved warning on absolute address clauses
    The alignment warning issued on strict-alignment architectures for address clauses whose value is an absolute address is now more accurate, catches more cases and prints the alignment value.

  • GNAT Pro | GPRbuild
    Apr 1st, 2016

    New procedure Get_Closures
    A new procedure GPR.Util.Get_Closures is added. It allows to get the full paths of the sources in the Ada closures of one or several mains.

  • GNAT Pro
    Apr 1st, 2016

    Expanded support for incomplete types in profiles
    The support for incomplete types as parameter and result types introduced in Ada 2012 has been implemented for a broader range of types.

  • 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 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.

  • 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
    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.

   1  2  3     Next »