==========================
SPARK 18 NEW FEATURES LIST
==========================

Copyright (C) 2021, AdaCore and Altran UK Limited

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

NF-QC15-007 Support for Predicate_Failure aspect and pragma (2017-12-18)

  GNATprove now fully supports the Predicate_Failure aspect of the
  Ada 2012 and the semantically equivalent pragma, which is specific
  to GNAT.

NF-QB01-017 Default initial condition for the File_Type objects (2017-12-19)

  Ada RM implicitly states that objects of the standard File_Type
  are initialized by default. This is now explicitly stated in the
  GNAT standard library in the form of a Default_Initial_Condition
  aspect. As a result, GNATprove no longer emits spurious checks
  about objects of this type not being initialized.

NF-Q915-035 New Manual Proof Feature for SPARK (2017-11-07)

  Using the new Manual proof feature of SPARK, the user can attempt
  to prove checks that the automatic provers shipped with SPARK are
  unable to prove without help. Via a new interface in GPS, users
  can manipulate the proof context using safe low-level
  transformations, to make it easier to solve by provers, or
  completing the proof entirely manually. For example, a witness can
  be given to a postcondition beginning with "for some X".

NF-Q912-021 Support for CWE ids in messages (2017-10-24)

  A new switch --cwe is introduced. When activated, GNATprove issues
  CWE ids in messages when relevant. For example, it will issue one
  for possible divisions by zero.

       file:line:col: medium: divide by zero might fail [CWE 369]

  CWE ids are issued for both check messages and warnings, which may
  originate either in flow analysis or proof.

NF-Q816-008 Ordering of checks for manual proof better preserved (2017-08-23)

  When manual proof is used, the order of checks is important for
  matching existing proofs to the checks. The SPARK tools now
  preserve this order better than previously. This simplifies the
  usage of SPARK tools when doing manual proof.

NF-Q713-033 Automatically unroll static loops w/o loop invariant (2017-07-19)

  Loop invariants are a known difficulty for beginners to use formal
  program verification. At the same time, many loops written in
  exercises and to familiarize oneself with the technology have
  static bounds and a small range. This enhancement implements loop
  unrolling for such loops with static bounds and not too many
  iterations (current threshold is at 20 iterations maximum). This
  way, simple loops with static bounds are proved without requiring
  a loop invariant.
  We let the user decide if she wants to use this feature or not: -
  by only unrolling FOR loops that have no loop (in)variant. - by
  disabling this feature when the switch --no-loop-unrolling is
  used.

NF-Q621-041 No inlining of subprograms visible to child packages (2017-06-28)

  GNATprove no longer inlines subprograms declared in private parts
  of package specifications as part of its "Contextual Analysis of
  Subprograms without Contracts" feature (which is documented in the
  SPARK User's Gude). Such inlining could be confusing for the
  users, because the same code could be provable if located in a
  package body, but not provable if located in a child package. As a
  result a spurious warning of the form "analyzing unreferenced
  procedure" for subprograms visible to child packages is no longer
  emitted.

NF-Q614-053 Enable multiprocesing by default in IDEs (2017-06-15)

  When interacting with GNATprove inside GPS or GNATbench, it is
  desirable that the analysis uses all available cores to go as fast
  as possible. This is now achieved by selecting by default the
  "multiprocessing" mode with -j0. The user can always revert that
  in the analysis/proof panel opened.

NF-Q531-031 Clearer messages default initialized objects (2017-06-26)

  We have improved check messages for out-mode parameters or globals
  of a default-initialized type. Before: "input value of Var will be
  used in Proc", now: "Foo is not set in Proc".

NF-Q525-025 Better precision on functions returning tagged types (2017-05-29)

  GNATprove now tracks better the value of the tag of the result of
  function calls. This will lead to more discharged checks on code
  dealing with functions returning tagged types.

NF-Q519-015 Conversion between arrays with different components (2017-07-21)

  GNATprove now supports conversion between array types with
  different component types as long as the component types are
  statically matching (as allowed by the Ada RM).

NF-Q511-020 Added preconditions to standard numerical functions (2017-05-11)

  Preconditions have been added to functions from the standard
  numerical package Ada.Numerics.Generic_Elementary_Functions, in
  cases that may lead to Numerics.Argument_Error or Constraint_Error
  when called on actual parameters that are not suitable, like a
  negative input for Sqrt. This ensures that GNATprove generates
  corresponding precondition checks when such functions are called.

