Development Log

  • SPARK Pro
    Jan 19th, 2015

    New form of pragma Warnings for specific tool
    Users of GNATprove can now specify pragma Warnings for GNAT and GNATprove separately, to selectively disable warnings from the compiler or the formal verification tool, using the syntax

      pragma Warnings (GNATprove, ...);
    
    for GNATprove-specific warnings, and
      pragma Warnings (GNAT, ...);
    
    for GNAT-specific warnings. This also allows detecting useless pragma Warnings with switch -gnatw.w, which was not possible previously as using this switch caused the tools to issue spurious warnings on the those pragma Warnings meant for the other tool.

  • Ada Web Server
    Jan 18th, 2015

    Add support for external schema
    It is now possible to use WSDL with references to external schema. In this case, wsdl2aws tool, will check the schema locally and load it if found.

  • Ada Web Server
    Jan 18th, 2015

    Add support for derived types
    AWS's wsdl2aws tool has now full support for derived types. The namespace for the parent type is properly used when generating the corresponding Ada code. This has make it possible to clean-up some old code to handle Ada Character mapping for example. Any type derivation level is properly handled.

  • GNAT Pro
    Jan 18th, 2015

    Better error recovery for WHEN in place of WITH
    The compiler now handles the case of WHEN used accicentally instead of WITH to introduce aspect specifications, and gives a clear error message.

  • GNAT Pro
    Jan 17th, 2015

    New documentation on floating-point
    A new section on "Floating-Point Operations" is added to the users guide. This section documents the infinity/NaN behavior of most GNAT ports, and also describes the -msse2 and -mfpmath=sse2 switches to force use of SSE2 arithmetic operations when the target is an x86.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Jan 14th, 2015

    GB: Debugger field added to toolchain editor
    Debugger command can be displayed and changed in the toolchain editor.

  • SPARK Pro
    Jan 13th, 2015

    Issue proof checks on calls to Assertions.Assert
    GNATprove now generates a check that Assertions.Assert procedures are always called with a Check argument of "True". This check shows as a precondition check when calling Assertions.Assert (a precondition added in the declarations of Assertions.Assert in a-assert.ads). The dynamic semantics of Assertions.Assert have not been modified, by setting the Assertion_Policy to Ignore for Pre in this unit (also in the same file).

  • SPARK Pro
    Jan 13th, 2015

    No implicit False pre on main loop subprogram
    During proof, GNATprove was treating all subprograms with No_Return aspect or pragma specified as error signaling subprograms, with an implicit precondition of "False". Now, subprograms with an output (parameter or global) are treated as main loop subprograms, hence without an implicit precondition of "False". This is similar to the distinction made in flow analysis.

  • Ada | Ada 2012
    Jan 12th, 2015

    Public Ada Training 2015

    This course, combining live lectures with hands-on lab sessions using the latest AdaCore tools and the STM32F4 Discovery Board, introduces software developers to the principal features of the Ada language with a special focus on embedded systems. Attendees will learn how to take advantage of Ada's software engineering support, including the contract-based programming features in Ada 2012, to produce reliable and readable code. No previous Ada experience is required.
     

  • SPARK Pro
    Jan 12th, 2015

    Support pragmas Precondition/Postcondition in body
    Pragmas Precondition and Postcondition (both GNAT-specific pragmas) inside subprogram bodies where currently ignored by GNATprove. They are now treated like assertions, occurring respectively on entry and on exit to the subprogram, so GNATprove generates checks to prove that they hold.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Jan 12th, 2015

    GPS: organize /Build menu by project
    When your project (or the imported projects) has a large number of mains, the /Build/Project and /Build/Run menu could become very large and require scrolling. Instead, an extra level of menu has been added, for each project that has a main.

  • GNAT Pro
    Jan 12th, 2015

    New tag missing-check in known problems file
    A new tag "missing-check" is added to the known-problems-73 file. This is similar to "wrong-code", but is used specifically for the case where the compiler is omitting a required run-time check.

  • GNAT Pro
    Jan 10th, 2015

    Warn on use of pragma Import in Pure unit
    The use of pragma Import in a Pure unit is worrisome since it can be used to "smuggle" non-pure behavior into a pure unit. This usage now generates a warning that calls to a subprogram imported in this manner may in some cases be omitted by the compiler, as allowed for Pure units. This warning is suppressed if an explicit Pure_Function aspect is given.

  • GNAT Pro
    Jan 8th, 2015

    Improve always True/False warning
    The warning that a condition is always False is improved to give a special clearer message when the subexpression is a simple object.

  • GPS: use unix-style paths when editing project
    When project properties are edited, all possible occurrences of backslashes are replaced with slashes. This makes it possible to use such project both under Windows and Linux.

  • SPARK Pro
    Jan 6th, 2015

    Support for multi-unit source files
    The SPARK toolset now supports the analysis of multi-unit source files, that is, files which define several library-level packages.

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

  • 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

    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.

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

  • GNAT Pro
    Nov 24th, 2014

    Proper message on predicate with infinite recursion
    A dynamic predicate for a type that includes a call to a primitive operation of the type will lead to infinite recursion. The compiler now emits a proper error message in this case, rather than a complaint about premature use of the type in the predicate expression.

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

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

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

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

  • GNAT Pro
    Oct 13th, 2014

    New function Non_Blocking_Spawn
    A new function Non_Blocking_Spawn is added to GNAT.OS_Lib. This function redirects standard error and standard output to two different files.

  • GNAT Pro
    Oct 10th, 2014

    Inlining of renamed subprograms
    The compiler supports inlining of renamed subprograms.

  • GNAT Pro
    Oct 10th, 2014

    Inlining of unchecked conversion instantiations
    Compiling with back-end inlining enabled the compiler supports implicit inlining of unchecked conversions defined in inlined subprograms (i.e. it is not necessary to add pragma Inline to instantiations of unchecked conversion defined in inlined subprograms).

  • GB: better scenario variables support
    Scenario variables editor added capability to:

     * set the variable for all projects
     * unset the variable for all projects to use GNAT project default value
    
    Scenario variables changes are taken into account immediately without having to restart GNATbench.

  • GB: add Ada/Environment preferences page
    New Ada/Environment preferences page allows the configuration of the environment used when GNATbench launch any command.

  • GNAT Pro
    Oct 7th, 2014

    Support for POSIX binding shared library
    Florist, the GNAT implementation of the standard Ada binding to the POSIX API, can now be built as a shared library by passing "--enable-shared" to its configure script.

  • SPARK Pro
    Oct 3rd, 2014

    Output of assumptions of verification results
    The SPARK toolset now supports the option --assumptions. With this option, the tool outputs for each verication result in the result file gnatprove.out, the assumptions it depends on. Assumptions are properties which should hold for the verification results to be true, but which the SPARK toolset could not verify by itself. This can happen because the corresponding code is not in the SPARK subset or the verification of that code was not finished. Currently, output assumptions only include the assumptions on called subprograms of analysed subprograms, but not assumptions about the calling context of analysed subprograms.

  • SPARK Pro
    Oct 3rd, 2014

    Support for list of provers to try
    The option --prover of the SPARK toolset has now been improved to allow a list of provers, e.g. the command line option --prover=altergo,cvc4 will first try to prove a VC with altergo, and if that fails, try again with CVC4. The same steps or timeout option applies to all provers.

  • GB: add support for “On File Change” builder target
    A builder target having its launch mode set to "On File Change" will be automatically launched each time an ada file is saved. Wind River Workbench users can use this feature to have ada code analyzed as soon as it is saved. Builder target settings are accessible through Ada / Builder Targets preferences page.

  • SPARK Pro
    Sep 30th, 2014

    Tools now warn on hidden unexposed state
    The SPARK toolset now issues a warning per hidden state of a package that is not exposed through a state abstraction while an enclosing package declares abstract state.

  • CodePeer
    Sep 29th, 2014

    New switches -show-reviews and -show-reviews-only
    A new switch -show-reviews (relevant with using -output-msg) shows the messages which have been reviewed, with their review information. -show-reviews-only is introduced and replaces the previous -show-manual-reviews switch.

  • GNAT Pro
    Sep 29th, 2014

    Improved elimination of useless range checks at -O2
    The compiler now eliminates more range checks that can never fail when the optimization level -O2 or above is specified.

   1  2  3     Next »