==========================
SPARK 23 NEW FEATURES LIST
==========================

Copyright (C) 2021, AdaCore and Altran UK Limited

This file contains a complete list of new features in version 23 of the
SPARK 2014 toolset. A full description of all SPARK features can be found in
the SPARK 2014 User's Guide and SPARK 2014 Reference Manual.

An ISO date (YYYY-MM-DD) appears in parentheses after the description line.
This date shows the implementation date of the feature. Any 23.0w wavefront
subsequent to this date will contain the indicated feature, as will any
subsequent 23 or later release.

NF-UB05-006 Support for 80-bit extended-precision floats (2021-11-12)

  GNATprove now supports 80-bit extended-precision floating-point
  numbers, which correspond to Long_Long_Float on x86 targets.

NF-UA28-038 Better message for inherited predicate checks (2021-11-02)

  If a type has several applicable predicates, messages associated
  to inherited predicates now have a continuation giving the
  location of the corresponding predicate.

NF-UA22-011 Better messages on inlined expression functions (2021-10-29)

  Expression function calls and type predicates are sometimes
  inlined to provide more precise messages for unproved checks (this
  only occurs for expression functions returning Boolean results).
  In this case, a continuation is added to the corresponding check
  message giving the location of the unproved conjunct.

NF-UA21-035 Counterexamples with Relaxed_Initialization (2021-10-26)

  GNATprove can now give counterexample values for objects annotated
  with the Relaxed_Initialization aspect.

NF-UA13-036 Better messages for checks on default values (2021-10-21)

  GNATprove now emits continuations for messages associated with
  checks occurring in the default value of a type. They give
  information about the point in the code where this default value
  is used.

NF-UA11-049 Improved counterexamples for unconstrained arrays (2021-10-20)

  Checking of counterexamples has been completed for unconstrained
  arrays (in particular the standard String type when
  unconstrained), which leads to more valid counterexamples being
  displayed even when counterexample checking is enabled.

NF-U924-019 Better error messages on misuse of abstract state (2021-11-08)

  Messages issued by GNAT/GNATprove on illegal abstract state
  declarations (typically when the abstract state is not correctly
  refined, or constituents do not correctly declare their attachment
  to the abstract state) now explain the cause of the error, to
  guide users towards a possible fix.

NF-U510-023 Add explanations to initialization checks (2021-11-05)

  This patch adds continuation messages to flow initialization
  checks, with explanations and possible fixes. This happens in two
  cases: when an OUT parameter is not initialized on return, and
  when a package variable is present in the Initializes contract of
  said package and is not initialized after package elaboration.