Development Log in January 2017.

  • SPARK Pro
    Jan 31st, 2017

    New switch—no-inlining prevents inlining for proof
    The special inlining used in GNATprove to increase the precision of proof may be harmful in some cases, as it increases precision at the cost of longer running time and greater memory usage. GNATprove now supports no inlining under switch --no-inlining.

  • GNAT Pro | GPRbuild
    Jan 30th, 2017

    New attribute Install_Project in package Install
    This new attribute controls whether to install a project file together with the sources and/or objects and libraries.

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

    GPS: Changing perspective from main toolbar
    GPS now includes a new button to the right of the main toolbar, to let users easily switch perspectives.

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

    GPS: changing perspective from main toolbar
    GPS now includes a new button to the right of the main toolbar, to let users easily switch perspectives.

  • GNATCOLL.SQL.SQLITE: support for URI filenames
    Support for sqlite's URI filename has now been added, via a new parameter to GNATCOLL.SQL.Sqlite.Setup

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Fixed_Equality_Checks
    A new rule named Fixed_Equality_Checks is added to gnatcheck. It flags all calls to the predefined equality operations for fixed- point types.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Unchecked_Address_Conversions
    A new rule named Unchecked_Address_Conversions is added to gnatcheck. It flags instantiations of Ada.Unchecked_Conversion where the actual for the formal type Source is the System.Address type (or a type derived from it), and the actual for the formal type Target is an access type.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule POS_On_Enumeration_Types
    A new rule named POS_On_Enumeration_Types is added to gnatcheck. It flags the 'Pos attribute in cases where the attribute prefix denotes an enumeration type (including types derived from enumeration types).

  • GNAT Pro
    Jan 28th, 2017

    New rule Enumeration_Representation_Clauses
    A new rule named Enumeration_Representation_Clauses is added to gnatcheck. It flags enumeration representation clauses.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Unchecked_Conversions_As_Actuals
    A new rule named Unchecked_Conversions_As_Actuals is added to gnatcheck. It flags a call to an instantiation of Ada.Unchecked_Conversion used as an actual in procedure or entry call or given as a default value in a subprogram or entry parameter specification.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Deriving_From_Predefined_Type
    A new rule named Deriving_From_Predefined_Type is added to gnatcheck. It flags a derived type declaration when the ultimate ancestor type is a predefined Ada type.

  • GNAT Pro
    Jan 28th, 2017

    New rule Default_Values_For_Record_Components
    A new rule named Default_Values_For_Record_Components is added to gnatcheck. It flags record component declarations that have default expressions.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Objects_Of_Anonymous_Types
    A new rule named Objects_Of_Anonymous_Types is added to gnatcheck. It flags any object declaration located immediately within a package declaration or a package body (including generic packages) when the object declaration has an anonymous access or array type definition.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Uninitialized_Global_Variables
    A new rule named Uninitialized_Global_Variables is added to gnatcheck. It flags object declarations located immediately within a package declaration, a generic package declaration, or a package body, when they do not have explicit initializations.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Nested_Subprograms
    A new rule named Nested_Subprograms is added to gnatcheck. It flags any subprogram declaration, subprogram body declaration, subprogram instantiation, expression function declaration, or subprogram body stub that is not a completion of another subprogram declaration and that is declared within a subprogram body (including bodies of generic subprograms), task body, or entry body directly or indirectly (that is, possibly within a local nested package).

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Binary_Case_Statements
    A new rule named Binary_Case_Statements is added to gnatcheck. It flags a case statement if this statement has only two alternatives, one containing exactly one choice, and the other containing exactly one choice or the OTHERS choice.

  • GNAT Pro
    Jan 28th, 2017

    New gnatcheck rule Null_Paths
    A new rule named Null_Paths is added to gnatcheck. It flags a statement sequence that is a component of an if, case, or loop statement when this sequence consists entirely of null statements.

  • GNAT Pro
    Jan 27th, 2017

    New parameter for Identifier_Suffixes gnatcheck rule
    A new parameter Access_Obj_Suffix is added to the gnatcheck Identifier_Suffixes rule. It allows specifying suffixes for objects of access types to be checked.

  • GNATCOLL.Traces add support for prefix decorators
    These decorators can be used to add information at the beginning of each log line, before the indentation and the name of the trace handle. Such information will always be aligned, so it might be convenient to display timestamps for instance.

  • SPARK Pro
    Jan 25th, 2017

    SPARK tools produce more information about VCs
    Previously, it was hard to see which VCs were produced for a given check, and which prover was used to attempt to prove it. Now, this information is stored in the .spark files that are produced by GNATprove. The content of these files is now documented.

  • SPARK Pro
    Jan 23rd, 2017

    New lemmas on monotonicity of float operators
    The SPARK lemma library includes six new lemmas on the monotonicity of the float addition, substraction, multiplication and division.

  • GNAT Pro
    Jan 20th, 2017

    Ability to check removal of Ghost code in object
    The names of Ghost entities in the objects and executables are now uniquely prefixed with "___ghost_" (three leading underscores). This makes it possible to independently check the removal of Ghost code by the compiler when generating the final executable with Ghost assertion policy of Ignore (the default).

  • GNAT Pro
    Jan 18th, 2017

    Better warnings for suspicious postconditions
    Postconditions (and consequences of contract cases) that do not refer to the post-state of the subprogram are suspicious, as they should either be preconditions, or another expression was meant to be checked. Originally only full postconditions were checked, now all conjuncts in a conjunction of Boolean sub-expressions are individually checked for such issues.

  • GNAT Pro
    Jan 17th, 2017

    Relaxed and strict secondary stack management
    The compiler now employs two different schemes of managing the secondary stack - relaxed and strict. In relaxed mode, a context which uses the secondary stack will no longer manage it if there exists an enclosing construct which already does that. This behavior cannot propagate beyond packages and subprograms. Relaxed mode is the default mode of secondary stack management. In strict mode, any context which uses the secondary stack will manage it unconditionally. This behavior can be enabled by switch -gnatd.s.

  • GNAT Pro
    Jan 13th, 2017

    Reduce -Wstack-usage false positives with strings
    The number of false positives reported by the compiler for the -Wstack-usage warning on strings or arrays has been reduced.

  • SPARK Pro
    Jan 12th, 2017

    Check default of private types at declaration
    GNATprove now checks that no runtime error can occur during the default initialization of private types once and for all at the declaration of the type. This enforces a cleaner separation of library code from user code, allowing for an easier integration of proof with other verification means (tests, review...).

  • GNAT Pro
    Jan 9th, 2017

    Do not emit unit version on bare board platforms
    On bare board platforms, units versions for Version and Body_Version attributes are not emitted anymore when not needed.

  • SPARK Pro
    Jan 6th, 2017

    Support for arbitrary lengths of entry queues
    GNATprove now supports arbitrary lengths of entry queues (which are specified by the Max_Queue_Length and Max_Entry_Queue_Length pragmas). This feature is only applicable when the GNAT Extended Ravenscar profile is active.

  • SPARK Pro
    Jan 5th, 2017

    Add message on proved termination
    When GNATprove is able to prove a Terminating annotation an info message is issued.

  • SPARK Pro
    Jan 5th, 2017

    Support of caching using memcached server
    The SPARK tools now support caching large parts of the analysis via a memcached server. If a memcached server is available to store analysis results, and this server is specified to GNATprove via the command line option --memcached- server=hostname:portnumber, then subsequent invocations of the tools, even across different machines, can store intermediate results of the tools. The user-visible effect is that GNATprove can produce results faster.

  • GNAT Pro | GPRbuild
    Jan 5th, 2017

    New GPRname switch—ignore-duplicate-files
    GPRname has a new switch --ignore-duplicate-files which will ignore identical basenames when scanning for sources. In addition, a warning is now emitted by default when not using this switch to warn about potential conflicts when duplicate filenames are found.

  • GNAT Pro
    Jan 3rd, 2017

    Improved debug information for enumeration types
    In its DWARF output, GNAT now generates DW_AT_encoding attributes for all DW_TAG_enumeration_type DIEs. These describe the signedness of the corresponding enumeration types, allowing precise interpretation of subranges.

  • GNAT Pro
    Jan 2nd, 2017

    No_Inline is a legal aspect name
    The GNAT-specific pragma No_Inline is now accepted as a legal aspect name, in analogy with the Ada aspect No_Return.