Development Log in July 2014.

  • GPS | GNATbench
    Jul 31st, 2014

    GPS: CodePeer messages grouping in Locations view
    All CodePeer messages (SCIL compilation errors, warnings and checks, race conditions) are displayed in one category in Locations view.

  • SPARK Pro
    Jul 25th, 2014

    Reject derived types with new discriminants
    SPARK does not allow defining discriminants on a type deriving from a discriminated type (SPARK RM 3.7(2)). Discriminants should be inherited in that case. This is now correctly detected and rejected.

  • GNAT Pro
    Jul 25th, 2014

    Support for hash based message authentication codes
    The packages providing standard hash functions (MD5, SHA1, SHA224, SHA256, SHA384, and SHA512) now also support the computation of the corresponding HMACs. This is achieved by initializing the context with HMAC_Initial_Context instead of the default Initial_Context.

  • GPS | GNATbench
    Jul 24th, 2014

    GPS: animations in browsers
    GPS now uses animations in the browsers (call graph, project,...) when items are moved from one position to another. This helps preserve the context.

  • Ada Web Server
    Jul 23rd, 2014

    Add support for WebSocket unique identifier
    This UID can be used to reference a WebSocket without having to copy the actual object. It is possible to send messages to this specific WebSocket.

  • SPARK Pro
    Jul 23rd, 2014

    Better proof for preservation of discriminants
    The SPARK toolset now tracks non-mutable discriminants of record variables better, especially when the variables are modified in a loop or updated by a procedure call. This results in more proved verification conditions.

  • SPARK Pro
    Jul 23rd, 2014

    Use of SPARK_Mode in generics
    Aspect/pragma SPARK_Mode can now appear in generic units.

  • GNAT Pro
    Jul 23rd, 2014

    Improve warnings in -gnatVa mode
    The use of -gnatVa could cause disappearance of warnings about unmodified variables that could be constants. The warning circuitry has been enhanced so that these warnings are issued in -gnatVa mode.

  • GPS | GNATbench
    Jul 21st, 2014

    GPS: add filter in Project browser
    The project browser now has a local filter, instead of having a specialized search context in the standard search dialog.

  • GPS | GNATbench
    Jul 21st, 2014

    GPS: review call graph browser
    The call graph browser was redesigned. The rendering has changed. We no longer display the list of locations for the references (which is more usable in the Call Trees), so as to be able to display more items in the browser. Standard contextual menus related to entities are now usable in the browser.

  • GNAT Pro
    Jul 18th, 2014

    New warning on ineffective box initialization
    The compiler now warns on an aggregate component association in an object declaration, when the object is a constant and the component type does not have default value or default initialization.

  • SPARK Pro
    Jul 18th, 2014

    Better generation of globals
    The auto-generated globals are now more precise. Outputs are no longer always also considered to be inputs. Additionally, when available, state abstractions are utilized to return globals relatively to the scope of the caller (this allows for more precise warnings/errors).

  • GPRbuild
    Jul 17th, 2014

    Switch -a accepted with a warning
    To ease migration from gnatmake to gprbuild, switch -a is now accepted by gprbuild. However, this switch has no other effect than to issue this warning:

       warning: switch -a is ignored and no additional source is compiled
    

  • SPARK Pro
    Jul 17th, 2014

    Better support for some bitwise operations
    The SPARK toolset now provides better proof support for right-shifts by a constant shift and for bitwise "and" with a constant. This results in more proved VCs which involve such constructs.

  • CodePeer
    Jul 17th, 2014

    Support for integer/address comparisons
    CodePeer now accepts expressions involving comparisons between System.Address and Integer values (e.g. "=", "/=", ">").

  • GPS | GNATbench
    Jul 16th, 2014

    GPS: smarter browser layout
    As part of revisiting the display in the browsers, the layout algorithm has also been improved and should result in fewer overlap of items and links.

  • SPARK Pro
    Jul 16th, 2014

    Better support of division for modular types
    Integer division on modular integer types is now better supported by the SPARK toolset, which results in more proved checks when integer division is involved.

  • GNAT Pro
    Jul 15th, 2014

    New query in Asis.Extensions (Is_Definite_Subtype)
    A new test query Is_Definite_Subtype is added to Asis.Extensions package. The query detects if the argument is a declaration of a definite subtype.

  • GPS | GNATbench
    Jul 15th, 2014

    GPS: move to previous and next entry in call tree
    Two new buttons (and the correspondings actions to which we can associate key bindings) were added to the call trees' local toolbar, to move to the next and previous location.

  • GNAT Pro
    Jul 15th, 2014

    GNATstack supports project files
    The -P option can be passed to GNATstack to automatically retrieve the GNATstack switches and stack usage information from the application.

  • GNAT Pro
    Jul 15th, 2014

    GNATstack supports—RTS switch
    The --RTS option can be passed to GNATstack to automatically retrieve the stack usage information from the run-time library.

  • GNAT Pro | GPS | GNATbench
    Jul 12th, 2014

    GPS: new action to select the current subprogram
    A new action "select subprogram" has been added to GPS, which selects the current subprogram, extending the selection to the englobing subprogram if a subprogram is already selected. This can be useful, for instance, to limit a search to the context of the current subprogram.

  • GPRbuild
    Jul 11th, 2014

    Randomized distributed job dispatching
    Now gprbuild in distributed mode will select slaves randomly instead of picking the first with some compilation slots available. This will better distribute the load over all the slaves.

  • SPARK Pro
    Jul 11th, 2014

    Better parallelism for proof with “Prove Line”
    Previously, when doing proof for a single line or check, the SPARK 2014 toolset was using only a single core. Now, it takes into account the -j command line option and may use the specified number of cores.

  • GPS | GNATbench
    Jul 11th, 2014

    GPS: new parameter on_exit to BuildTarget.execute
    The command GPS.BuildTarget.execute now accepts an extra parameter on_exit: a function which is called when the build target terminates.

  • GNAT Pro
    Jul 10th, 2014

    Untyped variables in case constructions
    It is now allowed to use single string variables that are not typed string in a case construction. When not in quiet mode, a warning is issued if there is no "when others" variant.

  • GNAT Pro
    Jul 10th, 2014

    New attribute ‘Default_Scalar_Storage_Order
    A new implementation-defined attribute has been implemented. A reference to Standard'Default_Scalar_Storage_Order (Standard is the only allowed prefix) provides the current value of the default scalar storage order (as specified using pragma Default_Scalar_Storage_Order, or equal to Default_Bit_Order if unspecified) as a static Bit_Order value.

  • GNAT Pro
    Jul 8th, 2014

    New defaults for some projects attributes
    Some project attributes have now defaults that are not empty strings or string lists. 'Object_Dir default is ".", 'Exec_Dir default is 'Object_Dir and 'Source_Dirs default is (".").

  • GNAT Pro
    Jul 8th, 2014

    Ignore Check_Float_Overflow if Machine_Overflows
    The Check_Float_Overflow pragma, and the -gnateF switch, are ignored on targets which do hardware overflow checking in any case. This allows the use of the pragma on such machines without generating inefficient checking code, making it more convenient for testing such code on a machine which normally generates infinities.

  • GNAT Pro
    Jul 7th, 2014

    Eliminate space before +Inf for float image
    The image of an infinite floating-point value (returned by the Image attribute) includes a space before +Inf, but that leads to ugly and inconsistent formatting, so that space is now removed. We prefer to include the + explicitly in this case to emphasize that it is a positive infinity, but the + belongs in the space reserved normally for a minus sign.

  • SPARK Pro
    Jul 7th, 2014

    Ignore dynamic predicates and type invariants
    SPARK toolset now issues a warning on dynamic predicates and type invariants in the code, and proceeds with analysis as if they were not in the code, instead of issuing an error that would prevent any analysis.

  • GPRbuild
    Jul 5th, 2014

    Add build master id in log message
    A unique id in front of all log messages is now output by gprslave. This make it is easier to find all log for a specific build.

  • GPS | GNATbench
    Jul 4th, 2014

    GPS: allow wider omni-search field
    A new setting allows users to chose the size of the omni-search field. On large screens, it can now display long file names more conveniently.

  • GNAT Pro
    Jul 3rd, 2014

    Package IDE accepted in all project files
    The package IDE is now accepted in all the project files, including aggregate and aggregate library projects.

  • SPARK Pro
    Jul 3rd, 2014

    Better proof with variables initialized by default
    The SPARK toolset now assumes default initialization for variables with no explicit initialization. This results in more proved verification conditions.

  • CodePeer
    Jul 3rd, 2014

    New checks for parameter aliasing on calls
    CodePeer now attempts to create preconditions for cases where a subprogram might have unwanted aliasing between a composite formal parameter and other parameters or global variables. This can result in messages about possible "aliasing check" violations on calls (and potentially within subprograms when preconditions aren't successfully created).

  • GPS | GNATbench
    Jul 2nd, 2014

    GB: SPARK2014 Traces support
    Selecting a SPARK2014 Problem marker having an associated trace, highlight the source lines containing a trace. Selecting again the same marker hides the highlighted lines.

  • SPARK Pro
    Jul 1st, 2014

    Limit analysis to a single check
    GNATprove's analysis can be limited to single checks with the new --limit-line format (--limit-line=file:line:column:checkkind) or through GPS' SPARK contextual menu "Prove Check".