Development Log

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

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

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

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

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

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

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

  • 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
    Jul 15th, 2014

    New query in Asis.Extensions (Is_Definite_Subtype)
    A new test query Is_Definite_Subtype is added to Asis.Extensions package. The query detects if the argument is a declaration of a definite subtype.

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

   1  2  3     Next »