Development Log

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

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

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

  • CodePeer
    Oct 29th, 2014

    Suppressing analysis via Annotate pragmas
    By adding "pragma Annotate (CodePeer, Skip_Analysis);" at the start of the declaration list of a subprogram body or a package body, CodePeer's analysis of selected subprogram bodies can be suppressed. This is typically done in order to improve performance. For details, see CodePeer User's Guide section 2.4 ("Running CodePeer Faster").

  • GNAT Pro
    Oct 29th, 2014

    Windows GNAT.OS_Lib.Wait_Process improvement
    On Windows the Wait_Process routine now follows the UNIX semantics more closely. The main improvement are:

     - It is possible to have multiple tasks waiting for a child process
       to terminate.
     - When a child terminates, a single wait call will receive the
       corresponding process id.
     - A call to wait will handle new incoming child processes.
    

  • SPARK Pro
    Oct 24th, 2014

    Better error locations for flow analysis
    Flow analysis used to point at the export (Something) when it issued messages like

      warning: incorrect dependency "Something => State"
    
    We now point at the incorrect dependency (State) instead.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Oct 23rd, 2014

    GPS:—version and—help no longer require GUI
    The switches are parsed before GPS attempts to connect to the GUI environment. As a result, it is possible to get the help or the version even when the environment is not setup for GUI.

  • GNAT Pro
    Oct 23rd, 2014

    Support for overriding keyword in Ada 95 mode
    For compatibility with some Ada 95 compilers which support only the overriding keyword of Ada 2005, the -gnatd.D debug switch can now be used along with -gnat95 to achieve a similar effect with GNAT.

  • GNAT Pro
    Oct 22nd, 2014

    Win32Ada has some WinCrypt support
    Some Windows WinCrypt routines has been added into the Win32Ada binding. They can be found into the Win32-WinCrypt unit.

  • SPARK Pro
    Oct 21st, 2014

    Mark Ghost functions in formal containers
    Functions First_To_Previous, Current_To_Last and Strict_Equal introduced in units of the formal container library should only be used in contracts and assertions, as they are very inefficient. They are now marked as Ghost functions, which prevents use outside assertions and ghost code.

  • GNAT Pro
    Oct 21st, 2014

    Use of floating-point in fixed-point operations
    In the presence of restriction No_Floating_Point, a multiplication of two fixed point quantities of the same fixed point type in an integer context does not generate conversions to floating-point for run-time evaluation.

  • SPARK Pro
    Oct 20th, 2014

    Raise, no-return and statically-false assertions
    Flow analysis now ignores all statements that inevitably lead to a raise statement, a statically-false assertion or a non-returning procedure. Additionally, all statements that follow a raise statement, a statically-false assertion or a non-returning procedure that are not otherwise reachable from the start of the subprogram are also ignored.

  • SPARK Pro
    Oct 20th, 2014

    New implementation of Ghost entities
    The SPARK toolset now implements the new semantic and legality rules of Ghost entities. This feature now encompases states, objects, subprograms, packages and types. As a result, convention Ghost has been replaced with aspect Ghost.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Oct 17th, 2014

    Support for Runtime & Target attributes in projects
    These two new attributes are now supported by GPS and should replace the use of the IDE'Gnatlist attribute to specify the same information.

  • GNAT Pro|GPRbuild
    Oct 15th, 2014

    GPRslave control of simultaneous responses
    A new option has been added to GPRslave to control the number of simultaneous responses (sending back object code and ALI files) supported. This was hard coded to 2, it is now possible to set this value between 1 and the maximum number of simultaneous compilations.

  • SPARK Pro
    Oct 14th, 2014

    Replay facility always reissue warnings
    When a unit or the units on which it depends have not changed, GNATprove detects it and avoids re-analyzing the unit. This caused some warnings to be issued only the first time a unit was analyzed. Now, a new replay facility is used in GNATprove to always reissue warning and check messages when a unit is considered, even when it does not require re-analysis.

  • PolyORB
    Oct 13th, 2014

    Extend fast-path CDR marshalling to nested arrays
    The fast-path CDR marsahlling circuitry, allowing efficient marshalling of common aggregates such as arrays of bytes or integers, has been extended to the case of nested arrays.

  • GNAT Pro|GPRbuild
    Oct 13th, 2014

    Runtime specific directories in the project path
    For each non default runtime, there are now two more directories in the project path: <runtime_root>/lib/gnat and <runtime_root>/share/gpr, where <runtime_root> is either:

      - <runtime> ifthe runtime is explicitly specified as an absolute path
      - <compiler_root>/<target>/<runtime> if the runtime is not explicitly
        specified as an absolute path
    

  • GNAT Pro|GPRbuild
    Oct 13th, 2014

    Project path depends on compilers
    For tools gprbuild, gprclean and gprinstall, the project path depends on the compilers, not the prefix of the tool. For each compiler driver in a "bin" subdirectory, the compiler root is the parent directory of this "bin" subdirectory and the directories in the project path are, in order:

       <compiler_root>/<target>/lib/gnat
       <compiler_root>/<target>/share/gpr
       <compiler_root>/share/gpr
       <compiler_root>/lib/gnat
    

  • GNAT Pro|GPRbuild
    Oct 13th, 2014

    New gprbuild option—complete-output
    A new option --complete-output is added to gprbuild, allowed only on the command line and incompatible with option --distributed=. When this option is used, the standard output and standard error of the compiler are redirected to text files. When these files exist for a source that is up to date, their content is output to stdout and stderr.

   1  2  3     Next »