==========================
SPARK 19 NEW FEATURES LIST
==========================

Copyright (C) 2021, AdaCore and Altran UK Limited

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

NF-RA29-047 Better heuristic for array initialization in loops (2019-03-01)

  GNATprove can now detect initialization of arrays through a FOR
  loop also when one of the array bound is dynamic and the other
  bound is static. Previously it could only detect initialization of
  arrays whose both bounds are of the same kind, i.e. either both
  are dynamic or both are static.

NF-R920-002 Preconditions for Main programs now provable (2018-09-21)

  SPARK generates a special precondition check for main programs,
  that corresponds to the implicit call to the main program after
  elaboration. This check was previously unprovable in many cases,
  because in general it depends on the initial_condition aspects of
  the with'ed packages. Now, these initial_condition aspects are
  assumed when proving this special precondition check, so the check
  becomes provable.

NF-R917-001 Explanation given for missing precondition (2018-09-21)

  When the cause of an unproved check may be a missing precondition,
  GNATprove now issues an explanation pointing to the faulty
  precondition in some cases. This is an extension of the existing
  mechanism for explanations about missing postconditions and loop
  invariants.

NF-R913-019 Improve message related to Initializes (2018-09-13)

  We now emit a clearer message when an input is missing from the
  Initializes contract.

NF-R912-008 Avoid blowups at levels 3 and 4 (2018-09-13)

  To avoid blowups when analyzing large and complex files at levels
  3 and 4, GNATprove no longer tries to split paths at these levels.
  Instead, timeouts are increased. This should make the comparative
  slowdown between levels more predictable.

NF-R903-021 Detect initialization of nonstatic arrays in loops (2018-09-04)

  GNATprove could already detect when an array is initialized in a
  FOR loop, but only for arrays with static bounds. Now it can also
  detect initialization of single-dimensional arrays with nonstatic
  bounds.

NF-R815-024 Possible explanations added to unproved messages (2018-09-14)

  When possible, GNATprove now includes an explanation for unproved
  check messages, pointing to the missing loop invariant or
  postcondition that should constrain the values of relevant
  variables to prove the property. The explanation, when available,
  follows the initial part of the message such as
  file:line:col: severity: check might fail
  with a possible explanation in square brackets such as
  [possible explanation: loop xxx should mention Var in a loop
  invariant] [possible explanation: call xxx should mention Var in a
  postcondition]
  The explanation is not guaranteed to be always correct, but it has
  shown to be in general accurate and useful.

NF-R808-039 Always unroll for-loops executed only once (2018-08-13)

  Loops of the form "for J in 1 .. 1" are used to simulate forward
  gotos with loop exits. They are now always unrolled in proof when
  no loop (in)variant is provided, leading to more precise analysis
  by GNATprove.

NF-R807-002 CCG runtime found automatically from project file (2018-09-11)

  When using GNATprove to analyze code that is compiled into C with
  the GNAT Common Code Generator (CCG), the appropriate runtime can
  now be found automatically when specifying the value "c" for the
  Target attribute and the value "ccg" for the Runtime attribute in
  the project file.

NF-R725-034 New warning by proof on unreachable branches (2018-07-30)

  When using switch --proof-warnings, a new warning may be issued by
  proof on unreachable branches in assertions and contracts. This
  applies to branches in if-expressions and case-expressions, to
  expressions inside quantified-expressions, to consequences of
  Contract_Cases and to right-and-side of lazy boolean operations.
  These correspond in general to errors in specifications, either in
  the assertion/contract where the warning is reported, or in other
  specifications that cause such a branch to become unreachable.

NF-R723-013 Support for memory limit for SPARK provers (2018-07-26)

  The provers run by the SPARK tool to discharge checks can consume
  a lot of memory. Now it is possible to limit the amount of memory
  used by a single prover run, similarly to time and step limits.
  Also, the various levels accessible via the --level switch now
  contain a memory limit in addition to the time limit.

NF-R713-031 Better handling of variables of a fixed point type (2018-07-17)

  Variables of a fixed point type are now handled in a more
  efficient way by the tool, resulting in slightly better proof
  results and more counterexamples for these variables.

NF-R710-028 New check on X'Old when subprogram body not in SPARK (2018-07-10)

  GNATprove now generates checks for possible runtime errors in
  evaluating X on entry to a subprogram, as a result of the use of
  X'Old in a postcondition or a contrat case, even when the
  subprogram body for the corresponding subprogram is not in SPARK.

NF-R709-005 Membership tests for arrays are now supported (2018-07-10)

  GNATprove now supports membership tests whose tested type is an
  array type.

NF-R706-020 SPARK lemmas for monotonicity of exponentiation (2018-07-23)

  The lemma library now provides two lemmas for monotonicity of
  exponentiation on signed integers.

