Development Log in December 2014.

  • GNAT Pro
    Dec 28th, 2014

    Eliminate false warnings for unused entities
    If no entities of a package are directly used, but the package is used as a generic actual parameter, the compiler could still give a warning that no entities of the package were used. These unhelpful warnings have now been eliminated.

  • GNAT Pro
    Dec 26th, 2014

    More complete warnings in validity checking mode
    In some cases, the warning about a variable not being modified (so that it could be a constant) gets lost if validity checking is turned on. This warning is now given in validity checking mode.

  • GNAT Pro
    Dec 23rd, 2014

    Warning for suspicious Subprogram’Access
    A warning is now given for P'Access, where P is a subprogram in the same package as the P'Access, and the P'Access is evaluated at elaboration time, and occurs before the body of P. For example, "X : T := P'Access;" would allow a subsequent call to X.all to be an access-before-elaboration error; hence the warning. This warning is enabled by the -gnatw.f switch.

  • SPARK Pro
    Dec 19th, 2014

    More automated proof on conversions to float
    Proof automation has been improved on code that converts between integers and floats.

  • GPRbuild
    Dec 18th, 2014

    Linking with—lto=nn when -jnn and—lto are used
    When gprbuild is invoked with -jnn (nn > 1) and with the linker switch --lto (or -flto), the linker is invoked with --lto=nn (or -flto=nn) to speed up linking.

  • SPARK Pro
    Dec 17th, 2014

    Warning on misuse of attribute Update
    A common mistake when using attribute Update in postconditions or loop invariants is to forget to use it in combination with attribute Old or Loop_Entry, which results in nonsensical expressions of the form

       X = X'Update(...)
    
    instead of the intended (in a postcondition)
       X = X'Old'Update(...)
    
    or (in a loop invariant)
       X = X'Loop_Entry'Update(...)
    
    GNAT and GNATprove now issue a warning by default on the nonsensical form, controlled with warning switches -gnatw.t/-gnatw.T

  • SPARK Pro
    Dec 17th, 2014

    Add search path for project files
    The GNATprove tool now has a commandline option "-aP" similar to the same option of gprbuild, which allows to add search paths for the location of project files.

  • GNAT Pro
    Dec 16th, 2014

    Simplified code in Delay_Until in Ravenscar Cert
    The implementation of delay until operations in the Ravenscar Cert runtime library for Vxworks Cert has been greatly simplified since many conditions cannot occur under the Ravenscar restrictions.

  • SPARK Pro
    Dec 15th, 2014

    Subprograms without exports no longer ineffective
    Flow analysis used to flag calls to subprograms without exports as ineffective. This is no longer the case.

  • SPARK Pro
    Dec 12th, 2014

    Improved handling of floating point conversions
    The SPARK toolset has now improved handling of conversions between single and double precision floating point types. The result is more proved checks in the presence of such conversions.

  • SPARK Pro
    Dec 11th, 2014

    Shared manual proof files
    User's can now provide theorem libraries to GNATprove in order to access contained theorems during manual proof. To do so, the user needs to provide the sources of the library in the Proof_Dir and GNATprove will be in charge to compile it.

  • SPARK Pro
    Dec 11th, 2014

    Accept “alt-ergo” as prover name
    A common typo is to type "alt-ergo" instead of "altergo" when specifying the prover "Alt-Ergo" using the option --prover. The tool now accepts both variants.

  • GPRbuild
    Dec 10th, 2014

    GPRinstall Mode & Install_Name attributes
    It is now possible to set the Mode and Install_Name value in the package Install of a project. These attributes are equivalent to the GPSinstall command line options but allow per project fine tuning of the installation setup.

  • GNAT Pro
    Dec 9th, 2014

    Setting custom linker script for LEON run times
    User-defined linker scripts for bare board LEON targets can be set by simply defining the environment variable LDSCRIPT to point to the file to use.

  • GNAT Pro
    Dec 9th, 2014

    Implement new restriction No_Use_Of_Entity
    A new restriction No_Use_Of_Entity is implemented. The form of this is pragma Restriction[_Warning]s (No_Use_Of_Entity => NAME), where NAME is a fully qualified entity name. The effect is to forbid references to this entity in the main unit, its spec, and any subunits. For example, the use of pragma Restrictions (No_Use_Of_Entity => Ada.Text_IO.Put_Line) would forbid references to Put_Line, but references to Put would still be allowed.

  • GNAT Pro
    Dec 9th, 2014

    Trap table for LEON not modified at execution time
    The run-time libraries for bare board LEON processors install statically the minimum number of trap entries. Hence, the trap table can be easily kept in ROM.

  • GNAT Pro
    Dec 8th, 2014

    Inline_Always effective on instances without -gnatN
    On targets where inlining of calls must be done by the front end (such as JVM, .NET, AAMP), calls to subprograms marked with Inline_Always that are declared within a generic instantiation are now inlined by default (without use of -gnatN).

  • GNAT Pro
    Dec 5th, 2014

    Implement NaN semantics for floating-point ‘Min/Max
    In GNAT, Machine_Overflows is generally False for floating-point types, which means that operations such as 0.0/0.0 can generate NaN's. The Min and Max attributes have been enhanced to yield a predictable outcome in their presence: if either operand is a Nan, the other operand is returned; if both operands are NaN's, a NaN is returned.

  • SPARK Pro
    Dec 2nd, 2014

    New formal vectors both definite and indefinite
    The API of formal vectors has been simplified for efficiency, and a new standard unit Ada.Containers.Formal_Indefinite_Vectors is defined to hold elements of an indefinite type, for example a classwide type. Both units can be used in SPARK code, and GNATprove then generates checks that the API is used correctly.

  • SPARK Pro
    Dec 1st, 2014

    Consistent casing of flow messages
    The casing in flow messages now precisely matches the user's code.

  • GNAT Pro
    Dec 1st, 2014

    Do not warn that ineffective Inline is redundant
    Previously, if a pragma Inline was ineffective, and warn on redundant constructs was in effect (-gnatwr, included in -gnatwa), then a warning would be given that the Inline was redundant. This is not a helpful warning, and it is now suppressed.

  • GNAT Pro
    Dec 1st, 2014

    S’Img is static for a static enum type expression
    If the GNAT attribute 'Img is applied to a prefix which is of an enumeration type and is a static expression, then the result is static (and is the literal from the enumeration type). This works even if Discard_Names is in effect. This allows for example X'Img as the operand for External_Tag.