========================== 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.