==========================
SPARK 22 NEW FEATURES LIST
==========================

Copyright (C) 2021, AdaCore and Altran UK Limited

This file contains a complete list of new features in version 22 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 22.0w wavefront
subsequent to this date will contain the indicated feature, as will any
subsequent 22 or later release.

NF-U914-008 Suggest precondition in possible fix of message (2021-09-16)

  When GNATprove can determine a sufficient precondition that would
  allow a check to pass, it suggests this precondition as part of
  its message as a "possible fix". Note that the suggested
  precondition may be stricter than necessary. This concerns range-
  related checks (overflow, range, index and length checks) for
  which GNATprove suggests preconditions of the form:

     add precondition (X < Integer'Last - 1) to subprogram at line
  xxx

  as well as division-by-zero checks (on mod, rem, / and other
  operations) for which GNATprove suggests preconditions of the
  form:

     add precondition (X /= 0) to subprogram at line xxx
  .

NF-U824-022 Detect stability in loop exit conditions (2021-09-21)

  Flow analysis now detects when a loop exit condition is stable,
  i.e. when the variables used in the loop exit condition are not
  modified in the loop body. Upon detection of a stable loop exit
  condition, a warning is reported.

NF-U722-041 Better performance when generating VCs for Alt-Ergo (2021-09-14)

  In some cases, the generation of VCs for Alt-Ergo could take a
  long time. We have improved the tool to speed up the VC generation
  for Alt-Ergo.

NF-U721-028 Improve provability of conversions from/to 128 bits (2021-07-22)

  Conversions to and from 128-bit modular integers are better
  interpreted now for provers CVC4 and Z3, leading to more automated
  proofs on code with such conversions.

NF-U716-019 More precise anaysis of function renamings (2021-07-20)

  When a function renaming has a separate spec with a contract, it
  is now treated as an equivalent expression function with the same
  contract, instead of as an implicit body hiding the call to the
  renamed function. This increases precision of the analysis for
  calls to such functions.

NF-U709-012 Warning suppression with a null dependency clause (2021-07-13)

  GNATprove normally emits a warning for a subprogram call that
  modifies a global variable when its value is not used afterwards.
  Now this warning can be suppressed by adding an explicit Depends
  contract with a null dependency clause for the corresponding
  global variable.

NF-U706-017 Return/exit/goto in the scope of local owning object (2021-07-06)

  GNATprove now supports return, exit, and goto statements located
  inside declare blocks containing declarations of local owning
  objects.

NF-U622-049 Support for owning components in tagged root types (2021-06-30)

  SPARK now supports components of an owning type in the root type
  of a tagged hierarchy. Such components are still not allowed in
  tagged extensions.

NF-U608-010 Better tracking of Unbounded_String initialization (2021-09-13)

  Flow now takes into account the default initialization of
  Unbounded_String variables for its analysis.

NF-U601-052 Better tracking of extensions in tagged conversions (2021-06-07)

  GNATprove now tracks hidden components from tagged extensions more
  precisely in view conversions of tagged types. This results in
  more proved checks in the presence of conversions and class-wide
  types.

NF-U528-009 Precise handling of UC between integers in proof (2021-06-07)

  Unchecked_Conversion between signed and modular types of the same
  size is now handled precisely in proof.

NF-U426-011 General access types are supported in SPARK (2021-06-11)

  General access-to-variable types introduced by the keyword ALL are
  now supported in SPARK. They are subjected to an ownership policy
  to prevent aliasing and they cannot be deallocated.

NF-U416-024 External abstract state in non-volatile function (2021-05-03)

  External abstract state (marked with aspect External) may now be
  read inside a non-volatile function (not marked with the aspect
  Volatile_Function) when it has neither the properties
  Async_Writers=>True or Effective_Reads=>True. This extends the
  handling of objects/types which are not "volatile for reading" to
  abstract state over such objects.

NF-U413-014 Access elements in formal containers without copy (2021-05-04)

  The formal containers library now provides Constant_Reference and
  Reference functions which provide read-only and read-write access
  to specific elements inside formal containers without copy. They
  use the ownership policy of SPARK to ensure that the container is
  not tampered with while the reference is valid.

NF-U402-026 Simpler model for dynamic memory (de)allocation (2021-04-27)

  SPARK now uses a simpler model for dynamic memory allocation and
  deallocation, in which allocators and instances of
  Ada.Unchecked_Deallocation neither read nor write a special
  abstract state as was done previously. This change makes it
  possible to deallocate memory inside functions, to allocate memory
  inside nonvolatile functions, and to use allocators more liberally
  inside expressions. See SPARK RM 4.8 for details. A counterpart
  for these usability improvements is that primitive equality
  between objects of pointer type is not allowed anymore in SPARK.
  Such code should be rewritten or marked SPARK_Mode Off.

NF-U302-016 More precise computation of packed array size (2021-05-26)

  GNATprove is now able to compute the object size for packed arrays
  whose component size is specified, even when their type cannot be
  given a corresponding Object_Size (because it is not a static
  value, e.g. in a generic). This makes it possible to check the
  validity of overlays involving such objects.

NF-U301-009 Support for named access-to-constant types (2021-03-23)

  Named access-to-constant types are now accepted in SPARK. The data
  they designate is constant all the way down, even through
  dereferences of access-to-variable parts. Objects of a named
  access-to-constant type are not subjected to ownership checking.

NF-U228-006 Static arrays not required for Unchecked_Conversion (2021-03-01)

  The SPARK tool no longer requires array types to be static when
  used for Unchecked_Conversion or for overlays.

NF-U223-004 Better handling of named numbers in Big_Reals (2021-02-24)

  GNATprove handles the use of named numbers inside expressions of
  type Big_Numbers.Big_Reals in a more precise way. It can now use
  the exact value of such constants in the computation.

NF-U220-008 Pre and postconditions disabled in formal containers (2021-04-14)

  Pre and postconditions from the formal container library are now
  disabled even when the user code is compiled with assertions
  enabled. These contracts are designed for formal verification and
  not execution.

NF-U218-053 Improved reporting of data races for abstract state (2021-07-29)

  If an abstract state is potentially subject to data-race
  conditions (because the state is accessed by different tasks),
  then GNATProve attempts to report this at the level of the common
  state abstraction rather than at the level of the state
  constituents. This used to only work for one "level" of state
  abstraction. Now the report is provided against the most abstract
  level of state that contains all contested constituents.

NF-U211-030 Identifying bounds for unproved range checks (2021-06-18)

  For unproved range and overflow checks, SPARK now reports which
  bound (lower or upper bound) is unproved. This helps finding the
  correct fix for such unproved checks.

NF-U208-007 Better handling of local borrowers in loops (2021-02-10)

  GNATprove will track the values at the end of the borrow of local
  borrower better inside loops. In particular, a loop invariant will
  no longer be needed to know that the value of the borrower at the
  end of the borrow is null if and only if the current value of the
  borrower is null.

NF-U202-015 Relax restrictions of NULL in aggregates (2021-02-02)

  It is now possible to use the literal NULL as the expression in an
  array or record component association whose choice list contains
  more than one element.

NF-U121-019 Detect stability in loop conditions (2021-06-29)

  Flow analysis now detects when a loop condition is stable, i.e.
  when the variables used in the loop condition are not modified in
  the loop body. Upon detection of a stable loop condition, a
  warning is reported.

NF-U120-015 Precise handling of shift operations on signed ints (2021-02-02)

  GNAT supports defining intrinsic shift operations (left, right,
  and right-arithmetic) on signed integers, with the expected
  bitwise interpretation. Previously these operations were accepted
  but treated as unknown operations by GNATprove. They are now
  treated precisely.

NF-U113-026 SPARK accepts attribute Address in more places (2021-01-26)

  Previously, SPARK accepted taking the address of a variable only
  at the top level of an address clause. Now it accepts taking the
  address anywhere inside an address clause, as long as the variable
  is volatile.

NF-TC17-028 Distinguish error messages with "error:" tag (2021-01-07)

  Error messages in GNATprove are now flagged with the "error:" tag
  after the location prefix, to make it easier to distinguish them
  from warnings (starting with "warning:" tag), check messages
  (starting with a tag denoting their severity: "high:", "medium:"
  or "low:") and information messages (starting with "info:" tag).

NF-TC16-016 Type invariants in public child units (2021-01-05)

  GNATprove now supports defining types with type invariants in
  public child units.

NF-TC15-040 Same patterns for pragma Annotate as for Warnings (2021-01-07)

  Justifying checks through pragma Annotate is now based on pattern
  maching messages against the given pattern string using the same
  simple rules as for pragma Warning, instead of the previous more
  complex pattern matching semantics.

NF-TC10-010 Change control over counterexample generation (2020-12-14)

  Counterexamples for unproved checks were previously enabled by
  default, and disabled explicitly with the switch --no-
  counterexample. As counterexamples can be spurious, especially at
  low levels of proof, they are now disabled by default and enabled
  either through the new switch --counterexamples=on or when switch
  --level is used with a value of 2, 3 or 4. The switch
  --counterexamples=off can be used to disable counterexamples
  explicitly at these levels.

NF-TC04-018 Use location spans in messages on the command line (2020-12-11)

  When using GNATprove from the command line, the location for the
  message (error, check, warning or info) is displayed precisely
  with characters that outline the span for the faulty expression.
  This is enabled by default, or when explicitly choosing
  --output=pretty switch.

NF-TC02-027 Validation of counterexamples by simulation (2021-10-08)

  Prior to being displayed, counterexamples generated in case of
  proof failure are validated by a special simulation of the
  corresponding execution, taking into account the specificities of
  loops and calls, so that GNATprove can report when the error
  likely originates in a missing contract or annotation.

NF-TB24-027 Lemma for monotonicity of floating point division (2020-11-27)

  A lemma has been added to the SPARK lemma library. It states that
  floating point division is monotonic with respect to its right
  parameter.

NF-TB19-042 Detect statically dead code in flow analysis (2021-05-21)

  Flow analysis now detects and raises warnings about statically
  dead code in IF and CASE statements.

NF-TB19-013 Support for attribute 'Access (2021-04-13)

  The 'Access attribute is now supported in SPARK. It allows
  borrowing or observing a part of an object temporarily.

NF-TB19-012 Support for Address clauses and overlays (2021-05-04)

  SPARK now takes into account aliases created by address clauses of
  the form "with Address => Obj'Address". If some variable X is
  overlaid on the address of Y, then any read or write of X will be
  considered a read or write of Y, and vice versa. Objects with such
  an address clause cannot appear in global contracts; one has to
  refer to the overlaid object instead.

NF-TB05-028 Add contracts to Ada.Strings.Fixed (2020-12-01)

  The runtime unit Ada.Strings.Fixed has been annotated with
  postconditions. As a result, SPARK now handles subprograms from
  this unit in a more precise way.

NF-TB04-016 Inheritance of the Default_Initial_Condition aspect (2020-11-13)

  Following its inclusion in the upcoming Ada standard, the
  semantics of the Default_Initial_Condition aspect has been
  modified. It is now inherited in type derivations.

NF-TB04-004 Improve display of array values in counterexamples (2020-11-05)

  Counterexamples displayed by GNATprove when a check is not proved
  now contain only those indexes which fit in the array bounds, and
  avoid stating a value for the "others" index when none is needed.
  Values inside arrays are also pretty-printed, so for example
  Integer'Last is displayed instead of 2147483647.

NF-TA27-008 Support for iterator filters (2020-10-30)

  GNATprove now supports disabling iterations inside loops and
  quantified expressions using an iterator filter.

NF-TA21-030 Listing suppressed checks (2021-09-20)

  The analysis results summary file, gnatprove.out, now provides a
  better report of where suppressed checks exist. Entities whose
  body is not in SPARK are now listed. For pragma Assume statements,
  there is now a report stating the number of pragma Assume
  statements used, and their location (subprogram, file, line,
  column).

NF-TA16-005 Improved suggestions for a fix on unproved checks (2020-10-21)

  GNATprove generates better suggestions as part of unproved check
  messages in two cases: when recommending the use of an expression
  function, it indicates when it should be in the spec unit (for a
  client unit to see), and when a check is on the right-hand side of
  an "and" expression in a precondition, and the left-hand side of
  the "and" refers to some of the same variables, it recommends
  using "and then" instead, so that the evaluation of the right-hand
  side is guarded by the condition on the left-hand side.

NF-TA07-006 Add contracts to Ada.Strings.Maps (2020-10-21)

  Pre- and postconditions are added to the subprograms in
  Ada.Strings.Maps. SPARK now generates new VCs for preconditions on
  these subprograms.

NF-T716-026 Use colors in messages for terminal output (2020-12-18)

  When GNATprove is called from a terminal, it now uses SGR (Select
  Graphic Rendition) to highlight different parts of messages, using
  colors and bold font. This is done by default when --output=pretty
  is used, which is the default value for command-line usage. Users
  who do not wish to have colors, or whose terminal does not support
  SGR, can either change the output mode, or call gnatprove piped to
  "cat" on Unix.

NF-S906-022 Better explanations for failed proofs (2021-06-08)

  SPARK can now identify the sub-part of an unproved assertion or
  predicate check. If a predicate check is unproved, and the
  predicate is a conjunction of several parts, SPARK will identify
  the part of the predicate that is unproved in the error message,
  similar to what is already the case for assertions. Furthermore,
  if an assertion is unproved, and the unproved part of an assertion
  is a call to an expression function, and the expression function
  is defined as a conjunction of several parts, SPARK can identify
  the unproved part of that call.

NF-S406-003 GNAT Studio integration: display Global contracts (2021-01-18)

  GNATprove writes to a JSON file the Global contracts generated
  during data-flow analysis. This feature is activated by specifying
  the --flow-show-gg switch when invoking GNATprove. GNAT Studio has
  a new contextual menu, "Globals -> Show generated Globals" to
  activate this feature and insert the Global contracts inline with
  the source code.

NF-S313-025 Improve handling of dispatching equality (2021-09-15)

  GNATprove is now able to determine which specific equality is used
  on a call to the dispatching equality of a tagged type when the
  tag can be determined.

NF-R417-042 Prove termination of expressions in type aspects (2020-12-25)

  Flow analysis now checks that the type aspects Dynamic_Predicate
  and Type_Invariant are defined by expressions that can be proved
  to terminate.