Development Log in May 2015.

  • GNAT Pro
    May 29th, 2015

    Better error message for illegal limited view
    Compiler provides a better error message when the limited view of a type is used in a membership test in a precondition.

  • GNAT Pro
    May 28th, 2015

    Single-line hexadecimal traceback
    Hexadecimal tracebacks are given as a single line of code addresses, which makes it easier to cut&paste into an addr2line command, for example.

  • SPARK Pro
    May 27th, 2015

    Complete translation of SPARKSkein to SPARK 2014
    The SPARKSkein cryptographic hashing program originally written in SPARK 2005 (http://www.skein-hash.info/SPARKSkein-release) has now been fully translated into SPARK 2014. GNATprove proves absence of run-time errors on the new version in a few minutes. See section about it in section 6.9.3 "Multi-Units Demos" of the User's Guide for more information.

  • GNAT Pro
    May 27th, 2015

    Instrumented System.Memory can use GNAT.Debug_Pools
    Packages instrumenting System.Memory can use GNAT.Debug_Pools package to allocate memory. Dump and Reset capabilities are added to GNAT.Debug_Pools.

  • GNAT Pro
    May 27th, 2015

    New gnatcheck rule - Maximum_Parameters
    A new rule named Maximum_Parameters is added to gnatcheck. It flags variable declarations in library package and library generic package declarations.

  • GNAT Pro
    May 25th, 2015

    New gnatcheck rule - Maximum_Parameters
    A new rule named Maximum_Parameters is added to gnatcheck. It checks if a subprogram has more formal parameters than are specified by the rule parameter.

  • SPARK Pro
    May 22nd, 2015

    Suppress no effect warning when user already knows
    The SPARK toolset no longer emits a "subprogram Bla has no effect" warning when the user has added a Global/Depends aspect on Bla since this indicates that the effects of the subprogram are already known to her. The message is also suppressed when Bla is marked No_Return and is deemed to abnormally terminate.

  • GNAT Pro
    May 21st, 2015

    Set the main stack size on bareboard platforms
    It is now possible to change the size of the stack for the environment task (the main task) on bareboard platforms: just give a value to the linker symbol __stack_size. One method is to use the following linker switch: -Wl,--defsym,__stack_size=VALUE where VALUE is the size.

  • SPARK Pro
    May 21st, 2015

    Lift restriction on calls to No_Return procedures
    This lifts the SPARK RM restriction forcing calls to procedures marked No_Return to appear either at the end of a subprogram or as the only statement inside an if-statement without else/elsif part. Indeed, this restriction is not needed anymore, similarly to what was done for raise-statements already.

  • GNAT Pro
    May 21st, 2015

    Change of runtimes on powerpc-elf bareboard
    The runtimes provided for powerpc-elf bareboard now runs on mpc8641 platforms instead of PReP. The former platform is still available, high performance, while the latter has been deprecated for more than 10 years. The GNATemulator product has been updated too.

  • SPARK Pro
    May 20th, 2015

    Support for Constant_After_Elaboration
    The SPARK toolset now supports and checks that aspect Constant_After_Elaboration is indeed respected.

  • SPARK Pro
    May 20th, 2015

    Do not issue spurious warnings with—limit-subp
    When analyzing a single subprogram (typically with 'Prove Subprogram' or 'Prove Line' in an GPS or GNATbench), spurious warnings were issued on justification pragmas (pragma Annotate(GNATprove,...)) in other subprograms. This is no longer the case.

  • GNAT Pro
    May 19th, 2015

    Static object allocation with complex static size
    The compiler can now statically allocate objects declared at the library level and whose static size depends on a constant whose value is taken from a static array aggregate indexed by a character or enumeration type, as was already supported for an integer index type.

  • CodePeer
    May 18th, 2015

    Improved performance computing possible value sets
    A more efficient method for computing the union of a large number of sets is used. The observed performance difference is substantial in some cases involving large array aggregates with floating point element values.

  • SPARK Pro
    May 15th, 2015

    Allow manual proof of parts of Checks
    Previously, it was not possible to run a manual prover on a VC that represents part of a check, i.e. that was obtained by option --proof=progressive. This is now possible.

  • SPARK Pro
    May 15th, 2015

    TCP/IP in SPARK distributed as example
    An implementation of TCP/IP in SPARK is distributed now in the 'examples' of the release. This implementation based on LWIP design is targeted at bare-board embedded applications in certifiable systems. Data dependency contracts are given for most subprograms. These contracts are proved by GNATprove flow analysis, which also proves the absence of reads of uninitialized data. See the description of this example in section 6.9 'Examples in the Toolset Distribution' in SPARK User's Guide, or the README in ipstack directory.

  • SPARK Pro
    May 15th, 2015

    More examples distributed with the release
    The examples distributed with the release now include 7 small examples (a few dozen slocs), 20 medium-size examples (a single unit of a few hundred slocs at most) and 7 larger examples (of a few hundreds or thousands slocs). These examples include for example the 'Autopilot' case study distributed with John Barnes's books on SPARK 2005 and the well-known 'Tokeneer' case study commissioned by the NSA, both translated to SPARK 2014. See section 6.9 of the SPARK User's Guide 'Examples in the Toolset Distribution' for details.

  • GNAT Pro
    May 13th, 2015

    Monotonic_Clock enhanced under Android
    The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday() under Android.

  • GNAT Pro
    May 13th, 2015

    Monotonic_Clock enhanced under GNU/Linux
    The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday() under GNU/Linux.

  • GNAT Pro
    May 13th, 2015

    Iteration over container with indefinite type
    An iterable aspect can be specified for a formal container whose components are indefinite types (except for unconstrained arrays). An element loop over such containers has the usual semantics.

  • SPARK Pro
    May 12th, 2015

    Use dedicated support for arrays in SMT solvers
    The SPARK toolset now uses dedicated support for arrays when available in the underlying solver. This should result in more proofs of array properties, in particular over arrays either indexed by or containing modular types.

  • GNAT Pro
    May 7th, 2015

    SSE is enabled by default on x86 platforms
    On native x86 32-bit platforms, the code generation is now using SSE floating-point extensions by default, taking advantage of modern hardware and generating more reliable code (avoiding intermediate extra precision used by the x86 processor) and in general more efficient code. This code is also compatible with static analysis and formal verifications performed by e.g. CodePeer and SPARK.

  • GNAT Pro
    May 7th, 2015

    Optimization of predicate checks
    If the expression in a dynamic predicate aspect is free of side effects, the compiler will eliminate redundant calls to the corresponding function, when code is compiled with inlining and high optimization (-gnatn -O3).

  • QGen
    May 6th, 2015

    Project P Open Workshop

    Project P is a three-year research project funded within the French FUI 2011 funding framework. It sees the collaboration of major industrial partners (Airbus, Astrium, Continental, Rockwell Collins, Safran, Thales), SMEs (AdaCore, Altair, Scilab Enterprise, STI), service companies (ACG, Aboard Engineering, Atos Origins) and research centers (CNRS, ENPC, INRIA, ONERA).

    With the project now drawing to an end comes the final presentation of all the work that has been produced over the past 3 years...

    Continental France, Project P leader, and all the project partners are pleased to invite you to the presentation of the final results of Project P.

  • SPARK Pro
    May 6th, 2015

    Better reporting of incorrect prover configuration
    Previously, when there where problems running external provers, GNATprove would silently consider the runs as simply "not proved". This could happen with user-provided configuration of external provers, for example using the "--why3-conf" command-line switch. Now, the SPARK toolset reports such problems explicitly as warnings.

  • GPS | GNATbench
    May 5th, 2015

    GPS: recent searches in view filters
    The filters that exist in some views now remember recent searches, so that you can repeat them more easily.

  • GPS | GNATbench
    May 5th, 2015

    GPS: remove support for title bars for views
    We removed a few preferences in the "Windows" section related to the support for title bars in views. This simplifies the preference dialog.

  • GNAT Pro
    May 5th, 2015

    Implement workaround for AT697F trap errata
    The LEON run-time libraries have been enhanced to work around the issue present in the AT697F processor and documented in the errata sheet 41003B-AERO-07/14 that causes unexpected clearing of interrupts.

  • GPS | GNATbench
    May 4th, 2015

    GPS: the speed bar is drawn on top of the scrollbar
    The speed bar has been removed, thus saving some horizontal space: the information of highlights in the editor is now drawn directly on top of the vertical scrollbar.

  • CodePeer
    May 2nd, 2015

    Tooltips for possible values of variables
    CodePeer generates information about possible values of variables and expressions during its analysis, which is now displayed in the GPS source editor as an information tooltip.

  • GNAT Pro
    May 2nd, 2015

    Improved message for bad last bit value
    The error message for violation of the RM 13.5.1(10) rules about the allowed value of last bit is improved (it is the last bit + 1 value, not last bit itself, that must meet the criteria).

  • CodePeer
    May 1st, 2015

    Generation of backtraces on messages
    CodePeer now generates by default detailed information about places in the source code involved in a particular check-related message, making it easier to analyze such messages and identify possible errors in the source. This extra information is displayed by GPS in a new view.

  • GNAT Pro
    May 1st, 2015

    Avoid use of secondary stack
    Use of the secondary stack, and the corresponding cleanup handlers, is avoided in many cases. For example, access discriminants no longer force functions to return on the secondary stack. This is a speed improvement. It is particularly relevant to the Ada.Containers.