Development Log in October 2016.

  • SPARK Pro
    Oct 31st, 2016

    Nested loops allowed before a loop (in)variant
    A limitation in GNATprove forbade nested loops before loop (in)variants. This limitation has been removed.

  • SPARK Pro
    Oct 27th, 2016

    Better handling of always-fail subprograms
    Subprograms where all possible execution paths end in an exception are now dealt with in a more obvious fashion. Instead of raising many checks and warnings, we now emit only a single high check indicating that no path will return normally.

  • SPARK Pro
    Oct 26th, 2016

    Improve tracking of bounds of array aggregates
    GNATprove now does a better job of tracking the bounds of aggregates of dynamic array types, resulting in more discharged checks on array aggregates.

  • GNAT Pro
    Oct 25th, 2016

    Minimize useless body compilations when inlining
    A filter has been added to the inlining / instantiation circuitry to recognize package bodies that do not contain bodies of inlined functions or generic bodies being instantiated, and that therefore do not need to be compiled, even though their declarations may appear in the context of other units that are needed for inlining.

  • GNAT Pro
    Oct 24th, 2016

    Better RM 6.3.1 (8-13) rules violation error message
    RM 6.3.1 (8) specifies that an inherited primitive of a type derived from a generic formal with unknown discriminants has convention intrinsic. As a result, access subprogram parameters of such an operation are also intrinsic, and the corresponding actual cannot be an access attribute reference. The new error message warns on the inherited subprogram before rejecting the attribute reference.

  • SPARK Pro
    Oct 20th, 2016

    level switch uses time limit instead of step limit
    The level switch used to provide a high level way of tuning the verification condition now sets time limits instead of step limits for provers. As a result, this switch is more predictable, as it always allows each prover to run for the same amount of time, but less deterministic, as the time needed for a prover to complete a proof may vary depending on the computer.

  • GNAT Pro | GPS | GNATbench
    Oct 19th, 2016

    GPS: resize Debugger Data items when pref changes
    When the preferences that control the maximum size of items are changed in the Preferences/Debugger dialog, this immediately impacts already displayed items in the Debugger Data view.

  • GNAT Pro | GPS | GNATbench
    Oct 19th, 2016

    GPS: resize Debugger Data items when pref changes
    When the preferences that control the maximum size of items are changed in the Preferences/Debugger dialog, this immediately impacts already displayed items in the Debugger Data view.

  • GNAT Pro | GPS | GNATbench
    Oct 18th, 2016

    GB: add library pages to GPR file creator
    During the execution of commands "new Ada project" or "convert to Ada project", the GPR file creation wizard is displaying two new pages when the user asks for a library GPR file. These pages allow configuring library attributes.

  • GNAT Pro | GPS | GNATbench
    Oct 18th, 2016

    GB: add library pages to GPR file creator
    During the execution of commands "new Ada project" or "convert to Ada project", the GPR file creation wizard is displaying two new pages when the user asks for a library GPR file. These pages allow configuring library attributes.

  • GNAT Pro
    Oct 14th, 2016

    gnatpp: Improved formatting with—par_threshold=0
    If --par_threshold=0 is specified, and --no-separate-is is not specified, then the "is" of a parameterless procedure is placed on a separate line.

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

    GPS: remove entity information in Project view
    We no longer display the list of entities defined in a file, in the Project view. This information is already available in the Outline, whenever a file is selected in the Project view. Removing it allowed us to speed up the display of the tree view.

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

    GPS: remove entity information in Project view
    We no longer display the list of entities defined in a file, in the Project view. This information is already available in the Outline, whenever a file is selected in the Project view. Removing it allowed us to speed up the display of the tree view.

  • GNAT Pro
    Oct 12th, 2016

    AI12-0127 implementation, partial aggregate notation
    Ada Issue AI12-0127, part of the Ada2012 amendment, describes a new constructor for aggregates, in terms of an existing record or array object, and a series of component-wise modifications of its value, given by named associations for the modified components. To use this feature the compilation flag -gnat2020 must be specified.

  • CodePeer
    Oct 8th, 2016

    No False Positive mode
    Significant work has been done to reduce the number of false alarm messages (also known as false positives) when using the -messages min switch. This is also the default when using -level 0, -level 1 and -compiler-mode switches. In this mode, only messages which are the most likely to be real errors are generated.

  • GNAT Pro
    Oct 1st, 2016

    AI12-0125, left-hand side of assignment abbreviation
    Ada Issue AI12-0125, part of the Ada2012 amendment, introduces the use of the character '@' as an abbreviation for the left-hand side of an assignment statement, usable anywhere within the expression on the right-hand side. To use this feature the compilation flag -gnat2020 must be specified. See motivation and examples of use at http://www.ada-auth.org/cgi- bin/cvsweb.cgi/ai12s/ai12-0125-3.txt?rev=1.12 .