Development Log

  • GNAT Pro
    Sep 19th, 2017

    New gnatcheck rule Specific_Type_Invariants
    This rule flags definitions of (non-class-wide) Type_Invariant aspects that are parts of tagged type declarations.

  • GNAT Pro
    Sep 19th, 2017

    New gnatcheck rule Specific_Type_Invariants
    This rule flags definitions of (non-class-wide) Type_Invariant aspects that are parts of tagged type declarations.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule Specific_Pre_Post
    This rule flags each Pre and Post aspect that is a part of an explicit declaration of a primitive operation of a tagged type. Pre'Class and Post'Class aspects are not flagged.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule Constructors
    This rule flags any declaration of a primitive function of a tagged type that has a controlling result and no controlling parameter. If a declaration is a completion of another declaration then it is not flagged.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule No_Inherited_Classwide_Pre
    This rule flags a declaration of an overriding primitive operation of a tagged type if at least one of the operations it overrides or implements does not have any (explicitly defined or inherited) Pre'Class attribute defined for it.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule Printable_ASCII
    This rule flags characters in source code that are not part of the printable ASCII character set.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule Deep_Library_Hierarchy
    This rule flags any library package declaration, library generic package declaration, or library package instantiation that has more than N parents and grandparents (that is, the name of such a library unit contains more than N dots), where N is a rule parameter.

  • GNAT Pro
    Sep 18th, 2017

    New gnatcheck rule Too_Many_Dependencies
    This rule flags a library item or a subunit that immediately depends on more than N library units (where N is a rule parameter). In the case of a dependency on a child unit, implicit and explicit dependencies on the child unit's parents are not counted.

  • GNAT Pro
    Sep 18th, 2017

    New parameter for gnatcheck rule Metrics_LSLOC
    A new optional parameter Subprograms is added to the gnatcheck Metrics_LSLOC rule. This parameter allows restricting checks made by this rule to subprogram bodies only.

  • GNAT Pro | GPS | GNATbench
    Sep 15th, 2017

    GPS: Display format of variables in the Variables view
    The format (display base) of variables can now be controlled via the contextual menu in the Variables view.

  • GNAT Pro
    Sep 14th, 2017

    New gnatcheck rule Representation_Specifications
    This rule flags aspect_clauses (formerly known as representation_clauses) and aspect_specifications that define representation aspects.

  • GNAT Pro
    Sep 14th, 2017

    New gnatcheck rule Expression_Functions
    This rule flags definitions of expression functions in package specifications (including generic packages).

  • GNAT Pro
    Sep 14th, 2017

    New gnatcheck rule Subprogram_Access
    This rule flags access_to_subprogram_definitions and access_definitions that define access-to-subprogram types.

  • GNAT Pro
    Sep 14th, 2017

    New gnatcheck rule Downward_View_Conversions
    This rule flags downward view conversions.

  • CodePeer
    Sep 12th, 2017

    Improved handling of nested recursive subprograms
    Some cases of nested recursive subprograms could result in CodePeer issuing messages about too many iterations, terminating analysis of the subprograms. CodePeer now does a better job of processing such subprograms.

  • GNAT Pro | GPS | GNATbench
    Sep 12th, 2017

    GPS: EUC-JP encoding support
    GPS can now edit files in the EUC-JP encoding.

  • GNAT Pro | GPS | GNATbench
    Sep 11th, 2017

    GPS: GPS traces are no longer buffered
    The GPS traces are no longer buffered, to avoid losing useful information in the log files.

  • GNAT Pro
    Sep 8th, 2017

    Better error messages when loading sources
    Compiler provides more descriptive error output in the case where a source file has bad permissions (no read access).

  • CodePeer
    Sep 5th, 2017

    Simple access to the GNAT target runtime
    CodePeer will now automatically find the GNAT target runtime specified in a project file by simply putting the target GNAT compiler in your PATH. You no longer need to copy the runtime directory into the CodePeer installation.

  • GNAT Pro
    Sep 1st, 2017

    Prebuilt version of XMLAda in GNAT Pro for VxWorks
    It is no longer necessary to build XMLAda from sources in order to use this add-on, as it now comes prebuilt in GNAT Pro for all VxWorks platforms.

  • GNAT Pro | GPRbuild
    Aug 31st, 2017

    New switches—no-project for gprbuild and gprclean
    A new command line only switch --no-project is added to gprbuild and gprclean. When this switch is used, the project file used by the tool is the default one in <prefix>/share/gpr/_default.gpr.

  • GNAT Pro
    Aug 30th, 2017

    New warning for ineffective use clauses
    Compiler's support for detecting unused entities (-gnatwu) has been extended to properly identify useless or "ineffective" use- type and use-package clauses.

  • GNAT Pro | GPS | GNATbench
    Aug 30th, 2017

    GPS: Menu separators more visible in dark themes
    The menu separators have been made more visible in dark themes.

  • GNAT Pro
    Aug 30th, 2017

    More aggressive inlining of expression functions
    Expression functions are now inlined more aggressively when optimization is enabled, overriding most of the usual heuristics.

  • SPARK Pro
    Aug 28th, 2017

    SPARK’s way of finding runtimes has been improved
    Previously, extra setup was required to make SPARK work with a non-default runtime, even when the project file contained all the information. Now, SPARK uses the same mechanism to find the runtimes as gprbuild does; as long as all required tools are installed and in the PATH, SPARK will find and use the correct runtime according to the --RTS and --target switches passed to it, or Runtime and Target attributes defined in the project.

  • GNATCOLL.Projects: support for excluded source files
    GNATCOLL.Projects now provides access to the attributes that define excluded source files (Excluded_Source_Files and Excluded_Source_List_File).

  • SPARK Pro
    Aug 23rd, 2017

    Ordering of checks for manual proof better preserved
    When manual proof is used, the order of checks is important for matching existing proofs to the checks. The SPARK tools now preserve this order better than previously. This simplifies the usage of SPARK tools when doing manual proof.

  • GNAT Pro
    Aug 22nd, 2017

    Improved performance of ‘Image for enumeration types
    The compiler generates faster code for attribute Image applied to user-defined enumeration types when the sources are compiled with optimizations enabled.

  • GNAT Pro
    Aug 22nd, 2017

    Clock on Linux is now monotonic
    The high-resolution system clock for tasking operations on Linux was previously subject to time jumps and was at the mercy of a privileged user resetting the clock and wreaking havoc with delay and sleep operations. The clock has been enhanced to be monotonic and is no longer subject to the aforementioned perturbations.

  • GNAT Pro | GPRbuild
    Aug 14th, 2017

    Wildcards in attribute Ignore_Source_Sub_Dirs
    Wildcards are now allowed in the value of attribute Ignore_Source_Sub_Dirs, allowing to exclude groups of directories from the source directories of the project.

  • GNAT Pro
    Aug 14th, 2017

    Improve type name matching in gnatdbg
    Both gnatdbg.printers.PrettyPrinter and gnatdbg.generics.Match.TypeName have been enhanced to be able to match pretty GDB type names (i.e. the result of `str(gdb_type)`) in addition to their raw names (`gdb_type.name` or `gdb_type.tag`).

  • GNAT Pro
    Aug 11th, 2017

    PolyORB: iac: ignore pragma javaPackage
    The IDL-to-Ada compiler iac now ignores pragma javaPackage. This is a convenience for those also using idlj (idl-to-java), because idlj recognizes that pragma.

  • CodePeer
    Aug 5th, 2017

    Better subprogram input annotations
    If a subprogram takes one or more components of one global object as inputs (as opposed to reading the object as a whole), CodePeer formerly omitted these from the list of inputs in the annotations generated for the subprogram. Now the global object is listed as an input. This means that if either or both of Some_Record.Field_1 and Some_Record.Field2 are global inputs to a subprogram, then Some_Record will be listed as an input.

  • GNAT Pro | GPS | GNATbench
    Aug 3rd, 2017

    GPS: Revamping of Help/GNAT Runtime menu
    GNAT runtime menu items for cross platforms have been moved into a separate submenu of Help/GNAT runtime instead of placing them after Help/About submenu.

  • GNAT Pro
    Aug 3rd, 2017

    gnatdbg: TypeName can match names with regexps
    gnatdbg.generics.Match.TypeName is now able to check that the name of input types matches a given regular expression.

  • GNAT Pro
    Aug 3rd, 2017

    gnatdbg: TypeName can recurse on basis types
    gnatdbg.generics.Match.TypeName is now able to recurse on basis types (typedef'd types or integer sub-range basis type) in order to find one type that matches the given name.

  • GNAT Pro
    Jul 30th, 2017

    More accurate C binding for enumerals and constants
    The C and C++ bindings generated by means of the -fdump-ada-spec option can now use a more accurate Ada type for enumeral types and support the declaration of const-qualified variables.

  • GNAT Pro | GPRbuild
    Jul 27th, 2017

    Directory of gprbuild added to the PATH
    When gprbuild is invoked, it now adds the directory of its executable to PATH, so that gprconfig can be found when using auto-configuration.

  • GNAT Pro
    Jul 24th, 2017

    Efficient array reset for all elementary types
    The compiler now generates efficient code to reset a large array of any elementary component type to zeros, or an equivalent value for the component type, so now includes arrays of floating-point and access values instead of being limited to arrays with a discrete component type.

  • SPARK Pro
    Jul 21st, 2017

    Conversion between arrays with different components
    GNATprove now supports conversion between array types with different component types as long as the component types are statically matching (as allowed by the Ada RM).

  • GNAT Pro
    Jul 21st, 2017

    Pragma Ada_2020
    Pragma Ada_2020 can be used to enable Ada 2020 features that have been implemented in GNAT. Ada_2020 is a configuration pragma. This is in addition to the -gnat2020 command-line switch.

  • SPARK Pro
    Jul 19th, 2017

    Automatically unroll static loops w/o loop invariant
    Loop invariants are a known difficulty for beginners to use formal program verification. At the same time, many loops written in exercises and to familiarize oneself with the technology have static bounds and a small range. This enhancement implements loop unrolling for such loops with static bounds and not too many iterations (current threshold is at 20 iterations maximum). This way, simple loops with static bounds are proved without requiring a loop invariant. We let the user decide if she wants to use this feature or not: - by only unrolling FOR loops that have no loop (in)variant. - by disabling this feature when the switch --no-loop-unrolling is used.

  • GNAT Pro | GPRbuild
    Jul 18th, 2017

    Object files in alphabetical order in libraries
    To be able to reproduce the same executable and libraries on different machines, the object files are put in libraries in alphabetical order of their path names.

  • GNAT Pro
    Jul 11th, 2017

    New gnatcheck rule Downward_View_Conversions
    This rule flags downward view conversions.

  • GNAT Pro
    Jul 10th, 2017

    New gnatcheck rule Printable_ASCII
    This rule flags characters in source code that are not part of the printable ASCII character set.

  • GNAT Pro
    Jul 7th, 2017

    New gnatcheck rule No_Inherited_Classwide_Pre
    This rule flags a declaration of an overriding primitive operation of a tagged type if at least one of the operations it overrides or implements does not have any (explicitly defined or inherited) Pre'Class attribute defined for it.

  • GNAT Pro | GPS | GNATbench
    Jul 5th, 2017

    GPS: New API to create nested messages
    A python method create_nested_message has been added to the GPS.Message class, to create nested messages.

  • GNAT Pro
    Jul 3rd, 2017

    New gnatcheck rule Specific_Pre_Post
    This rule flags each Pre and Post aspect that is a part of an explicit declaration of a primitive operation of a tagged type. Pre'Class and Post'Class aspects are not flagged.

  • GNAT Pro | GPS | GNATbench
    Jul 3rd, 2017

    GPS: Auto fix for Range attribute usage
    The compiler is clever enough to detect that the Range attribute should be used to loop over the content of an array. GPS now offers an autofix for such warnings.

  • GNAT Pro | GPRbuild
    Jul 3rd, 2017

    Improved gprconfig performance
    Gprconfig performance substantially improved by caching results of all external calls.

  • GNAT Pro
    Jun 30th, 2017

    New gnatcheck rule Specific_Parent_Type_Invariant
    This rule flags record extensions and private extensions having a parent type that specifies a Type_Invariant aspect. A record extension is not flagged when it is a completion of a private extension.

  • GNAT Pro | GPS | GNATbench
    Jun 30th, 2017

    GPS: Status indicator for source buffers
    A new status indicator has been placed in the bottom-right corner of source editors, showing whether the editor has been modified.

  • SPARK Pro
    Jun 28th, 2017

    No inlining of subprograms visible to child packages
    GNATprove no longer inlines subprograms declared in private parts of package specifications as part of its "Contextual Analysis of Subprograms without Contracts" feature (which is documented in the SPARK User's Gude). Such inlining could be confusing for the users, because the same code could be provable if located in a package body, but not provable if located in a child package. As a result a spurious warning of the form "analyzing unreferenced procedure" for subprograms visible to child packages is no longer emitted.

  • GNAT Pro
    Jun 28th, 2017

    New gnatcheck rule Too_Many_Dependencies
    This rule flags a library item or a subunit that immediately depends on more than N library units (where N is a rule parameter). In the case of a dependency on a child unit, implicit and explicit dependencies on the child unit's parents are not counted.

  • GNAT Pro | GPS | GNATbench
    Jun 26th, 2017

    GPS: New action to add extended characters
    A new action "insert extended character" has been added, allowing one to enter an extended character in the editor by its unicode number.

  • GNAT Pro
    Jun 23rd, 2017

    Direct conversion from unsigned subtype to FP type
    On 32-bit RISC platforms, the compiler now generates a direct conversion from a 32-bit unsigned subtype of a 64-bit base type to a floating-point type instead of calling a dedicated routine.

  • GNAT Pro | GPS | GNATbench
    Jun 22nd, 2017

    GPS: Finer distinction in navigation contextual menu
    The "Go declaration ..." item is no longer shown when the subprogram does not have a declaration. Instead, the contextual menu only shows "Goto body ...".

  • SPARK Pro
    Jun 21st, 2017

    No checks for array conversion with static bounds
    GNATprove no longer generates length checks when converting between two static array types with equal lengths.

  • GNAT Pro
    Jun 21st, 2017

    New gnatcheck rule Numeric_Indexing
    A new gnatcheck rule Numeric_Indexing flags integer literals used as index expressions.

  • GNAT Pro
    Jun 20th, 2017

    Efficiency of Trim improved
    Ada.Strings.Fixed.Trim is now slightly faster than it was.

  • GNAT Pro
    Jun 18th, 2017

    Symbolic tracebacks without hexadecimal addresses
    New functions Symbolic_Traceback_No_Hex are added to System.Traceback.Symbolic to avoid printing hexadecimal addresses. This is useful for getting deterministic output from tests.

  • SPARK Pro
    Jun 16th, 2017

    Better handling of discriminants of protected types
    GNATprove now tracks the value of discriminants of protected types in a better way, leading to better proof results.

  • GNAT Pro
    Jun 16th, 2017

    Extended version of -gnatR for record subcomponents
    The new -gnatRe variant of the -gnatR switch makes the compiler output extended representation information for record components that are themselves records, displaying information about their subcomponents.

  • SPARK Pro
    Jun 15th, 2017

    Enable multiprocesing by default in IDEs
    When interacting with GNATprove inside GPS or GNATbench, it is desirable that the analysis uses all available cores to go as fast as possible. This is now achieved by selecting by default the "multiprocessing" mode with -j0. The user can always revert that in the analysis/proof panel opened.

  • GNAT Pro
    Jun 15th, 2017

    Refine warning on redundant comparison to True
    In many cases, comparing the value of an expression to True is a matter of preference to decide what is clearer. Thus, in such cases the use of -gnatwr may lead to spurious warnings. This is revised: GNAT now only warns on comparisons with True when the expression being compared is an object name or a simple expression involving an operator.

  • GNAT Pro | GPS | GNATbench
    Jun 14th, 2017

    GPS: Interfaces attribute in Project Properties
    The Interfaces attribute is now editable from the Library/Standalone page of the Project Properties editor.

  • GNAT Pro | GPS | GNATbench
    Jun 13th, 2017

    GPS: Key shortcuts displayed in contextual menus
    Key shortcuts are now displayed in GPS contextual menus.

  • GNAT Pro | GPRbuild
    Jun 9th, 2017

    Allow path of object file (O817-030)
    In .d dependency files for file-based languages, the beginning of the file line may be the full path of the object file, instead of its simple file name.

  • CodePeer
    Jun 8th, 2017

    Warnings suppressed on unreferenced in out formals
    CodePeer now takes pragma Unreferenced into account on formal parameters of mode in out, instead of ignoring the pragma and generating unwanted messages that suggest changing modes to in or out.

  • GNAT Pro
    Jun 8th, 2017

    More expressions allowed in Pure_Barriers
    Type conversions and subcomponents of a protected object are now allowed to be specified in entry barriers under the restriction Pure_Barriers. The following constraints apply: type conversions cannot potentially raise Constraint_Error and subcomponents cannot be selected from a prefix that is a dereferenced access value.

  • GNAT Pro | GPS | GNATbench
    Jun 7th, 2017

    GPS: Edit register values from Registers view
    While debugging, it is now possible to change the value of registers directly from within the Registers view.

  • GNAT Pro
    Jun 2nd, 2017

    New gnatcheck rule Deep_Library_Hierarchy
    This rule flags any library package declaration, library generic package declaration, or library package instantiation that has more than N parents and grandparents (that is, the name of such a library unit contains more than N dots), where N is a rule parameter.

  • CodePeer
    Jun 2nd, 2017

    Warnings suppressed on unreferenced out parameters
    CodePeer now takes into account pragma Unreferenced on an actual parameter of mode out instead of ignoring it and generating a message.

  • GNAT Pro
    Jun 1st, 2017

    New gnatcheck rule Too_Many_Primitives
    This rule flags any tagged type declaration that has more than N user-defined primitive operations (counting both inherited and not overridden and explicitly declared, but not counting predefined operators), where N is a rule parameter.

  • CodePeer
    Jun 1st, 2017

    Better handling of unused assignment messages
    When tracking review of messages from one run to another, CodePeer is now able to differentiate between multiple unused assignments of different values into the same variable in the same subprogram.

  • SPARK Pro
    May 31st, 2017

    Improve message for overridden subprograms
    When an overriding subprogram has more effects on globals variables than the overridden subprogram, GNATprove will report an error message. We have now improved this message making more explicit the underlying issue and we have reworded the case when these effects are through access types (i.e. pointers).

  • CodePeer
    May 31st, 2017

    Ada syntax is used for addresses in messages
    When codepeer generates a message which refers to the address of some entity named Foo, the message text is now "Foo'Address" in cases where previous versions of CodePeer generated "&Foo".

  • GNAT Pro
    May 30th, 2017

    New parameter for gnatcheck rule Metrics_LSLOC
    A new optional parameter Subprograms is added to the gnatcheck Metrics_LSLOC rule. This parameter allows restricting checks made by this rule to subprogram bodies only.

  • Postgres notification support
    Support notifications between different postgres database sessions.

  • SPARK Pro
    May 29th, 2017

    Better precision on functions returning tagged types
    GNATprove now tracks better the value of the tag of the result of function calls. This will lead to more discharged checks on code dealing with functions returning tagged types.

  • GNAT Pro
    May 26th, 2017

    New gnatcheck rule Constructors
    This rule flags any declaration of a primitive function of a tagged type that has a controlling result and no controlling parameter. If a declaration is a completion of another declaration then it is not flagged.

  • GNAT Pro | GPRbuild
    May 26th, 2017

    Do not ignore sources when compiler cannot be found
    When the compiler for a language could not be found, sources of the language were ignored. This is no longer the case, but if one of these sources needs to be compiled, an error will be reported and the GPR tool will fail.

  • GNAT Pro | GPS | GNATbench
    May 25th, 2017

    GPS: Autofix removes redundant context clauses
    Autofix now removes redundant "with" clauses together with any accompanying "use" clauses.

  • GNAT Pro
    May 25th, 2017

    New function To_Ada in GNAT.Sockets
    A new function GNAT.Sockets.To_Ada supports converting externally created socket descriptors to type Socket_Type for use with other operations in package GNAT.Sockets.

  • GNAT Pro | GPS | GNATbench
    May 24th, 2017

    GPS: Autofix removes redundant context clauses
    Autofix now removes redundant "with" clauses together with any accompanying "use" clauses.

  • GNAT Pro
    May 24th, 2017

    Debug information for imported entities
    GCC now produces debug information to describe Ada entities that are imported using the Import pragma or aspect.

  • GNAT Pro
    May 23rd, 2017

    Warning on potential C++ ABI mismatch on ARM
    With -Wpsabi on ARM, the compiler now warns in corner case situations where it knows it could possibly generate wrong code for complex C++ constructs involving method calls passing vectors of composite elements as arguments. The issue warned against is a possible caller/callee disagreement about what arguments-passing convention to use, leading to crashes at run time.

  • CodePeer
    May 22nd, 2017

    Better handling of ‘Length in preconditions
    Less false positives when dealing with a 'Length attribute

  • GNAT Pro
    May 22nd, 2017

    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 | GPS | GNATbench
    May 17th, 2017

    GPS: Better default colors on Windows
    The colors used for selected items on Windows have been improved to make them more readable by default.

  • GNAT Pro | GPS | GNATbench
    May 17th, 2017

    GPS: The GNAT examples are now deployable
    GPS now asks to specify a directory for deploying GNAT examples via the HELP/GNAT/Examples menus, rather than opening examples in the location where they are installed.

  • SPARK Pro
    May 11th, 2017

    Added preconditions to standard numerical functions
    Preconditions have been added to functions from the standard numerical package Ada.Numerics.Generic_Elementary_Functions, in cases that may lead to Numerics.Argument_Error or Constraint_Error when called on actual parameters that are not suitable, like a negative input for Sqrt. This ensures that GNATprove generates corresponding precondition checks when such functions are called.

  • GNAT Pro
    May 10th, 2017

    New gnatcheck rule Subprogram_Access
    This rule flags access_to_subprogram_definitions and access_definitions that define access-to-subprogram types.

  • SPARK Pro
    May 10th, 2017

    Precise handling of dispatching calls with known tag
    GNATprove now precisely determines the subprogram called by a dispatching call when the tag is known. In particular, it is now able to use its more precise specific contract if any.

  • CodePeer
    May 9th, 2017

    Add identifier of a message to CSV output
    Add a new column Message_Id, which is an unique identifier of a finding, to CSV output.

  • GNAT Pro | GPS | GNATbench
    May 9th, 2017

    GPS: Debug/Print contextual menus reintroduced
    The Debug/Print contextual menus have been reintroduced in GPS.

  • GNAT Pro | GPS | GNATbench
    May 7th, 2017

    GPS: Debug/Print contextual menus reintroduced
    The Debug/Print contextual menus have been reintroduced in GPS.

  • GNAT Pro
    May 6th, 2017

    Warning on potential C++ ABI mismatch on ARM
    With -Wpsabi on ARM, the compiler now warns in corner case situations where it knows it could possibly generate wrong code for complex C++ constructs involving method calls passing vectors of composite elements as arguments. The issue warned against is a possible caller/callee disagreement about what arguments-passing convention to use, leading to crashes at run time.

  • GNAT Pro
    May 5th, 2017

    New gnatcheck rule Expression_Functions
    This rule flags definitions of expression functions in package specifications (including generic packages).

  • SPARK Pro
    May 5th, 2017

    Improve message for functions that could not return
    GNATprove used to emit a confusing check about initialization of functions when it could not determine if a function would return. We have now improved the message for this check. In addition, when encountering a potentially non returning function, GNATprove will now precise if the function may not return on some or on every path.