NF-Q502-017 Use unique names for private record parts (2017-05-03)

  GNATprove now generates unique names for the Why3 translation of
  private parts of distinct record types. This should facilitate
  mappings of these parts to distinct types in interactive theorem
  provers.

NF-Q418-004 Better handling of powers of 2 in modular types (2017-04-20)

  GNATprove now handles better powers of 2 that are of a modular
  type, leading to better proof results. This improvement only
  concerns modular types whose modulus is itself a power of 2.

NF-Q412-006 Improved handling of compile-time-known assertions (2017-04-19)

  Assertions that are known to be true at compile-time are now
  handled in a more efficient way by the SPARK tools. This results
  in shorter running times on projects that contain such assertions.

NF-Q407-026 Use unique names for simple private types (2017-05-02)

  For simple private types (untagged private type with no
  discriminants and full view out of SPARK) we now use unique names
  in Why3 so that they can easily be mapped to distinct existing
  types in interactive provers.

NF-Q407-010 No checks for array conversion with static bounds (2017-06-21)

  GNATprove no longer generates length checks when converting
  between two static array types with equal lengths.

NF-Q407-005 Better handling of discriminant-dependent components (2017-04-20)

  GNATprove now handles accesses to discriminant-dependent record
  components better, leading to more proofs and less spurious
  trivial checks on such components.

NF-Q405-014 SPARK's way of finding runtimes has been improved (2017-08-28)

  Previously, extra setup was required to make SPARK work with a
  non-default runtime, even when the project file contained all the
  information. Now, SPARK uses the same mechanism to find the
  runtimes as gprbuild does; as long as all required tools are
  installed and in the PATH, SPARK will find and use the correct
  runtime according to the --RTS and --target switches passed to it,
  or Runtime and Target attributes defined in the project.

NF-Q315-034 Globals of renamed subprograms in code not-in-SPARK (2017-03-30)

  GNATprove now synthesizes more precise Global contracts for
  subprograms annotated with SPARK_Mode => Off that make calls via
  subprogram renamings. Such calls happen, for example, in instances
  of generic units with formal subprogram parameters.

NF-Q313-012 Empty "others" alternative in Case statement (2017-03-24)

  Flow analysis now detects when an "others" alternative of a Case
  statement corresponds to an empty range and effectively considers
  its sequence of statements as unreachable. This helps to avoid
  spurious messages about variables not being referenced or
  initialized within that sequence of statements.

NF-Q306-008 New switch produces header in gnatprove.out (2017-03-09)

  The new switch --output-header produces a header in the generated
  file gnatprove.out, with useful information about the run of
  GNATprove, such as the version number, date, host platform and
  switches used.

NF-Q306-006 New switch for more modular analysis (2017-03-09)

  We have added a new switch to gnatprove "--no-global-generation"
  which can be used to disable generation of global contracts. In
  essence this means an absent global contract has the same meaning
  as "Global => null".

NF-Q301-007 Protect against unsound function contracts (2017-04-13)

  When a function has an inconsistent contract (a contract which
  cannot hold for some inputs), GNATprove used to generate an
  unsound axiom which may then allow to prove anything in a caller
  of such a function, and so, even if the function is always called
  on 'valid' inputs, that is, inputs on which the contract holds.
  Though this behavior is expected with a proof technology such as
  SPARK, it used to come as a surprise to some users. We now avoid
  generating unsound axioms as much as possible by introducing
  guards for function axioms which are only assumed to hold on
  actually used values. Note that there are still cases where an
  unsound axiom will be generated (functions called in type
  invariants / type predicates, in primitive equalities of record
  types, or sometimes in user written quantified expressions). As a
  consequence, having inconsistent contracts on functions is still a
  bad usage of SPARK, and users should avoid it as much as possible.
  Also, this new 'safer' translation can sometimes impact proof
  capabilities. Thus, we provide an advanced switch --no-axiom-guard
  to disable it.

NF-Q124-055 New switch --no-inlining prevents inlining for proof (2017-01-31)

  The special inlining used in GNATprove to increase the precision
  of proof may be harmful in some cases, as it increases precision
  at the cost of longer running time and greater memory usage.
  GNATprove now supports no inlining under switch --no-inlining.

