Development Log in June 2016.

  • SPARK Pro
    Jun 6th, 2016

    Support optional refinement in private part/child
    SPARK Reference Manual now allows refinement through the user of pragma or aspect Refined_Global and/or Refined_Depends in scopes where the full refinement of an abstract state is not visible, like the private part of the package defining the abstract state, or one of its child packages. The special rules in SPARK RM 7.2.4 for this so-called optional refinement are now supported in GNAT and GNATprove.

  • SPARK Pro
    Jun 6th, 2016

    Global variables known to be initialized in loops
    GNATprove now knows that in out global variables and parameters that are modified in loops are always initialized and thus are in their types. In particular, variables are in their range for scalars and their dynamic predicate is true if they have one.

  • SPARK Pro
    Jun 3rd, 2016

    Suppressed wrong warning message for X’Address
    SPARK does not look at X in X'Address as a used variable anymore and therefore it does not emit a warning message in case X is not initialised.

  • GNATCOLL.Atomic: Sync_*_Compare_And_Swap_Counter
    New atomic operations are provided, that change the value of an Atomic_Counter if, and only if, it currently has a given known value. This is useful to write lock-free algorithms.

  • GNAT Pro
    Jun 3rd, 2016

    gnattest: stub parent packages
    Gnattest now generates stubs for parent packages of packages undet test in --stub mode.

  • GNAT Pro | XMLAda
    Jun 2nd, 2016

    unicode names from the Unicode 8 standard
    The unicode-names-* packages were updated to match the Unicode 8 standard. The new bindings are generated via a new importer, which fixes a number of issues with the previous bindings:

       - some characters were put in the wrong block (and thus wrong package)
       - some typos due to incorrect parsing of the Unicode files
       - some name aliases would hide canonical names occurring later (for
         instance 1F5E2 was hidden by 1F48B)
       - some unofficial aliases were used (Bell is not long valid, for
    This change is not fully backward compatible, due to changes in the Unicode standard itself, since some blocks were renamed, as well as some characters. Contributed by Nicolas Boulenguez

  • GNAT Pro
    Jun 1st, 2016

    Improved version of attribute Type_Key
    The attribute Type_Key, which is provided for compatibility with the APEX attribute of that name, now uses a CRC computed from the type declaration of the type, and the declaration of all its components, to provide a reliable signature that allows the detection of changes in the semantics of the type.