Development Log

  • 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.

  • GNAT Pro|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

    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.

  • 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.

  • GNAT Pro|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 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.

  • GNAT Pro
    Nov 27th, 2014

    Better error msg for USE of [generic] subprogram
    A USE clause is not allowed for a subprogram or generic subprogram. The compiler now gives a clearer error message for such an illegal attempt.

  • Ada Web Server
    Nov 26th, 2014

    Add support for schema root naming
    It is now possible to set the schema root name generated in the WSDL with ada2wsdl. This is needed when mixing multiple project to avoid name clashes. The same support has been added in the wsdl2aws tool to generate the sources under a specific prefix. Again this is to avoid name clashes when multiple Ada source codes are generated.

  • SPARK Pro
    Nov 24th, 2014

    Removed redundant warning of null globals assumed
    The tools used to issue a warning of "null globals assumed" both at the declaration of an imported subprogram and whenever that subprogram was called. The tools now only emit the later. These warnings can be suppressed via the use of a pragma Warnings. However, the proper solution would be to provide a global contract for the imported subprogram.

  • GNAT Pro
    Nov 23rd, 2014

    Warn when fixed-point end-points are out of range
    The compiler is allowed to adjust the declared end points of a fixed-point type by delta (RM 3.5.9(13)). This can result in a declared end-point of the range being outside the actual range of the type. GNAT takes advantage of this when it can result in the type just fitting in a convenient size (e.g. 32 bits instead of 33 bits). This situation now generates a warning.

  • GNAT Pro|GPRbuild
    Nov 21st, 2014

    GPRinstall new—no-build-var option
    A new option --no-build-var has been introduced and is meant to be use for project with a single configuration (single installation). In this case there is no build/scenario variable generated.

  • SPARK Pro
    Nov 20th, 2014

    Actual parameters with property Async_Writers
    Actual volatile parameters with enabled external property Async_Writers can now appear in procedure calls where the corresponding formal is of mode OUT.

  • GNAT Pro
    Nov 20th, 2014

    Do not trust Elaborate in SPARK
    In normal GNAT static elaboration mode, a pragma Elaborate is trusted to be sufficient, and the use of such a pragma disables the static checking. In SPARK mode, the pragma Elaborate is allowed, but it is not trusted to be sufficient, since this cannot be verified at compile time. This means that we may require Elaborate_All even if a pragma Elaborate is present.

  • GNAT Pro
    Nov 20th, 2014

    New directories in project path for gnatls—RTS=
    Two new directories are added in the project path, when gnatls is invoked with --RTS=, just before the two directories for the target. When the runtime is a single name, the directories are:

      <prefix>/<target>/<runtime>/lib/gnat
      <prefix>/<target>/<runtime>/share/gpr
    
    Otherwise, the runtime directory is either an absolute path or a path relative to the current working directory and the two added directories are:
      <runtime_directory>/lib/gnat
      <runtime_directory>/share/gpr
    

  • GNAT Pro
    Nov 19th, 2014

    Ignore Suppress (Elaboration_Check) in SPARK
    In normal GNAT mode, Suppress (Elaboration_Check) disconnects the normal static elaboration mode circuitry. We don't want that in SPARK, where the elaboration rules are important static legality rules that must not be compromised. So in SPARK mode, we ignore the attempt with a warning.

  • GNAT Pro
    Nov 18th, 2014

    Require Elaborate_All for SPARK mode variable ref
    In SPARK mode, a variable reference to a variable in another package requires an explicit Elaborate_All call, and this is now implemented. Note that the current SPARK manual specified this is only required for read/write references, so the rule implemented is more restrictive. It is not clear exactly what constitutes a read/write reference, which is why the more general, more easily stated, rule is implemented.

  • SPARK Pro
    Nov 17th, 2014

    Tune options for CVC4
    The options used for CVC4 have been tuned, so that more VCs are discharged automatically.

  • GNAT Pro
    Nov 16th, 2014

    Handle aspects before initialization expression
    Aspect specifications belong after the initialization expression in an object declaration, not before, but the compiler now accepts them before with a clear error message

  • GNAT Pro
    Nov 16th, 2014

    Require Elaborate_All for calls in SPARK mode
    In SPARK mode, we always operate in the static elaboration mode, but we do not generate implicit Elaborate_All pragmas; instead we require such pragmas to be explicitly present for calls in elaboration code. This requirement is now implemented

  • GNAT Pro
    Nov 14th, 2014

    gnatpp:—split-line-before-op
    The --split-line-before-op switch is added to gnatpp. If it is necessary to split a line at a binary operator, by default the line is split after the operator, as always. With this option, it is split before the operator.

  • CodePeer
    Nov 13th, 2014

    Faster analysis of logical expressions
    CodePeer has improved the time necessary to perform the analysis of complex expressions that combine a large number of logical operators.

  • GNAT Pro
    Nov 13th, 2014

    Better error message for No_Elaboration_Code_All
    The error message for a violation of pragma No_Elaboration_Code_All now clearly identifies the offending package (the one that lacks the required pragma or restriction) in the case where the system.ads file contains the pragma No_Elaboration_Code_All.

  • GNAT Pro
    Nov 13th, 2014

    Forbid pragma Elaborate in SPARK mode
    The SPARK RM forbids the use of pragma Elaborate in SPARK mode (instead it is required to write pragma Elaborate_All explicitly). This rule is now properly enforced.

  • SPARK Pro
    Nov 12th, 2014

    CVC4 shipped with SPARK, enabled by default
    The SPARK toolset has provided the option --prover to select other automatic provers, but it was shipped only with prover Alt-Ergo, and by default proof was attempted only with this prover. Now, SPARK also comes with the SMT prover CVC4, and the new default setting of option --prover is

      --prover=cvc4,altergo
    
    
    This increases greatly the proof capabilities of the tool, while only slightly increasing running time.

  • GNAT Pro
    Nov 12th, 2014

    Numeric_Literals gnatcheck rule is improved
    The gnatcheck Numeric_Literals rule no longer flags numeric literals in aspect specifications and aspect clauses (representation clauses).

  • GNAT Pro
    Nov 12th, 2014

    Better handling of discriminants in Unchecked_Union
    The compiler no longer generates a warning for a "missing" component clause for a discriminant in an Unchecked_Union (since the discriminant is not stored, it does not need one), and also avoids listing the representation of such a discriminant in the output from use of -gnatR2.

  • GNAT Pro
    Nov 11th, 2014

    CPU_Set implemented
    AI12-0033-1, "Sets of CPUs when defining dispatching domains" is now implemented. This allows Dispatching_Domains to be defined as arbitrary sets of processors, rather than just ranges. See System.Multiprocessors.Dispatching_Domains (s-mudido.ads).

  • GNAT Pro
    Nov 10th, 2014

    Inter-unit inlining of expression functions
    Expression functions declared in package specifications are now inlined across units with -O1 or -O2 and -gnatn (which is equivalent to -gnatn1). They were previously inlined across units only with -O3 -gnatn (which is equivalent to -gnatn2).

  • GNAT Pro
    Nov 9th, 2014

    No_Elaboration_Code_All allowed for generics
    The pragma No_Elaboration_Code_All may now be applied to generic units (generic package specs and generic subprogram specs).

  • SPARK Pro
    Nov 7th, 2014

    Possibility to attempt proof for all VCs
    Normally, the SPARK toolset stops attempting to prove a check as soon as one VC has not been proved. This is well-suited for automatic proof and provides timely tool results. However, to combine automatic and manual proof, it may be useful to attempt proof of all VCs of a check. This can be done now by selecting the proof mode together with the mode for VC attempts, for example the switch

      --proof=progressive:all
    
    
    selects progressive splitting of VCs, while attempting proof on all, and
      --proof=per_path:lazy
    
    
    selects one VC per check and path, stopping at the first unproved VC per check.

  • CodePeer
    Nov 7th, 2014

    Comparison to baseline in different location
    It is now possible to compare the results of an analysis to a baseline of the same project established in a different location, as long as they share the same database.

  • GNAT Pro
    Nov 7th, 2014

    GNAAMP: Optimize literal indexing of global arrays
    On the AAMP target, with -O1 the compiler emits shorter code sequences for indexing of library-level arrays by literals.

  • SPARK Pro
    Nov 6th, 2014

    Support for tagged types
    Tagged types, interfaces and dynamic dispatch are now supported in SPARK. The new aspect Extensions_Visible (documented in the SPARK RM) controls if any extensions of a controlling parameter need to be considered or are visible. This aspect also controls if it is possible to convert a parameter to a class-wide type. By default this aspect is False in SPARK_Mode. Class-wide globals and depends (which are currently assumed to be equal to the non-class-wide globals and depends) will be checked by flow analysis. Flow analysis also checks that LSP (Liskov Substitution Principle) holds for class-wide globals and depends. Class-wide preconditions and postconditions are supported and checked by proof where appropriate. Proof also checks that LSP (Liskov Substitution Principle) holds for class-wide preconditions and postconditions.

  • SPARK Pro
    Nov 5th, 2014

    Better support for Refined_Post
    The SPARK toolset now fully supports the Refined_Post aspect. Previously, even callers who had visibility of the refined postcondition could not make use of it and only used the regular postcondition instead. This has been improved now.

  • SPARK Pro
    Nov 5th, 2014

    Warning about uninitializable state abstractions
    Flow analysis now issues a warning whenever a state abstraction is impossible to initialize.

  • GNAT Pro
    Nov 5th, 2014

    Unordered enumerate warning suppressed for generic
    The warning about inappropriate usage for an unordered enumeration type is now suppressed for generic types in the template (since the instantiation may be with an ordered enumeration type where the usage is legitimate).

  • GNAT Pro
    Nov 4th, 2014

    Type extensions always inherit parent SSO
    A type extension must have the same scalar storage order as its parent (as per the definition of the Scalar_Storage_Order aspect). The compiler now ensures that the default scalar storage order for a tagged derived type is set to this required value even in the presence of a Default_Scalar_Storage_Order pragma specifying a different value, so that the user does not have to repeat the parent SSO.

  • GNAT Pro
    Nov 3rd, 2014

    Implement new syntax for FCMP/FCMPE on Visium/GR6
    The assembler now supports the new syntax of the FCMP/FCMPE instructions for the GR6 variant of the Visium architecture.

  • SPARK Pro
    Nov 3rd, 2014

    Do not stop analysis on empty range check
    As GNATprove implements stricter rules than those mandated by Ada RM, in particular by issuing errors on compile-time known constraint errors which should not prevent compilation, it stopped analysis on empty range checks, which appear legitimately on deactivated code. Such empty range checks do no stop analysis anymore, instead a check is generated by GNATprove during proof.

  • GNAT Pro
    Nov 2nd, 2014

    Duplicate pragma Linker_Section is detected
    If a duplicate pragma Linker_Section is encountered for a single entity, an error message is now given.

   1  2  3     Next »