NF-PC14-017 Support of caching using memcached server (2017-01-05)

  The SPARK tools now support caching large parts of the analysis
  via a memcached server. If a memcached server is available to
  store analysis results, and this server is specified to GNATprove
  via the command line option --memcached-
  server=hostname:portnumber, then subsequent invocations of the
  tools, even across different machines, can store intermediate
  results of the tools. The user-visible effect is that GNATprove
  can produce results faster.

NF-PC14-014 Contracts for formal containers with model functions (2017-02-15)

  The formal containers library, which provides SPARK-compatible
  versions of Ada containers, has been enriched with comprehensive
  contracts. These contracts use functional, mathematical-like
  containers as models of imperative containers.

NF-PC08-013 Improve message for functions that could not return (2017-05-05)

  GNATprove used to emit a confusing check about initialization of
  functions when it could not determine if a function would return.
  We have now improved the message for this check. In addition, when
  encountering a potentially non returning function, GNATprove will
  now precise if the function may not return on some or on every
  path.

NF-PC08-007 Better termination error messages (2016-12-09)

  Every error message related to termination referred to a
  subprogram without specifying the name. This further information
  is now emitted.

NF-PC08-006 Add message on proved termination (2017-01-05)

  When GNATprove is able to prove a Terminating annotation an info
  message is issued.

NF-PC07-016 More precise analysis for exclusive use of entries (2016-12-21)

  Tasks were previously only allowed to call the same entry if they
  were using entries belonging to different (library-level) objects.
  Now GNATprove also accepts calls from more than one task to a
  single entry provided that each task uses an entry belonging to a
  different component of a record object.

NF-PC06-030 Only check component subtype at first declaration (2016-12-07)

  GNATprove now only checks subtype indications on record components
  when verifying the declaration of the first record type defining
  this component. This avoids having multiple checks on record
  component subtype indications, some of which could be undischarged
  due to missing information.

NF-PB30-023 Assume value of string literals (2016-12-01)

  GNATprove now knows precisely the value stored in a string literal
  which will result in more proofs when string literals are
  involved.

NF-PB23-035 SPARK tools produce more information about VCs (2017-01-25)

  Previously, it was hard to see which VCs were produced for a given
  check, and which prover was used to attempt to prove it. Now, this
  information is stored in the .spark files that are produced by
  GNATprove. The content of these files is now documented.

NF-PB23-014 New lemmas on monotonicity of float operators (2017-01-23)

  The SPARK lemma library includes six new lemmas on the
  monotonicity of the float addition, substraction, multiplication
  and division.

NF-PB15-030 Remove trivial checks on float-to-int conversions (2016-11-22)

  Range checks on float-to-int conversions that can be proved to be
  always passing by trivial interval analysis of the types of
  subexpressions are not emitted anymore. This improves provability
  of programs where such conversions are used, as automatic provers
  sometimes had difficulty proving range checks on such conversions.

NF-PB11-005 Better interval analysis of int to float conversions (2016-11-22)

  Interval analysis is a simple analysis that allows proving range
  checks and overflow checks simply by computing the worst-case
  bounds of expressions based on the types of subexpressions. This
  analysis now also deals precisely with conversions from integers
  to floating-point types, which improves provability of programs
  with such conversions.

NF-PA31-008 Static constants not printed in counterexamples (2017-04-26)

  Providing values for static constants in counterexamples is
  useless as their values can be deduced from reading the source
  code. Spark now detects such constant and avoid printing them in
  counterexamples to improve their readability.

NF-PA26-037 Nested loops allowed before a loop (in)variant (2016-10-31)

  A limitation in GNATprove forbade nested loops before loop
  (in)variants. This limitation has been removed.

NF-PA24-021 Assertion checks now proved by CodePeer integration (2016-11-02)

  Assertion checks (pragma Assert, Loop_Invariant, Assert_And_Cut)
  can now be proved by the CodePeer integration in SPARK, which was
  not the case previously.

NF-PA24-020 Division checks now proved by CodePeer integration (2016-11-02)

  Division by zero checks can now be proved by the CodePeer
  integration in SPARK, which was not the case previously.

NF-PA24-004 Improve provability of checks in loops (2016-11-08)

  Checks whose proof depends on assuming the loop invariant at the
  current iteration of the loop could be unprovable due to part of
  the loop invariant being simplified to True or False. This
  simplification is now disabled in assertions to improve
  provability of checks in loops.

