Development Log

  • GNAT Pro
    Jan 13th, 2017

    Reduce -Wstack-usage false positives with strings
    The number of false positives reported by the compiler for the -Wstack-usage warning on strings or arrays has been reduced.

  • SPARK Pro
    Jan 12th, 2017

    Check default of private types at declaration
    GNATprove now checks that no runtime error can occur during the default initialization of private types once and for all at the declaration of the type. This enforces a cleaner separation of library code from user code, allowing for an easier integration of proof with other verification means (tests, review...).

  • GNAT Pro
    Jan 9th, 2017

    Do not emit unit version on bare board platforms
    On bare board platforms, units versions for Version and Body_Version attributes are not emitted anymore when not needed.

  • SPARK Pro
    Jan 6th, 2017

    Support for arbitrary lengths of entry queues
    GNATprove now supports arbitrary lengths of entry queues (which are specified by the Max_Queue_Length and Max_Entry_Queue_Length pragmas). This feature is only applicable when the GNAT Extended Ravenscar profile is active.

  • SPARK Pro
    Jan 5th, 2017

    Add message on proved termination
    When GNATprove is able to prove a Terminating annotation an info message is issued.

  • SPARK Pro
    Jan 5th, 2017

    Support of caching using memcached server
    The SPARK tools now support caching large parts of the analysis via a memcached server. If a memcached server is available to store analysis results, and this server is specified to GNATprove via the command line option --memcached- server=hostname:portnumber, then subsequent invocations of the tools, even across different machines, can store intermediate results of the tools. The user-visible effect is that GNATprove can produce results faster.

  • GNAT Pro | GPRbuild
    Jan 5th, 2017

    New GPRname switch—ignore-duplicate-files
    GPRname has a new switch --ignore-duplicate-files which will ignore identical basenames when scanning for sources. In addition, a warning is now emitted by default when not using this switch to warn about potential conflicts when duplicate filenames are found.

  • GNAT Pro
    Jan 3rd, 2017

    Improved debug information for enumeration types
    In its DWARF output, GNAT now generates DW_AT_encoding attributes for all DW_TAG_enumeration_type DIEs. These describe the signedness of the corresponding enumeration types, allowing precise interpretation of subranges.

  • GNAT Pro
    Jan 2nd, 2017

    No_Inline is a legal aspect name
    The GNAT-specific pragma No_Inline is now accepted as a legal aspect name, in analogy with the Ada aspect No_Return.

  • CodePeer
    Dec 27th, 2016

    Improved handling of SCIL version mismatch
    When a SCIL version mismatch is detected (e.g. when using a new version of CodePeer) CodePeer will now display a simple info message and will automatically remove obsolete files, and regenerate them.

  • CodePeer
    Dec 23rd, 2016

    Incremental analysis via persistent annotations
    A beta version of incremental analysis is available where CodePeer will save the result of its full analysis on disk via the -persistent-annotations switch, allowing reuse in subsequent runs when the files are still up to date. This allows both faster re- analysis and more precise results.

  • SPARK Pro
    Dec 21st, 2016

    More precise analysis for exclusive use of entries
    Tasks were previously only allowed to call the same entry if they were using entries belonging to different (library-level) objects. Now GNATprove also accepts calls from more than one task to a single entry provided that each task uses an entry belonging to a different component of a record object.

  • GNAT Pro
    Dec 19th, 2016

    Support of extended interrupts on leon3-elf
    The ravenscar runtime can now support extended interrupts on leon3 targets, like Leon4 or UT700. User needs to edit s-bbbopa.ads to set the generated interrupt.

  • GNAT Pro
    Dec 15th, 2016

    Implement workaround for LEON3FT b-to-b store errata
    The compiler switch -mfix-ut699 has been enhanced to work around the issues present in Cobham Gaisler's UT699 LEON3FT processor and documented in the errata sheet titled "LEON3FT Stale Cache Entry After Store with Data Tag Parity Error". A new compiler switch -mfix-ut699e has also been added to work around the issues present only in the UT699E LEON3FT processor.

  • GNAT Pro | GPRbuild
    Dec 14th, 2016

    New attribute Required_Artifacts
    A new attribute Required_Artifacts has been introduced. This new attribute complements the Artifacts attribute and is very similar except that the artifacts must exist or an error is reported.

  • GNAT Pro | GPS | GNATbench
    Dec 13th, 2016

    GB: use legacy cmd when target not found in Makefile
    When running a GNATbench command (compile/build/clean/...) on a GNAT project where builds are handled by a Makefile, if the expected target is not found in the Makefile, the standard command (ie, the one used for GNAT projects where builds are not handled by a Makefile) is used instead.

  • GNAT Pro | GPS | GNATbench
    Dec 13th, 2016

    GB: use legacy cmd when target not found in Makefile
    When running a GNATbench command (compile/build/clean/...) on a GNAT project where builds are handled by a Makefile, if the expected target is not found in the Makefile, the standard command (ie, the one used for GNAT projects where builds are not handled by a Makefile) is used instead.

  • GNAT Pro | GPRbuild
    Dec 13th, 2016

    New GPRname switch—ignore-predefined-units
    GPRname has a new switch --ignore-predefined-units which will not consider any predefined Ada unit (children of Ada, Interfaces and System packages) when scanning source files.

  • GNAT Pro
    Dec 12th, 2016

    Class-wide type invariant optimization
    Subprogram calls within class-wide type invariant expressions now get resolved as primitive operations instead of being dynamically dispatched.

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

    GNATdoc: support for Ada 83 and Ada 95
    GNATdoc now supports processing Ada 83 and Ada 95 codebases, in addition to Ada 2005 and 2012.

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

    GNATdoc: support for Ada 83 and Ada 95
    GNATdoc now supports processing Ada 83 and Ada 95 codebases, in addition to Ada 2005 and 2012.

  • SPARK Pro
    Dec 9th, 2016

    Better termination error messages
    Every error message related to termination referred to a subprogram without specifying the name. This further information is now emitted.

  • GNAT Pro | GPS | GNATbench
    Dec 8th, 2016

    WB: revision controlled scenario variable settings
    Scenario variables values related to a project are stored in its .gb_project file to enable having them version controlled.

  • GNAT Pro | GPS | GNATbench
    Dec 8th, 2016

    WB: revision controlled scenario variable settings
    Scenario variables values related to a project are stored in its .gb_project file to enable having them version controlled.

  • GNAT Pro | GPRbuild
    Dec 8th, 2016

    Recognize native compiler of different architecture
    On multiarch systems, gprbuild can now recognize a native compiler of a different architecture than itself.

  • SPARK Pro
    Dec 7th, 2016

    Only check component subtype at first declaration
    GNATprove now only checks subtype indications on record components when verifying the declaration of the first record type defining this component. This avoids having multiple checks on record component subtype indications, some of which could be undischarged due to missing information.

  • CodePeer
    Dec 7th, 2016

    Support for annotations in the CSV output
    CodePeer annotations (preconditions, postconditions, global inputs and outputs, ...) can now be included in the CSV output using the -show-annotations switch (in addition to -output-msg -csv).

  • GNAT Pro
    Dec 7th, 2016

    Support in Linux for locking policies
    The Linux version now supports two additional locking policies pragma Locking_Policy (Ceiling_Locking); pragma Locking_Policy (Inheritance_Locking);.

  • GNAT Pro
    Dec 7th, 2016

    Pragma Discard_Names and exception declarations
    Pragma Discard_Names now suppresses the generation of String names for exception declarations. As a result, these names will not appear in the final binary. Note that routine Ada.Exceptions.Exception_Name will return an empty String when invoked with an exception subject to pragma Discard_Names.

  • GNAT Pro
    Dec 7th, 2016

    Ada issue AI12-0131, inheritance of Pre’Class
    AI12-0131, which is part of the Ada 2012 corrigendum 1, specifies that Pre'Class shall not be specified for an overriding primitive subprogram of a tagged type T unless the Pre'Class aspect is specified for the corresponding primitive subprogram of some ancestor of T.

  • GNAT Pro
    Dec 7th, 2016

    Reduce memory use for temporary files
    The run-time system now does a slightly better job of cleaning up some data structures used for temporary files created by Text_IO.

  • GNAT Pro
    Dec 7th, 2016

    Allow larger ppc-elf programs with mpc8641 RTS
    The ROM space available to program code and read-only data for powerpc-elf bareboard configurations with mpc8641 runtimes was unnecessarily limited to 1 MB. We relaxed this restriction, now allowing up to 32 MB instead.

  • GNAT Pro
    Dec 1st, 2016

    Constraint checks removed from tagged membership
    The compiler was generating unnecessary run-time checks (i.e. checks that cannot fail) for expressions like "X in T'Class". The same was true of type conversions like "T'Class (X)". These checks are now removed.

  • SPARK Pro
    Dec 1st, 2016

    Assume value of string literals
    GNATprove now knows precisely the value stored in a string literal which will result in more proofs when string literals are involved.

  • GNAT Pro
    Dec 1st, 2016

    Foreign thread names retained on Linux
    When foreign threads are registered with the Ada runtime on Linux, GNAT no longer changes the name of the thread to "foreign thread".

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

« Previous    1  2  3  4     Next »