NF-R629-018 GNATprove issues a warning on unit not in SPARK (2018-08-01)

  When a user uses switch -u to analyze specific units, GNATprove
  now issues a warning if the main declaration of that unit is not
  marked as being in SPARK (with SPARK_Mode=>On) or out of SPARK
  (with SPARK_Mode =>Off). This avoids confusion for beginners who
  do not understand why GNATprove does not analyze the body which
  they are asking to analyze.

NF-R622-041 Better information about scoped variables (2018-07-05)

  When verifying a package nested inside the declarative part of a
  subprogram, GNATprove now propagates the fact that the
  precondition of the enclosing subprograms holds. This results in
  more discharged checks in packages declared inside the declarative
  part of a subprogram.

NF-R618-026 Better counterexamples for private types (2018-06-25)

  Counterexamples have been improved for values of private types or
  private extensions. Values should now be printed for components
  which are private, as long as they are not declared in a part with
  SPARK_Mode Off.

NF-R618-018 Improve message on missing global (2018-09-13)

  When a global is missing from a Refined_Global or Refined_Depends
  we now issue a clearer message suggesting to also add this global
  to the relative Global or Depends contract.

NF-R601-048 SPARK outputs list of all message categories (2018-06-22)

  The gnatprove tool now supports the switch --list-categories. If
  this switch is provided, the tool outputs a list of the categories
  of all messages that the tool can possibly issue.

NF-R531-025 GNAT-specific lemmas on fixed-point arithmetic (2018-06-08)

  A new unit in the SPARK lemma library provides three GNAT-specific
  lemmas about the behavior of division between a value of a fixed-
  point type and an integer. These lemmas rely on the use of integer
  division by GNAT compiler for these operations, which guarantees
  monotonicity and rounding properties.

NF-R529-008 Gnatprove now supports the --subdirs switch (2018-06-12)

  The --subdirs switch is a standard switch for tools that process
  project files. If provided, any artifacts produced during the
  analysis are created in subfolders of the directory provided to
  the --subdirs switch.

NF-R509-011 Library of higher order functions over arrays (2018-06-06)

  A library providing higher order functions over arrays has been
  added to the SPARK Lemma Library. It provides several versions of
  Map for one-dimensional arrays, Fold for both one-dimensional and
  two-dimensional arrays, as well as common instances of Fold,
  namely Count and Sum, over the same arrays. General purpose lemmas
  are also provided for Count and Sum.

NF-R508-022 Unroll loops with dynamic bounds over small range (2018-05-11)

  GNATprove can now unroll loops with dynamic bounds over a small
  range, when they satisfy the conditions for loop unrolling (in
  particular, they should not contain a loop invariant). As before,
  this additional unrolling can be suppressed with --no-loop-
  unrolling.

NF-R502-056 Highlight path for missing dependency in GPS (2018-07-30)

  The GNATprove tool can now highlight in GPS the path for a
  dependency missing from the Depends contract.

NF-R423-012 New warning by proof on dead code after loop (2018-04-24)

  A new warning in GNATprove signals when the code after a loop is
  unreachable. This might be either because the loop never exits
  normally, or because the loop itself is unreachable. Special care
  is taken not to issue the warning on statements meant to signal
  abnormal execution, like a raise statement. This warning is
  triggered by switch --proof-warnings and can be suppressed like
  other warnings. It is relying on a call to provers, like the
  previously implemented warning on inconsistent preconditions.

NF-R416-004 Better frame condition for loops over slices (2018-04-19)

  GNATprove generates better frame conditions for loops over array
  slices. In particular, it is now able to infer the preservation of
  array components outside of the loop range if updates are only
  done at the position of the loop index.

NF-R411-018 Support Obj'First/Last/Length for volatile object (2018-04-13)

  SPARK and GNATprove now accept that the prefix of an attribute
  reference for attribute First, Last or Length is a volatile
  object. SPARK RM 7.1.3(12) has been updated to include these
  attributes in the list that define a non-interfering context.

NF-R328-003 SPARK now supports --no-subprojects switch (2018-04-26)

  The SPARK tool now supports the --no-subprojects switch. If this
  switch is used, only the root project is analyzed, any other
  projects of the project tree are not analyzed.