NF-PA14-032 Improve tracking of bounds of array aggregates (2016-10-26)

  GNATprove now does a better job of tracking the bounds of
  aggregates of dynamic array types, resulting in more discharged
  checks on array aggregates.

NF-PA12-001 Check default of private types at declaration (2017-01-12)

  GNATprove now checks that no runtime error can occur during the
  default initialization of private types once and for all at the
  declaration of the type. This enforces a cleaner separation of
  library code from user code, allowing for an easier integration of
  proof with other verification means (tests, review...).

NF-P916-032 Support for arbitrary lengths of entry queues (2017-01-06)

  GNATprove now supports arbitrary lengths of entry queues (which
  are specified by the Max_Queue_Length and Max_Entry_Queue_Length
  pragmas). This feature is only applicable when the GNAT Extended
  Ravenscar profile is active.

NF-P915-007 more precise volatility for protected objects (2016-11-03)

  A new rule 7.1.2(16) was added to SPARK RM, along with SPARK tool
  updates, to better control the volatility of protected objects.
  Previously they were fully volatile, now they have only
  Async_Readers and Async_Writers. If a separate volatile variable
  is a Part_Of such a protected object, the protected object
  inherits any volatility aspects (i.e. Effective_Reads or
  Effective_Writes) of its Part_Of constituent.

NF-P914-008 New lemma on array ordering (2016-11-21)

  We have added a new lemma for sorted arrays in the SPARK lemma
  library. This lemma allows proving ordering between arbitrary
  elements of the array using transitivity of the order.

NF-P909-014 Different message for floating point overflows (2017-02-05)

  Previously, for overflows on integer types and floating point
  types, the SPARK check message mentioned simply "overflow check".
  This made it difficult to know if the check was an overflow on
  integers or floating point numbers. Now, the message for floating
  point overflow checks mentions "float overflow check". The message
  for integer overflow is unchanged.

NF-P907-030 Improved error message (2016-11-23)

  In case of a subprogram having an output global which is used as
  an input of the subprogram in its body we now provide more
  information on the error message.

NF-P831-008 Improve message for overridden subprograms (2017-05-31)

  When an overriding subprogram has more effects on globals
  variables than the overridden subprogram, GNATprove will report an
  error message. We have now improved this message making more
  explicit the underlying issue and we have reworded the case when
  these effects are through access types (i.e. pointers).

NF-P729-017 Types with partial default initialization allowed (2016-11-09)

  Types with partial default initialization were previously not
  allowed in SPARK, which made it difficult to analyze some existing
  codebases. They are now allowed.

NF-P518-021 Loop invariant generation for preserved components (2016-11-10)

  GNATprove can automatically generate loop invariants specifying
  the preservation of array and record components that are not
  modified during a loop. This generation is a heuristic which only
  works in the most common cases.

NF-P413-011 Full SPARK elaboration rules (2017-11-27)

  The SPARK Pro toolset now verifies all the rules defined in SPARK
  RM 7.7. Legality checks with respect to calls and tagged types are
  always in effect. The remaining checks are off by default, but can
  be enabled using compilation switch -gnatd.v (Enforce SPARK
  elaboration rules in SPARK code).

NF-P412-021 Better handling of discriminants of protected types (2017-06-16)

  GNATprove now tracks the value of discriminants of protected types
  in a better way, leading to better proof results.

NF-OB17-038 Dynamic type constraints of protected components (2017-02-24)

  GNATprove now better tracks dynamic type constraints of protected
  components, such as dynamic bounds, predicates and invariants.
  This results in more automatic proof on protected operations or
  their callers, whenever types of protected components have some
  dynamic constraints.

NF-O902-020 Simplified translation of simple private types (2017-03-21)

  Untagged private types with no discriminant whose full view is not
  in SPARK are now translated in Why3 as clones of the predefined
  __private abstract type. This should allow users of interactive
  proof assistants to more easily map these private types to a logic
  type of their choice.

NF-O827-017 Precise handling of dispatching calls with known tag (2017-05-10)

  GNATprove now precisely determines the subprogram called by a
  dispatching call when the tag is known. In particular, it is now
  able to use its more precise specific contract if any.

NF-N311-015 Theories for conversion of discrete types realized (2017-03-20)

  The Why3 theories used by GNATprove to model conversions between
  discrete types have been realized in Coq. This increases
  confidence in their correction.