Development Log

  • CodePeer
    Oct 29th, 2014

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

  • GNAT Pro
    Oct 29th, 2014

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

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

  • SPARK Pro
    Oct 24th, 2014

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

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

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

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

  • GNAT Pro
    Oct 23rd, 2014

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

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

  • GNAT Pro
    Sep 27th, 2014

    Support for 32bit and 64bit Windows registry views
    GNAT.Registry has been enhanced to be able to open or create a key into either of the registry view on Windows 64bit.

  • SPARK Pro
    Sep 26th, 2014

    New categorization of messages
    The SPARK toolset used to issue not suppressible errors for violations of legality rules and important analysis problems, and suppressible warnings for less severe problems and suspicious situations. There is now a third category of messages, called checks. Some previous errors and warnings have become checks. The new categorization is that only violations of legality rules are errors, only suspicious situations are warnings, and all messages which impact the soundness of the code or the tool output are checks. Checks are suppressible, but the mechanism for suppression is different, so this represents an incompatible change. See the users guide for more details about messages and how to suppress them.

  • GNAT Pro|GPRbuild
    Sep 26th, 2014

    gprconfig issues an error for compiler not found
    When gprconfig cannot find a compiler for a language specified with a switch --conf, it now issues an error, even in quiet mode, indicating the language, the target and the runtime.

  • PolyORB
    Sep 23rd, 2014

    Lifted limitations on IAC command line
    IAC used to support only 64 preprocessor arguments, and 64 search path elements at most. Both limitations have been removed.

  • CodePeer
    Sep 22nd, 2014

    Ability to exclude source files from analysis
    A new project attribute Excluded_Source_Files in package CodePeer is available to easily exclude source files from analysis.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Sep 19th, 2014

    GPS: outline showing C structs and typedefs
    The outline will now show entries for the named C structs (i.e. not those defined as part of a typedef). For instance, "struct foo {}" and "typedef struct foo bar" will generated entries, but not "typedef struct { ... } bar"

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Sep 19th, 2014

    GPS: alignment preserves the selection
    When using the contextual menu Align, this will now preserve the selection so that multiple such commands can be chained.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Sep 18th, 2014

    CodePeer: display check kinds for messages
    GPS and GNATbench now display corresponding check kinds for CodePeer precondition messages. GPS allows filtering out messages based on these check kinds.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Sep 18th, 2014

    GPS: save scenario on exit and restore on startup
    The value for the scenario variables is saved when GPS exits or you load a new project, and restored when the same project is loaded in the future (unless a new value is specified via environment variables or the -X command line parameter).

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

    GPS: Review handling of auto-saved files
    When you open a file for which there exists an auto-save file, GPS displays a dialog asking whether you would like to load this auto-save file instead of the actual file. This dialog was enhanced with the following capabilities: not displayed when the auto-save file contains the same thing as the file itself; loading the auto-save file can be undone, thus ending with the actual file, or redone, thus going back to the auto-save file.

  • GNAT Pro
    Sep 17th, 2014

    Better error msg for illegal deferred constants
    The compiler provides a more explicit message when a deferred constant is declared with an anonymous array type, explaining that the type of the full declaration is a different type.

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

    GPS: remove the GPS Shell console
    Although the GPS shell scripting is still supported for this language, the console itself has been removed. We recommend using the Python console instead. Most commands are available there, with the following replacements possible:

              GPS Shell         |    Python
                  cd            | os.chdir('...')
                  pwd           | os.getcwd()
                  ls            | os.listdir('...')
                  help          | help(...)
    

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

    GPS: save browser contents in desktop
    When GPS is restarted, the contents of the various browsers (call graph, project dependencies, file dependencies or entities) is restored.

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

    GPS: new File Operations menu in project view
    The File Operations menu, already available in the Files view, has also been added to the Project view. Through this contextual menu, it is possible to easily create new files or directories, rename existing files or directories, and delete them.

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

    GPS: folding compartments in entity view
    It is now possible to fold the attributes or operations compartment in the Entities browser. A new local configuration is also available to chose whether to display fully qualified names or simple names for the boxes.

  • GNAT Pro
    Sep 16th, 2014

    Support for C/C++ xrefs and symlinks
    The -fdump-xref compiler switch for C and C++ sources no longer resolves symbolic links under unix systems, thus allowing generation of cross references on the direct files, as used by e.g. some CM systems.

  • CodePeer
    Sep 11th, 2014

    Faster processing of enumeration type data
    CodePeer has improved the analysis of very large enumeration type declarations.

  • GNAT Pro
    Sep 8th, 2014

    Improve recognition of misspelled aspects
    The compiler now does a better job of recognizing and diagnosing misspelled aspects (such as Prelaborate for Preelaborate).

  • GNAT Pro
    Sep 8th, 2014

    Improve error recovery for bad comma/semicolon
    The compiler now gives a clearer error message for the case of an extra comma or semicolon after a logical phrase when more follow (e.g. X > 3; and then).

  • GNAT Pro
    Sep 7th, 2014

    Implement No_Tagged_Streams pragma and aspect
    A new pragma No_Tagged_Streams allows selective suppression of generation of stream routines for tagged types for which no stream operations are used. There are two forms, one with no parameters which appears in a package spec or declarative region and applies to all subsequent declarations of root tagged types in the package or declarative region, and one with an argument that names a specific root tagged type for which streams are not allowed. The latter form has a corresponding aspect.

  • PolyORB
    Sep 6th, 2014

    Changed preference order for Ada compiler
    When looking for an Ada compiler, the PolyORB configure scripts now favor "gcc" over "gnatgcc" or "adagcc". The default Ada compiler can always be overridden at configure time using the "ADA" environment variable.

  • GNAT Pro
    Sep 4th, 2014

    Inter-unit inlining of instantiated subprograms
    The compiler now considers instantiations of generic subprograms subject to pragma Inline or with an Inline aspect as equivalent for inter-unit inlining to regular subprograms subject to the pragma or aspect. Previously they were much less likely to be inlined across units.

  • SPARK Pro
    Sep 4th, 2014

    Individual checks for each Loop_Invariant Pragma
    For a given loop, the SPARK toolset used to generate a single check for all loop invariant pragmas in a group of loop invariants of that loop. This made it difficult to see which loop invariants were not proved. Now, the SPARK toolset generates a check for each Loop_Invariant pragma individually.

  • Ada Web Server
    Sep 3rd, 2014

    Add support for controlling WebSocket lifetime
    It is now possible to control the WebSocket's lifetime. First the new configuration option Max_WebSocket can be used to allow a maximum of simultaneous opened WebSocket and so avoid using all operating system file descriptor. Second the new configuration option WebSocket_Timeout can be used to control the time without activity after which a WebSocket is in timed-out mode. A timed-out WebSocket can be closed if the maximum number of WebSocket is reached.

  • GNATCOLL.Email: Reset multipart to single part
    Procedure Convert_To_Single_Part now takes an additional formal parameter Purge (default False). When Purge is set True, the message is reset to an empty single part text/plain payload, regardless of previous contents.

  • CodePeer
    Sep 2nd, 2014

    Switch -update-scil now enabled by default
    The switch -update-scil is now the default, so can be omitted. A switch -no-update-scil is provided for compatibility with the previous default behavior in the rare cases where it is useful to separate SCIL generation from codepeer analysis. This means that a typical launch of codepeer now looks like:

      codepeer -P<project>
    

  • GPS: on-the-fly syntax error reporting for Python
    GPS now runs the pep8 syntax checking library on Python source editors and reports errors as you type.

  • GNAT Pro
    Aug 29th, 2014

    Improve error message for illegal iterator
    The compiler provides an improved error mesage on an Ada 2012 iterator specification whose name is a function call, when the function does not yield a type that implements the predefined iterator interface.

  • GNATCOLL.SQL: support for bigint
    Add support for the standard sqlite type BIGINT, mapping to a Long_Long_Integer.

  • GNAT Pro
    Aug 28th, 2014

    Parameter for Positional_Parameters gnatcheck rule
    A parameter is added to the gnatcheck Positional_Parameters rules, it causes the rule to flag all the positional associations that can be replaced with named associations according to Ada rules.

  • GNAT Pro
    Aug 22nd, 2014

    Pragma/aspect Suppress_Initialization for variables
    Suppress_Initialization can now be used as a boolean aspect as well as a pragma, and now applies to variables as well as types. When applied to a variable it suppresses all implicit initialization for that variable.

  • GNAT Pro
    Aug 22nd, 2014

    Improved messages in configurable run-time mode
    The error messages for unsupported features in a configurable run-time have been enhanced for the cases of task rendezvous not supported, and specified array packing not supported. Instead of just listing the (possibly obscure) name of the missing entity in these cases, a clear error message is now given saying that the feature is not supported. In the latter case an error is now issued on the array type declaration itself, as well as on packed operations.

  • SPARK Pro
    Aug 21st, 2014

    Support for manual proof with Coq
    GNATprove now offers suppor to use of Coq to manually prove SPARK 2014 VCs. This includes:

       - Extraction and verification of files containing SPARK 2014 VC that must
         be completed by the user with proof.
       - Definition of a project attribute to specify the location of VC files.
       - Communication with GPS environment for SPARK 2014 to perform manual
         proof from the IDE.
    

  • GNAT Pro|GPRbuild
    Aug 20th, 2014

    —target and CodePeer mode
    When gprbuild is called with switches --codepeer and --target, it now issues a clear error message indicating that these two switches cannot be used simultaneously, instead of hard to understand errors such as:

        no languages defined for this project
    

  • CodePeer
    Aug 20th, 2014

    Compiler specific libraries
    CodePeer now provides compiler specific libraries to ease analysis of Ada code used with most compilers.

  • GNAT Pro
    Aug 19th, 2014

    Pragma Warnings with string literal OK in Ada 83
    The compiler now accepts the two argument form of pragma Warnings in Ada 83 with a string literal as the second argument. This was previously not allowed because a static string expression was required, and there is no such thing in Ada 83.

  • SPARK Pro
    Aug 19th, 2014

    Support for Default_Initial_Condition
    Both proof and flow analysis now support aspect Default_Initial_Condition.

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

    Improved indentation of conditional expressions
    Indentation of Ada 2012 conditional expressions (if and case expressions) spanning multiple lines has been improved.

  • GNAT Pro
    Aug 17th, 2014

    New application unit System.Atomic_Counters
    The unit System.Atomic_Counters is now officially available to application programmers. This unit provides an atomic counter type, along with increment, decrement and test operations using hardware synchronization primitives. It is available for most targets: See documentation for complete list of supported targets.

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

    GPS: auto-load plugin
    GPS now loads project-specific plugin named <project>.ide.py when root <project>.gpr is open.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Aug 14th, 2014

    GPS: defining tool switches no longer needs size
    When you define new tool switches with <tool><switches...></tool>, you no longer need to define the "lines" and "columns" attributes, which are computed automatically.

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

    GPS: Save callgraph browsers across sessions
    The contents of the callgraph browser is now saved when GPS exits, and restored the next time it is restarted.

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

    CodePeer: Read-only message review dialog
    The CodePeer message review dialog now prevents changes the message review status when a message was reviewed in the source code with pragma Annotate.

  • CodePeer
    Aug 12th, 2014

    Faster generation of messages
    The generation of messages has been improved, which is particularly noticeable when lots of messages are generated.

  • SPARK Pro
    Aug 12th, 2014

    Use of volatile objects in type conversions
    Volatile objects with enabled properties Async_Writers or Effective_Reads can now appears as the expression of a type conversion.

  • GNAT Pro
    Aug 11th, 2014

    -gnatn is equivalent to -gnatN on non-GCC targets
    For non-GCC targets, such as JVM, .NET, and AAMP, -gnatn now enables inlining in the front end, and is thus equivalent to -gnatN on these targets.

  • GNATCOLL.Atomic: new package
    This package provides some task-safe, low-level subprograms, which are implemented via CPU-supported atomic operations when possible.

  • GNAT Pro
    Aug 10th, 2014

    Improved accuracy of warnings with pragmas involved
    The treatment of variables for which pragmas such as Shared are given has been improved to give more accuracy in the warnings when a variable is not referenced (for example, appearence in pragma Shared does not count as a reference for the purpose of this warning).

  • GNAT Pro
    Aug 10th, 2014

    Improve casing of identifiers in error messages
    The casing of identifiers in error messages has been improved by copying the exact casing from the source program in cases where this is possible.

  • GNAT Pro
    Aug 9th, 2014

    New pragma Prefix_Exception_Messages
    A new configuration pragma Prefix_Exception_Messages sets a mode in which raise statements using "raise with" where the message is given as a static string expression add an automatic prefix to this string consisting ot the name of the enclosing entity (identifying the package and subprogram). This mode is automatic for run-time library routines, which makes it easier to tell where an exception message came from.

  • GNAT Pro
    Aug 7th, 2014

    Sockets implemented for arm-linux-android
    Sockets have been implemented for the arm-linux-android eabi toolchain.

  • SPARK Pro
    Aug 6th, 2014

    Quantification on type with Iterable aspect
    Generalized loop iteration is now supported in quantified expressions using a new, more SPARK friendly, mechanism for defining an iterable container type.

  • GPS: support for auto-indentation in Python
    GPS provides auto-indentation for Python files.

  • CodePeer
    Aug 4th, 2014

    Support for -U and -U main_file switches
    CodePeer now supports switches -U (analyze all files from the project) and -U main_file (analyze only the closure of the specified main file) on the command line.

  • GNAT Pro
    Aug 3rd, 2014

    Add warning for access to atomic record component
    If X.Y is referenced where X is an atomic object and Y is a non-atomic component, the RM does not specify exactly what mechanism is used to do this access. In particular there is no guarantee that this will be done using a full access to X. A warning is now given in this situation if X has an address clause, typical of the memory mapped I/O case, that the result may not be what is expected (there are several possible different expectations in this case).

  • GNAT Pro|GPRbuild
    Aug 2nd, 2014

    Better reactivity for gprslave
    The locking circuitry of gprslave has been rewritten completely to ensure better responsiveness to multiple requests. For example, now a gprclean distributed request won't have to wait the end of compilations.

  • GNAT Pro
    Aug 2nd, 2014

    Implementation aspect Obsolescent
    A new implementation-defined aspect Obsolescent is implemented that is equivalent to the existing implementation defined pragma of the same name.

  • GNAT Pro
    Aug 1st, 2014

    Improved error recovery for bad aspect syntax
    Omitting => in an aspect definition could causee a "compilation abandoned" message when operating with -gnatQ mode to force semantic analysis of the program, This is now fixed, and the compiler recovers gracefully,

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

    GPS: CodePeer messages grouping in Locations view
    All CodePeer messages (SCIL compilation errors, warnings and checks, race conditions) are displayed in one category in Locations view.

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

  • Ada Web Server
    Jul 23rd, 2014

    Add support for WebSocket unique identifier
    This UID can be used to reference a WebSocket without having to copy the actual object. It is possible to send messages to this specific WebSocket.

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

  • GNAT Pro|GPRbuild
    Jul 17th, 2014

    Switch -a accepted with a warning
    To ease migration from gnatmake to gprbuild, switch -a is now accepted by gprbuild. However, this switch has no other effect than to issue this warning:

       warning: switch -a is ignored and no additional source is compiled
    

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

   1  2  3     Next »