Development Log

  • GNAT Pro|GPRbuild
    Jul 6th, 2015

    New tool gprname
    A new GPR tool, gprname, is now available. It is the replacement of "gnatname -P".

  • SPARK Pro
    Jun 26th, 2015

    Constant can now appear in contracts
    The SPARK toolset now allows for constants with variable input to appear in flow-related contracts. This allows for more precise information flow analysis.

  • GNAT Pro
    Jun 26th, 2015

    Verification of ignored Ghost code removal
    The removal of Ghost entities declared with Ghost policy Ignore along with associated code can now be verified by first compiling the code base, then searching for prefix "_ghost_" in object files. The lack of this prefix indicates that all ignored Ghost code has been sucessfully removed.

  • SPARK Pro
    Jun 25th, 2015

    Support for volatile functions
    The SPARK toolset now correctly implements the semantics of the Boolean aspect volatile_function in both flow analysis and proof.

  • SPARK Pro
    Jun 24th, 2015

    Detect violations of language restrictions
    The SPARK toolset now checks settings of the pragma Restrictions before analyzing the code; previously they were only checked by the compiler.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Jun 23rd, 2015

    GPS: Navigation from race conditions report
    CodePeer's Race contitions report allows to navigate to location of access to shared object in source code.

  • GNAT Pro
    Jun 19th, 2015

    Array comparison on reconfigurable runtimes
    Comparison operations on arrays of discrete components are now allowed on ZFP and Ravenscar-SFP runtimes.

  • GNAT Pro
    Jun 18th, 2015

    New restriction - No_Task_At_Interrupt_Priority
    A new restriction No_Task_At_Interrupt_Priority has been implemented. It forbids pragma or aspect Interrupt_Priority on tasks. This restriction is enforced in Ravenscar for Cortex-M runtimes on the ARM-elf platform.

  • CodePeer
    Jun 17th, 2015

    Integration with Jenkins
    A Jenkins plug-in is now distributed with CodePeer. It provides a Build Step to configure a run of CodePeer as part of a Jenkins build.

  • GNAT Pro
    Jun 16th, 2015

    Debug info for limited class-wide objects
    The compiler now generates debug info for a limited class-wide object initialized by a function call.

  • GNAT Pro|GPRbuild
    Jun 15th, 2015

    Add variables in gprinstall’s generated projects
    Project generated with gprinstall will now contains global variables as found in the original project.

  • GNAT Pro
    Jun 12th, 2015

    UET_Address attribute removed
    The unused and internal use only attribute UET_Address has been removed.

  • SPARK Pro
    Jun 11th, 2015

    Do not generate spurious discriminant checks
    Discriminant checks were previously generated on all component accesses on discriminant records. These only correspond to an actual language check when the component is defined in a variant part. Thus, GNATprove has been improved to only generate these checks when mandated by the language.

  • SPARK Pro
    Jun 9th, 2015

    For loops on type with Iterable aspect
    The SPARK toolset now supports for loops on objects of types with the Iterable aspect specified. In particular, it is the case for loops on formal containers. Both iteration over cursors (for in) and over elements (for of) are supported.

  • SPARK Pro
    Jun 9th, 2015

    Support for iterators on arrays
    Iterators on arrays, both in loop statements and in quantified expressions, are now supported by GNATprove, except for the case of a quantified expression with an iterator over a multi-dimensional array.

  • SPARK Pro
    Jun 7th, 2015

    Better support for fixed-point division
    The SPARK toolset now supports division of fixed-point values when the result type is integer and both operands have the same base type.

  • GNAT Pro
    Jun 5th, 2015

    Image function for dimensioned quantities
    The package System.Dim.float_IO now includes a function Image, that provides a string representation of a dimensioned quantity, where the numeric value is followed by the declared symbol for the corresponding unit, or the expression that enumerates its dimensions.

  • SPARK Pro
    Jun 3rd, 2015

    Improve tracking of bounds on slice assignments
    The SPARK toolset now tracks better the values of dynamic array bounds when assigning into a slice of an array, especially when this array is itself contained in a composite variable.

  • GNAT Pro|GPRbuild
    Jun 1st, 2015

    Create a symlink for the versioned libraries
    A symlink is now created on the main library directory for a library name with a version (Library_Version attribute).

  • GNAT Pro
    Jun 1st, 2015

    Suppressing checks in containers
    Two new check names, Container_Checks and Tampering_Check, are added to allow suppression of checks in Ada.Containers packages. You can put:

      pragma Suppress (Container_Checks);
    
    
    before an instantiation of (say) Ada.Containers.Vectors, and all checking code is removed. More importantly, all the controlled-type machinery involved with tampering checks is also removed. You can Suppress (Tampering_Check) to suppress just the tampering checks and machinery (which are the most expensive, and least effective at catching bugs). Suppress(All_Checks) and the -gnatp switch also work.

  • GNAT Pro
    May 28th, 2015

    Single-line hexadecimal traceback
    Hexadecimal tracebacks are given as a single line of code addresses, which makes it easier to cut&paste into an addr2line command, for example.

  • SPARK Pro
    May 27th, 2015

    Complete translation of SPARKSkein to SPARK 2014
    The SPARKSkein cryptographic hashing program originally written in SPARK 2005 (http://www.skein-hash.info/SPARKSkein-release) has now been fully translated into SPARK 2014. GNATprove proves absence of run-time errors on the new version in a few minutes. See section about it in section 6.9.3 "Multi-Units Demos" of the User's Guide for more information.

  • GNAT Pro
    May 27th, 2015

    Instrumented System.Memory can use GNAT.Debug_Pools
    Packages instrumenting System.Memory can use GNAT.Debug_Pools package to allocate memory. Dump and Reset capabilities are added to GNAT.Debug_Pools.

  • GNAT Pro
    May 27th, 2015

    New gnatcheck rule - Maximum_Parameters
    A new rule named Maximum_Parameters is added to gnatcheck. It flags variable declarations in library package and library generic package declarations.

  • GNAT Pro
    May 25th, 2015

    New gnatcheck rule - Maximum_Parameters
    A new rule named Maximum_Parameters is added to gnatcheck. It checks if a subprogram has more formal parameters than are specified by the rule parameter.

  • SPARK Pro
    May 22nd, 2015

    Suppress no effect warning when user already knows
    The SPARK toolset no longer emits a "subprogram Bla has no effect" warning when the user has added a Global/Depends aspect on Bla since this indicates that the effects of the subprogram are already known to her. The message is also suppressed when Bla is marked No_Return and is deemed to abnormally terminate.

  • SPARK Pro
    May 21st, 2015

    Lift restriction on calls to No_Return procedures
    This lifts the SPARK RM restriction forcing calls to procedures marked No_Return to appear either at the end of a subprogram or as the only statement inside an if-statement without else/elsif part. Indeed, this restriction is not needed anymore, similarly to what was done for raise-statements already.

  • GNAT Pro
    May 21st, 2015

    Change of runtimes on powerpc-elf bareboard
    The runtimes provided for powerpc-elf bareboard now runs on mpc8641 platforms instead of PReP. The former platform is still available, high performance while the latter has been deprecated for more than 10 years. The GNATemulator product has been updated too.

  • SPARK Pro
    May 20th, 2015

    Do not issue spurious warnings with—limit-subp
    When analyzing a single subprogram (typically with 'Prove Subprogram' or 'Prove Line' in an GPS or GNATbench), spurious warnings were issued on justification pragmas (pragma Annotate(GNATprove,...)) in other subprograms. This is no longer the case.

  • GNAT Pro
    May 19th, 2015

    Static object allocation with complex static size
    The compiler can now statically allocate objects declared at the library level and whose static size depends on a constant whose value is taken from a static array aggregate indexed by a character or enumeration type, as was already supported for an integer index type.

  • CodePeer
    May 18th, 2015

    Improved performance computing possible value sets
    A more efficient method for computing the union of a large number of sets is used. The observed performance difference is substantial in some cases involving large array aggregates with floating point element values.

  • GNATCOLL.Refcount: new package Shared_Pointers
    A new implementation for reference counted types is provided. It provides a more flexible API than the Smart_Pointers (since the Element_Type does not need to be a tagged type derived from Refcounted), and is faster, thanks to the use of storage pools. The API is safer since Get now returns a reference type rather than a direct access to the element. This new package is used throughout GNATCOLL, in particular GNATCOLL.SQL. In general, this has no effect on existing code.

  • SPARK Pro
    May 15th, 2015

    Allow manual proof of parts of Checks
    Previously, it was not possible to run a manual prover on a VC that represents part of a check, i.e. that was obtained by option --proof=progressive. This is now possible.

  • SPARK Pro
    May 15th, 2015

    TCP/IP in SPARK distributed as example
    An implementation of TCP/IP in SPARK is distributed now in the 'examples' of the release. This implementation based on LWIP design is targeted at bare-board embedded applications in certifiable systems. Data dependency contracts are given for most subprograms. These contracts are proved by GNATprove flow analysis, which also proves the absence of reads of uninitialized data. See the description of this example in section 6.9 'Examples in the Toolset Distribution' in SPARK User's Guide, or the README in ipstack directory.

  • SPARK Pro
    May 15th, 2015

    More examples distributed with the release
    The examples distributed with the release now include 7 small examples (a few dozen slocs), 20 medium-size examples (a single unit of a few hundred slocs at most) and 7 larger examples (of a few hundreds or thousands slocs). These examples include for example the 'Autopilot' case study distributed with John Barnes's books on SPARK 2005 and the well-known 'Tokeneer' case study commissioned by the NSA, both translated to SPARK 2014. See section 6.9 of the SPARK User's Guide 'Examples in the Toolset Distribution' for details.

  • GNAT Pro
    May 13th, 2015

    Monotonic_Clock enhanced under Android
    The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday() under Android.

  • GNAT Pro
    May 13th, 2015

    Monotonic_Clock enhanced under GNU/Linux
    The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday() under GNU/Linux.

  • GNAT Pro
    May 13th, 2015

    Iteration over container with indefinite type
    An iterable aspect can be specified for a formal container whose components are indefinite types (except for unconstrained arrays). An element loop over such containers has the usual semantics.

  • SPARK Pro
    May 12th, 2015

    Use dedicated support for arrays in SMT solvers
    The SPARK toolset now uses dedicated support for arrays when available in the underlying solver. This should result in more proofs of array properties, in particular over arrays either indexed by or containing modular types.

  • GNAT Pro
    May 7th, 2015

    Optimization of predicate checks
    If the expression in a dynamic predicate aspect is free of side effects, the compiler will eliminate redundant calls to the corresponding function, when code is compiled with inlining and high optimization (-gnatn -O3).

  • QGen
    May 6th, 2015

    Project P Open Workshop

    Project P is a three-year research project funded within the French FUI 2011 funding framework. It sees the collaboration of major industrial partners (Airbus, Astrium, Continental, Rockwell Collins, Safran, Thales), SMEs (AdaCore, Altair, Scilab Enterprise, STI), service companies (ACG, Aboard Engineering, Atos Origins) and research centers (CNRS, ENPC, INRIA, ONERA).

    With the project now drawing to an end comes the final presentation of all the work that has been produced over the past 3 years...

    Continental France, Project P leader, and all the project partners are pleased to invite you to the presentation of the final results of Project P.

  • SPARK Pro
    May 6th, 2015

    Better reporting of incorrect prover configuration
    Previously, when there where problems running external provers, GNATprove would silently consider the runs as simply "not proved". This could happen with user-provided configuration of external provers, for example using the "--why3-conf" command-line switch. Now, the SPARK toolset reports such problems explicitly as warnings.

  • GPS: recent searches in view filters
    The filters that exist in some views now remember recent searches, so that you can repeat them more easily.

  • GPS: remove support for title bars for views
    We removed a few preferences in the "Windows" section related to the support for title bars in views. This simplifies the preference dialog.

  • GNAT Pro
    May 5th, 2015

    Implement workaround for AT697F trap errata
    The LEON run-time libraries have been enhanced to work around the issue present in the AT697F processor and documented in the errata sheet 41003B-AERO-07/14 that causes unexpected clearing of interrupts.

  • GPS: the speed bar is drawn on top of the scrollbar
    The speed bar has been removed, thus saving some horizontal space: the information of highlights in the editor is now drawn directly on top of the vertical scrollbar.

  • CodePeer
    May 2nd, 2015

    Tooltips for possible values of variables
    CodePeer generates information about possible values of variables and expressions during its analysis, which is now displayed in the GPS source editor as an information tooltip.

  • GNAT Pro
    May 2nd, 2015

    Improved message for bad last bit value
    The error message for violation of the RM 13.5.1(10) rules about the allowed value of last bit is improved (it is the last bit + 1 value, not last bit itself, that must meet the criteria).

  • CodePeer
    May 1st, 2015

    Generation of backtraces on messages
    CodePeer now generates by default detailed information about places in the source code involved in a particular check-related message, making it easier to analyze such messages and identify possible errors in the source. This extra information is displayed by GPS in a new view.

  • GNAT Pro
    May 1st, 2015

    Avoid use of secondary stack
    Use of the secondary stack, and the corresponding cleanup handlers, is avoided in many cases. For example, access discriminants no longer force functions to return on the secondary stack. This is a speed improvement. It is particularly relevant to the Ada.Containers.

  • SPARK Pro
    Apr 30th, 2015

    Improve tracking of values of constants
    The SPARK toolset now tracks better the values of constants defined outside of the analyzed unit. This should result in better proofs, in particular for constants with a nonstatic value or aggregates containing real literals.

  • SPARK Pro
    Apr 30th, 2015

    Improved messages about illegal usage of input
    Formal and global parameters of mode out that are fully default initialized but incorrectly have their input value used have a more accurate message.

  • SPARK Pro
    Apr 29th, 2015

    Better messages for initialization of constituents
    Flow-related messages about constituents now explicitly refer to names of the refined abstract state variables.

  • GNAT Pro
    Apr 29th, 2015

    Speed improvements for controlled types
    The implementation of controlled types is optimized so that in simple cases, they are just as efficient as noncontrolled types where initialization and cleanup is done by hand. For short Initialize/Finalize routines, this can double the speed of object creation and destruction.

  • CodePeer
    Apr 28th, 2015

    New switch -no-presumptions
    CodePeer supports a new switch -no-presumptions to suppress generation of presumptions on unanalyzed subprogram calls. Use of this switch will generally result in additional messages being reported in the vicinity of unanalyzed calls, since assumptions about the result of such calls are no longer made. This option is implied by -level 4.

  • GNAT Pro
    Apr 27th, 2015

    Pragma Abort_Defer respects Restrictions
    Pragma Abort_Defer does nothing in the presence of Restrictions that prevent abort, thus avoiding the overhead of abort deferral. The idea is that you might write some reusable code that is used in programs with abort, and needs Pragma Abort_Defer, but is also used in programs without abort. For the latter, use these restrictions:

      pragma Restrictions (No_Abort_Statements);
      pragma Restrictions (Max_Asynchronous_Select_Nesting => 0);
    
    
    and there will be no overhead for abort deferral.

  • GNAT Pro
    Apr 26th, 2015

    Elaboration Warning for Finalize can be suppressed
    The warning that Finalize (or Initialize or Adjust) might cause a possible elaboration problem can now be suppressed by using Warnings (Off, T) where T is the controlled type involved.

  • SPARK Pro
    Apr 24th, 2015

    Better support for expression functions
    The SPARK toolset now deals better with non-recursive expression functions returning real types.

  • GNAT Pro
    Apr 24th, 2015

    Static elab—internal calls to instances
    The static elaboration model is necessarily conservative, leading to elaboration cycles in cases that would in fact not fail at run time. However, in certain obscure cases of a call to a subprogram in an instance of a generic package that is within this same unit as the call, the compiler is now less conservative, avoiding elaboration cycles in those cases.

  • GNAT Pro|GPRbuild
    Apr 21st, 2015

    —create-map-file for cross targets
    This is now supported on cross platforms that use GNU ld to link.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Apr 20th, 2015

    GPS: Ability to provide fonts under UNIX
    GPS comes with a mechanism for adding custom fonts. (This does not work on Windows, where the fonts need to be installed at the system level). GPS 6.2 also comes with better default fonts out-of-the-box.

  • GNAT Pro
    Apr 20th, 2015

    Improve consistency of floating-point **
    This enhancement ensures on all targets that A**B = A**C when B is a small static constant in the range 0 .. 4 and C is a variable with the same value. Previously for Float and Long_Float on some targets, this was not the case. The results given were both within the error bounds that are allowed by the Ada standard, but it is desirable not to have this discrepancy. This also aids formal verification of such operations.

  • GNAT Pro
    Apr 18th, 2015

    New restrictions pragmas recognized in System
    Only certain restriction pragmas are recognized in package System, and now No_Specification_Of_Aspect, No_Use_Of_Attribute, and No_Use_Of_Pragma have been added to the recognized list, allowing more flexibility in configuring new versions of the System package.

  • SPARK Pro
    Apr 14th, 2015

    support for ‘Address Attribute
    The SPARK toolset now supports the 'Address attribute for objects.

  • GNAT Pro|GPRbuild
    Apr 12th, 2015

    GPRbuild distributed environment variables
    gprbuild and gprslave now accepts slaves to be specified using environment variables. Either GPR_SLAVES which contains a coma separated list of host names or GPR_SLAVES_FILE with specify a file whose content must be an host name per line.

  • GNAT Pro
    Apr 11th, 2015

    New aspect Disable_Controlled
    A new aspect Disable_Controlled is defined for controlled record types. If active, this aspect causes suppression of all related calls to Initialize, Adjust, and Finalize. The intended use is for conditional compilation, where for example you might want a record to be controlled or not depending on whether some run-time check is enabled or suppressed.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Apr 10th, 2015

    GPS: Python to configure views
    The settings from the local configuration menus of the views can now be toggled via python commands, using the GPS.Preference API.

  • SPARK Pro
    Apr 9th, 2015

    Improve support for Size attributes
    The SPARK toolset now fully supports the Size attribute, which was supported only for prefixes that are constrained types.

  • GNAT Pro
    Apr 7th, 2015

    Improve speed of Append for Vectors
    The speed of Ada.Containers.Vectors.Append has been improved. Simple benchmarks show that in common cases, Append is over 3 times faster than it was.

  • GNAT Pro
    Apr 6th, 2015

    Improve speed of “for ... of” loops for containers
    The speed of "for ... of" loops over predefined containers has been improved substantially. Simple benchmarks show that the overhead of such loops has been cut by a significant factor, up to 30.

  • GNAT Pro
    Apr 6th, 2015

    Improved warning for misused trailing array idiom
    Some packages implementing interfaces to C/C++ libraries, for example Win32, use the trailing array idiom, whereby a trailing array in a record type is intended to be safely overrun to access a larger buffer. The compiler now warns in more cases where this idiom is used in an incorrect manner on the client side in conjunction with aggressive loop optimization (-O2 or above).

  • GNAT Pro
    Apr 3rd, 2015

    Avoid surprising failure of fpt postcondition
    When operating on a machine with extended precision intermediate results, such as the x86 with traditional floating-point, then a postcondition of the form X'Result = Expr may unexpectedly fail due to extra precision in the calculation of Expr. An implicit 'Machine operation is now introduced in this specific case to avoid this surprise.

  • GNAT Pro
    Apr 2nd, 2015

    The visium-elf port produces GR6 code by default
    The visium-elf toolchain now produces code for the latest variant (GR6) of the architecture by default and the associated RTS libraries are compiled in this mode as well.

  • SPARK Pro
    Apr 2nd, 2015

    Improve handling of discrete types
    The SPARK toolset now handles discrete types in a way closer to the underlying model for arithmetic operations. This results in more discharged verification conditions.

  • GNAT Pro
    Apr 1st, 2015

    gnatmake -P invokes gprbuild when available
    When gnatmake [gnatclean] is invokes with -P, if gprbuild [gprclean] is available, then gnatmake [gnatclean] invokes gprbuild [gprclean] with the same arguments.

  • Ada Web Server
    Apr 1st, 2015

    Add support pattern in WebSocket registry
    It is now possible to use regular expression to register WebSocket constructors.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 31st, 2015

    GPS: library directories displayed in Project view
    For library project, the library directory is displayed as an explicit node in the Project view, in addition to the object directory.

  • GNAT Pro
    Mar 31st, 2015

    New pragma/aspect Volatile_Full_Access
    A new pragma (and equivalent aspect) Volatile_Full_Access is implemented. This is similar to Volatile except that there is a guarantee that every read and write to an object with this aspect will use only instructions which read or write all the bits of the object. This includes the case of accessing a component of the object. Note that this differs from Atomic in that there is no such guarantee for Atomic (the compiler can read part of the object). It is not allowed to use Atomic and Volatile_Full_Access for the same entity.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 30th, 2015

    GPS: GPS.Action.disable is a new python function
    Using this function, it is now possible to disable all usage of an action within GPS, and gray out/hide all corresponding menus.

  • GNAT Pro|GPRbuild
    Mar 29th, 2015

    Out of tree build
    gprbuild can now build a project file out of a the source tree. That is, all artifacts (object, executable, ALI files) are relocated to the directory where gprbuild is launched when using the new --relocate-build-tree option. The --relocate-build-tree option is also available with gprinstall and gprclean to install artifacts or delete them from the out-of-tree build directory.

  • GNAT Pro
    Mar 27th, 2015

    Improved optimization of 2**K
    The compiler now optimizes 2**K into a quick shift instruction in more cases including handling binary modular types and signed integer types for the case where overflow checking is enabled. The latter is significant given the new default in the compiler which has overflow checking on by default. The new circuit avoids taking a significant penalty for 2**K with overflow enabled.

  • GNAT Pro
    Mar 26th, 2015

    Optimized visium-elf zfp RTS
    The zfp RTS for visium-elf is now compiled with options more suitable for the library's intended use, tailored for improved generated code efficiency and ability to perform automatic removal of unused functions at link time.

  • SPARK Pro
    Mar 26th, 2015

    Bodies of non-Ghost packages with Ghost constructs
    Ghost constructs that require a completion in a package body now always require the completion regardless of whether the enclosing package is a Ghost construct or not.

  • SPARK Pro
    Mar 24th, 2015

    Use of constants in contracts
    Constants with variable input can now appear in the following annotations: Global, Depends, Initializes, Part_Of, Refined_Global, Refined_Depends and Refined_State.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 24th, 2015

    GPS: makefile.py reads include statements
    Makefile targets found in included makefiles are now listed in the /Build/Makefile menu.

  • SPARK Pro
    Mar 20th, 2015

    Improve support of modular as index of array
    GNATprove now handles modular types as index of array with bitvectors. With this change, all modular types are handled in a similar way. This results in limiting to a minimum conversions to, and from, bitvectors on why3 side (badly supported by SMT solvers).

  • Ada Web Server
    Mar 20th, 2015

    Add support for encrypted server key file
    It is now possible to use a encrypted key file with AWS. In this case, a pass-phrase is required in order to start HTTPS sessions. This pass-phrase can be handed over to the server using Set_Password_Callback in AWS.Net.SSL.Certificate.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 17th, 2015

    GPS: new Color Theme window
    The plugin colorschemes.py has been modified: the way to switch between color themes is no longer through an entry in the Preferences dialog, but through a dedicated window, accessed using the menu Edit -> Color Themes. GPS now supports importing TextMate theme definitions, and a number of themes now ship by default with GPS.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 17th, 2015

    GPS: initial dir for the “Change Directory” dialog
    Under Linux/UNIX/Mac OS, the "Change directory" dialog now opens on the current directory, matching the behavior already present on Windows.

  • SPARK Pro
    Mar 17th, 2015

    Contracts on generic subprograms and packages
    The SPARK toolset now supports contracts on generic subprograms, packages and their respective bodies.

  • GNAT Pro
    Mar 17th, 2015

    Alignment_Check suppressed for non-strict alignment
    Alignment_Check is now suppressed by default for machines with non-strict alignment (such as the x86) since these machines handle unaligned references without any problem. Associated compile-time warnings are also suppressed if the run-time check is suppressed. The previous mode of operation (with this check enabled by default) can be obtained by placing in a configuration pragma file "pragma Unsuppress (Alignment_Check)".

  • GNAT Pro
    Mar 16th, 2015

    Add low bit rates to GNAT.Serial_Communications
    New literals B75, B110, B150, B300, and B600 have been added to type GNAT.Serial_Communications.Data_Rate to denote these low bit rates, in order to allow communication with legacy devices that require them.

  • GNAT Pro
    Mar 15th, 2015

    Exclude extended precision for ignored assertion
    If an assertion is compiled using the Ignore policy, and the overflow mode is Eliminate, then the extended precision arithmetic run-time unit (s-bignum) was being included in the build even though no code was being generated. This is now avoided, which is particularly important when using a configurable run-time that does not include this unit.

  • Ada Web Server
    Mar 14th, 2015

    Add support for document style SOAP/WSDL
    AWS now supports document style SOAP messages and WSDL documents.

  • PolyORB
    Mar 13th, 2015

    gnatdist now uses gprbuild by default
    The gnatdist partitioning tool will now use gprbuild by default to build partitions, if that tool is available. You can force the use of gnatmake using debugging switch -dM.

  • SPARK Pro
    Mar 13th, 2015

    Improve handling of dynamic types with dispatch
    The SPARK toolset now tracks bounds of dynamic scalar and array types better in particular in presence of dispatching calls and for verification of LSP conformance.

  • GNAT Pro|GPRbuild
    Mar 13th, 2015

    Dependency with different timestamp
    gprbuild now recompiles a file based source if one of its dependency source has a different time stamp, even when the time stamp is before the one of the object file.

  • Ada Web Server
    Mar 8th, 2015

    Add support for minOccurs/maxOccurs
    Add support for multi-occurrence SOAP elements. SOAP element declared with a minOccurs or maxOccurs different than 1 are now properly handled as multi-occurrence elements. If minOccurs is set to 0 the element can be omitted.

  • GNAT Pro
    Mar 5th, 2015

    Null procedures allowed in protected bodies
    AI12-0147 specifies that null procedures and expression functions are now allowed in protected bodies.

  • SPARK Pro
    Mar 5th, 2015

    Improve support of rotation of modular types
    The SPARK toolset now deals better with rotation of modular types of non constant amount.

   1  2  3     Next »