Development Log in June 2015.

  • SPARK Pro
    Jun 26th, 2015

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

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

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

  • SPARK Pro
    Jun 19th, 2015

    Better progress bar in graphical interface
    SPARK now provides better progress information when the --ide-progress-bar switch is used, so that the progress bar in graphical interfaces can convey this information to the user.

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

  • GPRbuild
    Jun 18th, 2015

    Value of Runtime when—RTS= is specified
    When --RTS= is specified for a language on the command line, the value of attribute reference 'Runtime (<language>) is the value specified by the switch --RTS=, even when attribute Runtime (<language>) has been declared.

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

  • 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

    Restrictions to refine No_Implicit_Heap_Allocations
    Two new restrictions have been added: No_Implicit_Task_Allocations and No_Implicit_Protected_Object_Allocations. They could be used to refine the wider No_Implicit_Heap_Allocations restriction.

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

  • GPS | GNATbench
    Jun 10th, 2015

    GB: use selected project as project to convert
    When running "convert to ada..." action, use current selected project as project to convert initial value.

  • GNAT Pro
    Jun 10th, 2015

    Sanitizer libraries on GNU/Linux native platforms
    Native x86 and x86_64 Linux toolchains now come with a family of "Sanitizer" libraries that can help with the debugging or anticipation of various run-time misbehaviors in an application. The "Address Sanitizer" library, for example, tracks and reports memory management hazards such as buffer overruns (including on static arrays), multiple deallocations or memory leaks. Taking advantage of this library simply requires to compile and link with -fsanitize=address.

  • GNAT Pro
    Jun 9th, 2015

    Ada exception message in catchpoint condition
    In the debugger, an Ada exception catchpoint can now be made conditional on the contents of the exception's message, whose content is available through a variable called "Message". For instance:

       (gdb) catch exception if message = "EXCEPTION_ACCESS_VIOLATION"
    

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

  • SPARK Pro
    Jun 7th, 2015

    Better support for fixed-point division
    The SPARK toolset now supports division of fixed-point values when the result type is integer and both operands have the same base type.

  • 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
    Jun 2nd, 2015

    Better error recovery for misplaced access keyword
    The compiler provides a meaningful error message when the keywords constant and access are interchanged in an access discriminant specification.

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