Development Log

  • GNAT Pro
    Jun 30th, 2015

    Controlled types and No_Exception_Propagation
    The compiler no longer generates exception management code for the handling of controlled types when restriction No_Exception_Propagation is active.

  • SPARK Pro
    Jun 26th, 2015

    Constant can now appear in contracts
    The SPARK toolset now allows for costants with variable input to appear in flow-related contracts. This allows for more precise information flow analysis.

  • GNAT Pro
    Jun 26th, 2015

    Verification of ignored Ghost code removal
    The removal of Ghost entities declared with Ghost policy Ignore along with associated code can now be verified by first compiling the code base, then searching for prefix "_ghost_" in object files. The lack of this prefix indicates that all ignored Ghost code has been sucessfully removed.

  • SPARK Pro
    Jun 25th, 2015

    Support for volatile functions
    The SPARK toolset now correctly implements the semantics of the boolean aspect volatile_function in both flow analysis and proof.

  • SPARK Pro
    Jun 24th, 2015

    Detect violations of language restrictions
    The SPARK toolset now checks settings of the pragma Restrictions before analyzing the code; previously they were only checked by the compiler.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Jun 23rd, 2015

    GPS: Navigation from race conditions report
    CodePeer's Race contitions report allows to navigate to location of access to shared object in source code.

  • GNAT Pro
    Jun 19th, 2015

    Array comparison on reconfigurable runtimes
    Comparison operations on arrays of discrete components are now allowed on ZFP and Ravenscar-SFP runtimes.

  • GNAT Pro
    Jun 18th, 2015

    New restriction - No_Task_At_Interrupt_Priority
    A new restriction No_Task_At_Interrupt_Priority has been implemented. It forbids pragma or aspect Interrupt_Priority on tasks. This restriction is enforced in Ravenscar for Cortex-M runtimes on the ARM-elf platform.

  • CodePeer
    Jun 17th, 2015

    Integration with Jenkins
    A Jenkins plug-in is now distributed with CodePeer. It provides a Build Step to configure a run of CodePeer as part of a Jenkins build.

  • GNAT Pro
    Jun 16th, 2015

    Debug info for limited class-wide objects
    The compiler now generates debug info for a limited class-wide object initialized by a function call.

  • GNAT Pro|GPRbuild
    Jun 15th, 2015

    Add variables in gprinstall’s generated projects
    Project generated with gprinstall will now contains global variables as found in the original project.

  • GNAT Pro
    Jun 12th, 2015

    UET_Address attribute removed
    The unused and internal use only attribute UET_Address has been removed.

  • SPARK Pro
    Jun 11th, 2015

    Do not generate spurious discriminant checks
    Discriminant checks were previously generated on all component accesses on discriminant records. These only correspond to an actual language check when the component is defined in a variant part. Thus, GNATprove has been improved to only generate these checks when mandated by the language.

  • SPARK Pro
    Jun 9th, 2015

    For loops on type with Iterable aspect
    The SPARK toolset now supports for loops on objects of types with the Iterable aspect specified. In particular, it is the case for loops on formal containers. Both iteration over cursors (for in) and over elements (for of) are supported.

  • SPARK Pro
    Jun 9th, 2015

    Support for iterators on arrays
    Iterators on arrays, both in loop statements and in quantified expressions, are now supported by GNATprove, except for the case of a quantified expression with an iterator over a multi dimensional array.

  • GNAT Pro
    Jun 5th, 2015

    Image function for dimensioned quantities
    The package System.Dim.float_IO now includes a function Image, that provides a string representation of a dimensioned quantity, where the numeric value is followed by the declared symbol for the corresponding unit, or the expression that enumerates its dimensions.

  • SPARK Pro
    Jun 3rd, 2015

    Improve tracking of bounds on slice assignments
    The SPARK toolset now tracks better the values of dynamic array bounds when assigning into a slice of an array, especially when this array is itself contained in a composite variable.

  • GNAT Pro|GPRbuild
    Jun 1st, 2015

    Create a symlink for the versioned libraries
    A symlink is now created on the main library directory for a library name with a version (Library_Version attribute).

  • GNAT Pro
    Jun 1st, 2015

    Suppressing checks in containers
    Two new check names, Container_Checks and Tampering_Check, are added to allow suppression of checks in Ada.Containers packages. You can put:

      pragma Suppress (Container_Checks);
    
    
    before an instantiation of (say) Ada.Containers.Vectors, and all checking code is removed. More importantly, all the controlled-type machinery involved with tampering checks is also removed. You can Suppress (Tampering_Check) to suppress just the tampering checks and machinery (which are the most expensive, and least effective at catching bugs). Suppress(All_Checks) and the -gnatp switch also work.

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

  • 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

    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.

  • GNATCOLL.Refcount: new package Shared_Pointers
    A new implementation for reference counted types is provided. It provides a more flexible API than the Smart_Pointers (since the Element_Type does not need to be a tagged type derived from Refcounted), and is faster, thanks to the use of storage pools. The API is safer since Get now returns a reference type rather than a direct access to the element. This new package is used throughout GNATCOLL, in particular GNATCOLL.SQL. In general, this has no effect on existing code.

  • 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

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

  • SPARK Pro
    Apr 30th, 2015

    Improve tracking of values of constants
    The SPARK toolset now tracks better the values of constants defined outside of the analyzed unit. This should result in better proofs, in particular for constants with a nonstatic value or aggregates containing real literals.

   1  2  3     Next »