Development Log

  • SPARK Pro
    Jul 25th, 2014

    Reject derived types with new discriminants
    SPARK does not allow defining discriminants on a type deriving from a discriminated type (SPARK RM 3.7(2)). Discriminants should be inherited in that case. This is now correctly detected and rejected.

  • GNAT Pro
    Jul 25th, 2014

    Support for hash based message authentication codes
    The packages providing standard hash functions (MD5, SHA1, SHA224, SHA256, SHA384, and SHA512) now also support the computation of the corresponding HMACs. This is achieved by initializing the context with HMAC_Initial_Context instead of the default Initial_Context.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jul 24th, 2014

    GPS: animations in browsers
    GPS now uses animations in the browsers (call graph, project,...) when items are moved from one position to another. This helps preserve the context.

  • SPARK Pro
    Jul 23rd, 2014

    Better proof for preservation of discriminants
    The SPARK toolset now tracks non-mutable discriminants of record variables better, especially when the variables are modified in a loop or updated by a procedure call. This results in more proved verification conditions.

  • SPARK Pro
    Jul 23rd, 2014

    Use of SPARK_Mode in generics
    Aspect/pragma SPARK_Mode can now appear in generic units.

  • GNAT Pro
    Jul 23rd, 2014

    Improve warnings in -gnatVa mode
    The use of -gnatVa could cause disappearance of warnings about unmodified variables that could be constants. The warning circuitry has been enhanced so that these warnings are issued in -gnatVa mode.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jul 21st, 2014

    GPS: add filter in Project browser
    The project browser now has a local filter, instead of having a specialized search context in the standard search dialog.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jul 21st, 2014

    GPS: review call graph browser
    The call graph browser was redesigned. The rendering has changed. We no longer display the list of locations for the references (which is more usable in the Call Trees), so as to be able to display more items in the browser. Standard contextual menus related to entities are now usable in the browser.

  • GNAT Pro
    Jul 18th, 2014

    New warning on ineffective box initialization
    The compiler now warns on an aggregate component association in an object declaration, when the object is a constant and the component type does not have default value or default initialization.

  • SPARK Pro
    Jul 18th, 2014

    Better generation of globals
    The auto-generated globals are now more precise. Outputs are no longer always also considered to be inputs. Additionally, when available, state abstractions are utilized to return globals relatively to the scope of the caller (this allows for more precise warnings/errors).

  • SPARK Pro
    Jul 17th, 2014

    better support for some bitwise operations
    The SPARK toolset now provides better proof support for right-shifts by a constant shift and for bitwise "and" with a constant. This results in more proved VCs which involve such constructs.

  • CodePeer
    Jul 17th, 2014

    Support for integer/address comparisons
    CodePeer now accepts expressions involving comparisons between System.Address and Integer values (e.g. "=", "/=", ">").

  • SPARK Pro
    Jul 16th, 2014

    Better support of division for modular types
    Integer division on modular integer types is now better supported by the SPARK toolset, which results in more proved checks when integer division is involved.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jul 15th, 2014

    GPS: move to previous and next entry in call tree
    Two new buttons (and the correspondings actions to which we can associate key bindings) were added to the call trees' local toolbar, to move to the next and previous location.

  • GNAT Pro
    Jul 15th, 2014

    GNATstack supports project files
    The -P option can be passed to GNATstack to automatically retrieve the GNATstack switches and stack usage information from the application.

  • GNAT Pro
    Jul 15th, 2014

    GNATstack supports—RTS switch
    The --RTS option can be passed to GNATstack to automatically retrieve the stack usage information from the run-time library.

  • SPARK Pro
    Jul 11th, 2014

    Better parallelism for proof with “Prove Line”
    Previously, when doing proof for a single line or check, the SPARK 2014 toolset was using only a single core. Now, it takes into account the -j command line option and may use the specified number of cores.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jul 11th, 2014

    GPS: new parameter on_exit to BuildTarget.execute
    The command GPS.BuildTarget.execute now accepts an extra parameter on_exit: a function which is called when the build target terminates.

  • GNAT Pro
    Jul 10th, 2014

    Untyped variables in case constructions
    It is now allowed to use single string variables that are not typed string in a case construction. When not in quiet mode, a warning is issued if there is no "when others" variant.

  • GNAT Pro
    Jul 10th, 2014

    New attribute ‘Default_Scalar_Storage_Order
    A new implementation-defined attribute has been implemented. A reference to Standard'Default_Scalar_Storage_Order (Standard is the only allowed prefix) provides the current value of the default scalar storage order (as specified using pragma Default_Scalar_Storage_Order, or equal to Default_Bit_Order if unspecified) as a static Bit_Order value.

  • GNAT Pro
    Jul 8th, 2014

    New defaults for some projects attributes
    Some project attributes have now defaults that are not empty strings or string lists. 'Object_Dir default is ".", 'Exec_Dir default is 'Object_Dir and 'Source_Dirs default is (".").

  • GNAT Pro
    Jul 8th, 2014

    Ignore Check_Float_Overflow if Machine_Overflows
    The Check_Float_Overflow pragma, and the -gnateF switch, are ignored on targets which do hardware overflow checking in any case. This allows the use of the pragma on such machines without generating inefficient checking code, making it more convenient for testing such code on a machine which normally generates infinities.

  • GNAT Pro
    Jul 7th, 2014

    Eliminate space before +Inf for float image
    The image of an infinite floating-point value (returned by the Image attribute) includes a space before +Inf, but that leads to ugly and inconsistent formatting, so that space is now removed. We prefer to include the + explicitly in this case to emphasize that it is a positive infinity, but the + belongs in the space reserved normally for a minus sign.

  • SPARK Pro
    Jul 7th, 2014

    Ignore dynamic predicates and type invariants
    SPARK toolset now issues a warning on dynamic predicates and type invariants in the code, and proceeds with analysis as if they were not in the code, instead of issuing an error that would prevent any analysis.

  • GNAT Pro
    Jul 3rd, 2014

    Package IDE accepted in all project files
    The package IDE is now accepted in all the project files, including aggregate and aggregate library projects.

  • SPARK Pro
    Jul 3rd, 2014

    Better proof with variables initialized by default
    The SPARK toolset now assumes default initialization for variables with no explicit initialization. This results in more proved verification conditions.

  • CodePeer
    Jul 3rd, 2014

    New checks for parameter aliasing on calls
    CodePeer now attempts to create preconditions for cases where a subprogram might have unwanted aliasing between a composite formal parameter and other parameters or global variables. This can result in messages about possible "aliasing check" violations on calls (and potentially within subprograms when preconditions aren't successfully created).

  • GB: SPARK2014 Traces support
    Selecting a SPARK2014 Problem marker having an associated trace, highlight the source lines containing a trace. Selecting again the same marker hides the highlighted lines.

  • SPARK Pro
    Jul 1st, 2014

    Limit analysis to a single check
    GNATprove's analysis can be limited to single checks with the new --limit-line format (--limit-line=file:line:column:checkkind) or through GPS' SPARK contextual menu "Prove Check".

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jun 25th, 2014

    GPS: remove Search in Project view
    In the /Navigate/Find or Replace dialog, there is no longer a context to search in the project view. Instead, users should use the new filter in the Project view. Editors still have a "Locate in Project view" contextual menu.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jun 25th, 2014

    GPS: not grouping by directories in Project view
    A new setting in the Project view was added to show files directly underneath projects, and not grouped by directories.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jun 25th, 2014

    GPS: support for auto-completion in Python
    GPS now provides smart completion in Python files, providing completion for modules found in the standard Python search paths and all source directories for projects that list "Python" as their language. This is done through an integration of the Jedi library. <https://github.com/davidhalter/jedi>

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jun 25th, 2014

    GPS: show runtime files in Project view
    The Project view now has a setting to show the runtime files.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    Jun 24th, 2014

    GPS: filter in project view
    The Project view now includes a filter in its local toolbar. A number of additional settings were also added to its local config menu: hiding object directories and sorting imported projects before directories.

  • configure: search for sqlite in path/lib64
    When a path is passed to configure's --with-sqlite switch, we now test both the lib and lib64 directories.

  • GNAT Pro
    Jun 20th, 2014

    ASIS: better processing of configuration files
    Now for each configuration file involved in a compilation a separate A_Configuration_Compilation unit is presented in the ASIS Context. Asis.Compilation_Units.Text_Name query now returns the full path to the configuration file when applied to A_Configuration_Compilation unit.

  • GNAT Pro
    Jun 18th, 2014

    New mathematics library on bareboard platfoams
    A new mathematics library written in Ada is now used instead of newlib for bareboard platforms. It is much easier to recompile it.

  • SPARK Pro
    Jun 17th, 2014

    Improved proof for discriminant checks
    The SPARK toolset now handles values of discriminants of discriminant records better. As a consequence, proof of discriminant checks and other checks related to discriminant records is improved

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

    GPS: filter empty directories in Project view
    A new filter was added to the Project view to hide empty directories.

  • SPARK Pro
    Jun 16th, 2014

    Better handling of dynamic types
    The SPARK toolset now tracks bounds of dynamically constrained arrays and discrimiants of dynamically constrained records better. This results in more proved verification conditions.

  • GNAT Pro
    Jun 16th, 2014

    Missing entity messages given even in -gnatc mode
    In No_Run_Time mode or configurable run-time mode, messages for missing entities (corresponding to unsupported features) are now given even when compiling in -gnatc mode.

  • GNAT Pro
    Jun 16th, 2014

    Better handling of info messages
    The count of info messages is now listed separately from the warning message count in a full listing, and -gnatwe never causes info messages to be treated as errors.

  • GNAT Pro
    Jun 13th, 2014

    Syntax only check without a runtime
    It is now possible to invoke the compiler with -gnats and to use gnatchop even when the runtime is not available.

  • GNAT Pro
    Jun 12th, 2014

    Clock and PLL declarations added to System.STM32F4
    The package System.STM32F4 (available on arm-eabi in runtimes for stm32f4) has been augmented with declarations for the clocks and PLLs. The clock configuration is now defined in System.BB.Parameters.

  • GNAT Pro
    Jun 11th, 2014

    GNAT.Regpat: support for non-capturing parenthesis
    It is now possible to use regular expression using the (?:...) syntax to indicate a non-capturing parenthesis.

  • Ada Web Server
    Jun 7th, 2014

    Add support for WSDL extension
    WSDL extension are now recognized and wsdl2aws will generate proper Ada code.

  • SPARK Pro
    Jun 4th, 2014

    Improved tool output in case of errors
    The message issued by the SPARK toolset in case of errors in the source code has been improved. A confusing message involving gprbuild has been suppressed and the formulation of another message has been improved.

  • GNAT Pro
    Jun 4th, 2014

    Better code for attributes Machine, Model, Rounding
    The object code has been improved on selected architectures for the floating-point attributes Machine, Model, and Rounding.

  • GNAT Pro
    Jun 1st, 2014

    Better support for large files on 32bit systems
    It is now possible to obtain the size of a file using Directories.Size and OS_Lib.File_Length for files larger than 2Gb on 32bit systems. In addition, the use of Os_Lib.Copy_File is now supported for such files.

  • GNAT Pro
    May 31st, 2014

    Improved messages for duplicated case values
    For a case statement over an integer type, if there are duplicated values that are given named constants, use the name of these constants in the error messages instead of the integer values.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 29th, 2014

    GPS: Clear locations view for an individual file
    New contextual menu added to clear Location View from messages for current file only. Corresponding action allows binding key shortcut.

  • CodePeer
    May 29th, 2014

    New “subprogram” field in CSV output
    The CSV output now contains a new field to indicate the enclosing subprogram where the message is generated.

  • GNAT Pro
    May 28th, 2014

    Add support for large files on 32bit systems
    Stream_IO and Direct_IO are now fully functional for files larger than 2GB on 32-bit based systems. Previously such files could be read or written, but positional operations (Set_Index, Index, Size) did not work correctly. Note that this changes some implementation-defined types, notably the declaration of Ada.Streams.Stream_Element_Offset, which may require some modification of clients using any of the streams related packages.

  • SPARK Pro
    May 28th, 2014

    Less false alarms regarding unused statements
    Flow analysis used to issue one unused statement warning per unused record component. This is no longer the case. We now only emit a single warning when no record component is used in any way.

  • Linking with static libpq (postgres)
    It is now possible to link with a static version of the postgres library, by passing its full path to configure's --with-postgres switch.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 26th, 2014

    WB: quickfix support on Wind River Workbench
    Quick fix feature is now available for errors created during VxWorks projects build.

  • GNAT Pro
    May 23rd, 2014

    New gnattest switch—test-duration
    A new switch --test-duration is added to gnattest. This switch causes the generated test driver to print time measurement for each test.

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

    GPS: Review key shortcuts dialog
    This dialog can now be embedded in the main GPS window, and kept open. Changes are automatically changed (the save button was removed). A filter has been added to make it easy to find the proper action or shortcut. User-defined shortcuts are displayed in bold. The icons associated with actions are displayed, for consistency with the rest of GPS. Menus are no longer displayed in the dialog, since it is better to associate the shortcuts with the corresponding action instead. Multiple key themes are provided and can dynamically be switched (the emacs.py plug-in was removed and replaced with an Emacs key theme instead)

  • SPARK Pro
    May 22nd, 2014

    Better proof for bounds of unconstrained arrays
    The SPARK toolset now tracks bounds of unconstrained arrays stored in local variables better, especially when they are modified in a loop. This results in more proved verification conditions.

  • SPARK Pro
    May 22nd, 2014

    Better proof for bounds of unconstrained arrays
    The SPARK toolset now tracks bounds of unconstrained arrays better than before, especially when they are passed to a procedure with mode "in out". This results in more proved verification conditions.

  • SPARK Pro
    May 22nd, 2014

    Improved Look and Feel of GPS integration
    The integration into GPS of the SPARK toolset is now closer to the integration of other tools. The localisation of messages of inlined subprograms and instantiated generics has also been improved.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 21st, 2014

    GPS: “file changed on disk” dialog review
    The dialog that pops up when a file has been modified on the disk has been modified. It will now list all such files in a single dialog (as opposed to having one dialog per file when it gets the focus). There is now also an option for automatically reloading files (which can be undone).

  • SPARK Pro
    May 20th, 2014

    pragma Warnings for proof results
    Pragma Warnings is now fully supported by the SPARK toolset, in particular non-proved checks can be accepted using pragma Warnings (Off), just as was already the case for warnings related to flow analysis.

  • SPARK Pro
    May 20th, 2014

    Use of “aliased” keyword now accepted in SPARK
    Use of the "aliased" keyword in the declaration of an object, a parameter or a record or array component is now allowed in SPARK. What is still not allowed is to introduce aliasing by converting an address to such an entity into a pointer.

  • GNAT Pro
    May 19th, 2014

    New pragma/aspect No_Elaboration_Code_All
    A new program unit pragma and corresponding aspect No_Elaboration_Code_All are added. This aspect applies the restriction No_Elaboration_Code to all parts of the extended main unit (spec, body, and subunits). In addition, it requires that any with'ed unit also have the No_Elaboration_Code_All aspect (thus providing a transitive guarantee that a unit and its dependents all have no elaboration code).

  • GNAT Pro
    May 17th, 2014

    Improved pdf for GNAT user manuals
    The pdf files for the GNAT User's Guide, GNAT Reference Manual, User's Guide supplements for Cross Platforms and High-Integrity Edition, GPRbuild, and GNATstack now are formatted so that the text occupies full-sized pages (versus the "small book" format used previously).

  • GNAT Pro
    May 17th, 2014

    Bind some heap related routines in Win32Ada
    The routines HeapSetInformation and HeapQueryInformation are now available in the Win32Ada binding.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 16th, 2014

    GPS: Setting for background color of expanded code
    It is now possible to change the color of expanded code lines in GPS.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 16th, 2014

    gnatinspect recognizes IDE’Xref_Database
    This attribute is used to specify the location of the xref database. It was so far only recognized by GPS, which set up the appropriate command line switches for gnatinspect. This attribute is now also recognize by gnatinspect itself, so that it creates the database in the right location.

  • SPARK Pro
    May 15th, 2014

    Support functions with mutually recursive spec
    The SPARK toolset now supports subprograms with mutually recursive contracts.

  • SPARK Pro
    May 15th, 2014

    Fewer false alarms involving unreferenced vars
    Flow analysis used to generates warnings about ineffective statements that involved variables which were marked with pragma Unreferenced. This is no longer the case.

  • GNAT Pro
    May 14th, 2014

    Better warnings on non-static protected objects
    The compiler distinguishes between private components of protected types whose size depends on a discriminant, from those whose size depends on some other non-static expression. When restriction No_Heap_Allocation is in force, these two cases lead to different warnings.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 13th, 2014

    GPS: New syntax highlighting engine
    GPS has a new extensible syntax highlighting engine, that will be used for C, C++ and python by default, and is extensible in python, as documented in GPS user's guide.

  • GNAT Pro|GPS | GNAT Pro|GNATbench
    May 12th, 2014

    GPS: New technology for documentation generation
    GPS is now shipped with a new command-line tool for documentation generation, called gnatdoc. Amongst the features of GNATdoc are:

      - support of Javadoc/Doxygen style of tags in documentation comments
      - support for comment placement detection
      - support for separating documentation comments from code comments
      - a new extensible HTML back-end
        - support for users defined image directory
        - support for package groups
    

  • GNAT Pro
    May 9th, 2014

    Better error recovery from bad aspect name
    The error message from a bad aspect now includes the bad aspect name, and the recovery is better, avoiding missing useful additional messages, and avoiding unnecessary duplicated messages in -gnatf mode.

  • GNAT Pro
    May 8th, 2014

    More accurate analysis of overflow for division
    The compiler now avoids setting the flag to check overflow on division in many cases where overflow is impossible. This eases proof of absence of run-time errors, and also allows the compiler to do a better job in some cases of detecting conditions whose result is known at compile time.

  • GNAT Pro|GPRbuild
    May 7th, 2014

    Handles Library_Options in gprinstall
    When generating a project for a library (standard or aggregate), gprinstall now adds into the generated Linker_Options the options that were into the Library_Options.

  • GNAT Pro|XML | Ada
    May 6th, 2014

    New subprograms Import_Node and Adopt_Node
    These subprograms, part of respectively DOM level 2 and DOM level 3, are now implemented, and can be used to move or copy one node from a tree to another. In addition, subprograms like Append_Child will now correctly complain when the new node was not created for the same tree.

  • GPS: change icon for root project in Project view
    The icon for the root project is now different from that of other projects, to make it easier to spot the root project.

  • CodePeer
    May 5th, 2014

    Recognize Sqrt with a positive argument is nonzero
    CodePeer now recognizes that a call to the Sqrt (square root) function (as defined in the predefined Generic_Elementary_Functions generic package) with a positive argument will return a result greater than zero, avoiding divide-by-zero messages when the result is used as a divisor.

  • GNAT Pro
    May 3rd, 2014

    Integer overflow checking now enabled by default
    The default behavior of the compiler is changed so that integer overflow checking (as required by the Ada RM) is now enabled by default. A switch -gnato0 is added which disables integer overflow checking (thus reverting to the previous default behavior).

  • GNAT Pro|GPRbuild
    Apr 29th, 2014

    Limit SAL content to the closure of the interface
    When using gprbuild to build a Stand-Alone Library, only the closure of the Ada interface is compiled, bound and put in the library file.

  • GNAT Pro
    Apr 26th, 2014

    Valid_Scalars attribute for variant record types
    The 'Valid_Scalars attribute can now be applied to variant records, and it correctly checks just the variant fields that are present. Note that it is not legal to use 'Valid_Scalars on Unchecked_Union records (or on any type that recursively has an Unchecked_Union component).

  • SPARK Pro
    Apr 23rd, 2014

    The Translator now converts squized assertions
    The translator now converts the following contract:

       while cond
          --# assert inv;
       loop
    
    into:
       loop
          pragma Loop_Invariant (inv);
          exit when not (cond);
    

  • GNAT Pro
    Apr 22nd, 2014

    Secondary stack reclamation during elaboration
    The compiler now reclaims the storage used by the secondary stack during the elaboration of a library level object declaration when the initialization expression contains a function returning a controlled or unconstrained result.

  • GNAT Pro
    Apr 22nd, 2014

    gnat2xml generates representation clauses
    A new switch --rep-clauses causes gnat2xml to generate representation clauses for certain types. Size and Component_Size clauses, as well as record_representation_clauses, are generated as appropriate. These may be used to see the representation the compiler has chosen.

  • GNAT Pro|GPRbuild
    Apr 19th, 2014

    New gprinstall option to copy only project sources
    Using gprinstall's --sources-only option it is now possible to install projects sources only. In this mode it is not required for the project to have been built before.

  • SPARK Pro
    Apr 18th, 2014

    Better provability of checks on floats
    GNATprove now analyzes type bounds of sub-expressions to compute when an overflow check or a range check cannot fail, because these bounds guarantee that the resulting bounds on the result fit into the required range. As a result, many run-time checks on floats that were previously not proved become proved.

  • GNAT Pro
    Apr 18th, 2014

    Implement workaround for FPU store errata on LEON3
    The compiler switch -mfix-ut699 has been enhanced to work around the store forwarding problem of the FPU in Aeroflex Gaisler's LEON3 Microprocessor.

  • GNAT Pro
    Apr 17th, 2014

    New warning on equality of Unchecked_Union objects
    The compiler emits a warning on an equality when the operands are of an Unchecked_Union type and their discriminants cannot be determined statically, resulting in a Program_Error exception being raised.

  • GNAT Pro
    Apr 16th, 2014

    Debugger support for variable length arrays in C
    The debugger has been enhanced to print the value of C variable length arrays correctly. The sizeof operator now also prints the correct value.

  • SPARK Pro
    Apr 15th, 2014

    Support contextual analysis of local subprograms
    GNATprove can now analyze local subprograms without contracts in the context of their calls, as if their body was inlined. This makes it possible to get a very precise analysis, without requiring that the user writes a contract on these subprograms.

  • GNAT Pro
    Apr 14th, 2014

    Warn on postconditions for No_Return Subprograms
    The only postcondition that makes sense for a subprogram labeled as being No_Return (using the pragma of that name) is an explicit False test. Any other postcondition is useless and suspicious. A warning (under control of -gnatw.t/-gnatw.T) is now given for such useless postconditions.

  • GNAT Pro
    Apr 13th, 2014

    gnatcheck:—incremental mode
    gnatcheck now supports the --incremental switch, similarly to gnat2xml and gnatpp. --incremental invokes incremental processing on a per-file basis. Source files are only processed if they have been modified, or if files they depend on have been modified. This is similar to the way gnatmake/gprbuild only compiles files that need to be recompiled.

  • GNAT Pro|GPRbuild
    Apr 12th, 2014

    Add a time-stamp in all gprslave’s message
    All gprslave's messages are now prefixed with a time-stamp in verbose mode. This will help tracking down possible issues with the slave.

  • CodePeer
    Apr 11th, 2014

    Compiler-like mode
    A new switch -gnateC is introduced, providing a compiler-like behavior to analyze files one by one quickly, with no global analysis and no database. This switch should be used by calling directly codepeer-gnatmake with -gnatcC -gnateC.

  • GNAT Pro
    Apr 11th, 2014

    New implementation of Ada.Task_Attributes
    The package Ada.Task_Attributes has been reimplemented, taking advantage of RM permission C.7.2(28), and putting a maximum number of task attributes supported to simplify the implementation and make it more efficient (the limit is 32 on most platforms). In addition, a special case is made for task attributes holding an address/pointer-sized object (or something smaller) and whose Initial_Value is 0 (or null for access types) which is more efficient and doesn't require the use of an indirection (and therefore, no extra dynamic memory allocation, and no locking). In addition, Ada.Task_Attributes now supports also foreign threads (created outside Ada).

  • GNATCOLL.Xref.Get_Entity searching in all files
    It is now possible to call Get_Entity and look for that entity in all sources of the project, rather than in a specific file.

  • SPARK Pro
    Apr 8th, 2014

    Contracts of functions available in assertions
    An axiom is now generated for contracts of non-recursive normal functions. As a consequence, the contracts of non-recursive normal functions is now available for proof even if the function is called in a contract or an assertion.

  • GPS: Show “withs” in Outline view
    New filter in Outline view enables visualization of with-clauses in current compilation unit to find them easier among unsorted clauses and comments.

   1  2  3     Next »