NF-R226-017 Support attributes X'Image and X'Img (2018-03-13)

  Ada 2012 has introduced the notation X'Image as an equivalent for
  S'Image(X) where S is the subtype of object X. This is now
  supported in GNATprove, as well as the GNAT-specific equivalent
  attribute Img (which was useful before X'Image was allowed).

NF-R223-017 New distributed example with tagged types (2018-03-02)

  There is a new distributed example named tagged_stacks featuring
  tagged types, inheritance, and dispatching.

NF-R221-047 More precise handling of the 'Image attribute (2018-09-05)

  GNATprove now handles more precisely references to the 'Image and
  'Img attributes. This results in less spurious messages concerning
  potential range checks on string operations involving these
  attributes.

NF-R220-054 Extended support for fixed-point types & operations (2018-03-12)

  Fixed-point types with more values of small are now supported:
  instead of requiring that the small is a negative power of 2 or 5,
  it is sufficient now that the small is the reciprocal of an
  integer. For example, a value of small of (1.0 / 400.0) is now
  supported while it was previously rejected. Operations that mix
  different fixed-point types are also supported now in some cases:
  multiplication and division between fixed-points which result in a
  fixed-point are supported when their respective smalls are
  "compatible" in the sense of Ada RM G.2.3(21). This ensures that
  the result is precisely computed.

NF-R122-044 New switch to treat check messages as errors (2018-03-20)

  Instead of treating unproved check messages as errors by default,
  a behavior introduced by a previous enhancement, this behavior is
  now obtained with the switch --checks-as-errors. The default is
  that such messages are not treated as errors, and do not cause the
  exit status of GNATprove to be non-zero.

NF-R103-025 Improved version output of SPARK tools (2018-01-18)

  When the gnatprove tool is invoked with the --version switch, it
  now not only reports the version of the gnatprove tool itself, but
  also the versions of the Alt-Ergo, CVC4, Why3 and Z3 components
  that are part of SPARK.

NF-QC19-042 Improved behavior for incorrect why3.conf file (2018-01-18)

  The SPARK toolset now issues helpful messages when the user
  specifies an incorrect why3.conf file via the --why3-conf switch
  of gnatprove. Specifically, the tool now checks for the presence
  of a main section in that file, and the existence of the driver
  files specified for each prover.

NF-QC11-016 Better counterexample for quantified variables (2018-08-03)

  GNATprove provides better counterexample values for quantified
  variables from array component iterators or container element
  iterators.

NF-QB30-008 SPARK now ships with why3session executable (2017-12-07)

  The why3session tool, part of the Why3 tool suite, can be useful
  to inspect the Why3 session generated by the gnatprove tool during
  its operation. This tool is now part of the SPARK installation.

NF-QB24-013 Part_Of constituents in non-SPARK code (2017-12-04)

  The SPARK toolset now verifies references to Part_Of constituents
  of single concurrent types when the references appear in non-SPARK
  code. This prevents any undesirable modifications of the
  constituents.

NF-QB20-027 Warning on permissive elaboration model for SPARK (2017-11-21)

  The SPARK toolset now warns when a permissive elaboration model is
  used to verify the rules defined in the SPARK Reference Manual,
  Chapter 7.7. The static elaboration model is the suggested
  elaboration model for SPARK.

NF-QB03-022 GNATprove issues an error status for check messages (2017-11-10)

  When GNATprove issues check messages, it now terminates with a
  non-zero error status. This facilitates the integration of calls
  to GNATprove in Makefiles and similar builders. Note that this
  does not apply to warnings, which can however be considered as
  errors when --warnings=error is set.

NF-QB01-024 Subprogram renaming as primitive of tagged type (2017-11-07)

  The SPARK toolset now implements rule SPARK RM 6.1.1 which states
  that a subprogram renaming declaration shall not declare a
  primitive operation of a tagged type.

NF-QA23-022 Constants as Part_Of constituents (2017-12-01)

  The SPARK toolset now detects illegal usage of constants as
  Part_Of constituents earlier in the processing pipeline.

NF-QA02-024 New SPARK-compatible units for dimensional analysis (2018-08-06)

  It is now possible to rely on units from the GNAT library to do
  dimensional analysis on SPARK code. While the previous unit
  System.Dim.Mks based on Long_Long_Float is still not supported by
  GNATprove on platforms where Long_Long_Float is 128 bits, the new
  units System.Dim.Float_Mks and System.Dim.Long_Mks, based
  respectively on Float and Long_Float, are supported.

NF-Q927-016 Better counterexamples for arrays (2018-07-27)

  GNATprove now avoids printing values for out of bounds indexes
  inside counterexample values for statically bounded array types.

NF-Q915-037 Improve counterexample traces on branches (2018-03-27)

  With level 0 to 2, GNATprove now avoids printing traces for
  inaccessible branches of the code (according to the counterexample
  at hand). For example:
  if A > 0 then
  -- A = 0
    return C;
    -- C = 1
  else
    return C;
    -- C = 1
  end if;
  is replaced by:
  if A > 0 then
  -- A = 0
    return C;
  else
    return C;
    -- C = 1
  end if;
  This avoids printing counterexample values on the first branch of
  the if.
  This improvement should come with a minor added time to generate
  the counterexample.

NF-Q817-011 Improved support for Floating-Point operations (2018-05-17)

  The cvc4 prover used by SPARK has now a vastly improved support
  for floating-point operations. This results in much better support
  for such operations of the SPARK tools as well.

NF-Q802-030 New switch --info to control info messages (2018-09-11)

  GNATprove now issues information messages related to proof only
  when the switch --info is used. Information messages are now
  issued on loop unrolling (with confirmation of loop unrolling when
  successful, or the reason for not unrolling the loop otherwise),
  on subprogram inlining (with confirmation of subprogram inlining
  when successful, or the reason for not inlining the call
  otherwise), and on whether possible subprogram nontermination
  impacts the proof of calls to that subprogram.

NF-Q706-028 More precise messages on potentially blocking calls (2018-04-30)

  Messages emitted by GNATprove about calls to potentially blocking
  operations from protected subprograms now include the exact name
  of the called routine and the exact location of the call
  statement.

NF-Q606-060 Improve messages related to renamings (2018-09-25)

  The tools now issue better messages related to renamings of
  function calls. In particular, they will be more explicit and
  mention the keyword "renaming" instead of "constant".

NF-Q426-004 New Prove Selected Region command (2018-09-14)

  A new switch --limit-region has been added to limit analysis to a
  range of lines inside a given file. This option is accessible from
  GPS through a Prove Selected Region command, available from the
  contextual menu of SPARK whenever a region is selected.

NF-Q313-019 Add counterexamples for floating point values (2018-07-27)

  The SPARK toolset may now provide counterexample values for
  objects of a floating point type. These values are printed as a
  decimal approximation of the actual floating point value in
  scientific notation.

NF-Q113-013 Better messages for constituents of abstract states (2018-04-20)

  When constituents of an abstract state have the same name and
  happen to be declared in different packages, the messages emitted
  by GNATprove are ambiguous. We have now improved those messages by
  appending a prefix to the constituent.

NF-P915-005 Initializing arrays via procedure calls (2018-09-24)

  GNATprove has now been improved to detect initialization of arrays
  via procedure or entry calls in a loop.

NF-P805-023 SPARK processes less unused entities (2018-07-02)

  When processing a unit, the SPARK tools now do not process unused
  entities of other units. As a consequence, large projects with
  code that is mostly not in SPARK, or which does contain very
  little SPARK_Mode annotations, should now be processed much faster
  by the SPARK tools.

NF-P308-055 Improved CodePeer integration in SPARK (2018-06-21)

  The SPARK tool now can take into account checks that have been
  proved by CodePeer via loop unrolling. This leads to more proved
  checks when the switch --codepeer=on is used.

NF-OA26-040 Issue warning on inconsistent preconditions (2018-04-12)

  GNATprove can now issue a warning on preconditions that are always
  False, which denote usually a mistake in defining or formalizing
  the requirement for a subprogram. This warning is not guaranteed
  to be issued on all preconditions that are inconsistent. In
  particular, it is not issued when one conjunct in the precondition
  is statically False (another warning is issued for that case).
  This is the first warning in GNATprove which is issued by proof: a
  prover is called with a very limited timeout of 1 second to try to
  detect if a precondition is inconsistent. This new capability is
  enabled by using the new switch --proof-warnings.

NF-OA19-025 Counterexample values use type bounds (2018-09-20)

  Counterexample values that are close to a bound of their type are
  now printed as a function of this bound. An example of these new
  values is: (Integer'Last - 1). For readability, this is not done
  for trivial values like: (Natural'First + 1) (which is 1).

NF-O820-005 SPARK violation messages now point to root cause (2018-04-05)

  When an entity which is not in SPARK was used in a SPARK context,
  this resulted in a SPARK violation message which was only pointing
  at the entity not in SPARK, but not the root cause for the
  violation. When the root cause was at the end of a chain of
  entities, possibly in some code not explictly marked with
  SPARK_Mode(On), getting to this root cause could be difficult.
  Now, SPARK violation messages include the root cause in many
  cases, to facilitate the understanding of these messages.

NF-O813-018 Support for more fixed-point types and operations (2018-03-28)

  GNATprove now supports fixed-point types whose small is not the
  reciprocal of an integer, as well as all multiplications,
  divisions and type conversions with fixed-point arguments or
  return types, provided the values of smalls involved ensure that
  the result is in the "perfect result set" according to Ada RM
  G.2.3(21-24).

NF-O219-001 GPS displays Analysis Panel for GNATprove results (2018-10-02)

  GPS can display an interactive view reporting the results of
  GNATprove analysis, with a count of issues per file, subprogram
  and severity, as well as filters to selectively view a subset of
  the issues only. This feature becomes available after the
  preference "Display analysis report" is selected in SPARK
  Preferences panel.

NF-K516-007 New proof warning on postcondition always False (2018-07-09)

  A new warning can be issued by GNATprove when switch --proof-
  warnings is set, on subprograms with a postcondition whose body is
  not in SPARK. The warning is issued when GNATprove can detect by
  proof that the postcondition is always False.