========================== SPARK 20 NEW FEATURES LIST ========================== Copyright (C) 2021, AdaCore and Altran UK Limited This file contains a complete list of new features in version 20 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 20.0w wavefront subsequent to this date will contain the indicated feature, as will any subsequent 20 or later release. NF-S916-007 Pragmas Export_Function and Export_Procedure (2019-09-17) SPARK now accepts the use of the Export_Function and Export_Procedure pragmas without issuing a warning. NF-S802-034 Function to remove a mapping from a functional map (2019-08-05) The specification of functional maps has been enriched with a Remove primitive which creates a new map from an existing one by copying all mappings but one. NF-S801-023 Improve location of initialization checks (2019-08-05) Checks introduced for the Default_Initial_Condition of a private type on default initialization of a variable are now reported on the variable which is default initialized rather than on the Default_Initial_Condition aspect. Note that this only matters for types which a Default_Initial_Condition which does not mention the current type instance as otherwise the checks are done on the private type declaration. NF-S730-045 Check DIC only referring to discriminants at use (2019-08-08) If Default_Initial_Condition of a private type only refers to the current type instance through its discriminants, GNATprove now checks it when an object of this type is declared, as opposed to checking it when the type itself is declared. It allows using a Default_Initial_Condition aspect to specify constraints on visible discriminants which are required for a default initialization to be safe. NF-S725-044 More precise data dependencies for protected objects (2019-08-29) GNATprove now more precisely tracks data dependencies for protected objects that are components of an array or a record. Previously, writing to one such object was considered as writing to the entire array or record; now it is considered as writing to precisely the component designated by the prefix of a call to a protected subprogram. NF-S724-033 Switch --info displays info on contextual analysis (2019-07-29) Switch --info used to display information about subprograms that are not contextually analyzed despite being local subprograms without contracts, hence candidates for contextual analysis. In addition, it now displays also information on subprograms that are contextually analyzed. NF-S722-026 Summary table in log now lists all check messages (2019-07-26) Not all check messages from flow analysis were accounted for in the summary table printed at the top of the log file gnatprove.out. Now all check messages are reflected in this table, so that any unverified (by flow analysis of proof) check appears in the table. New categories Termination and Concurrency have been added. Note that the categories Run-time Checks and Termination may contain checks from both flow analysis and proof. NF-S711-045 Warnings for ineffective statements in ghost code (2019-07-11) GNATprove now emits warnings about ineffective statements in ghost subprograms. Previously such warnings were only emitted for non- ghost subprograms. NF-S711-044 Dead code and unreachable branches detected by proof (2019-07-22) The switch --proof-warnings now triggers detection of dead code after branches in the program (in if-statements, case-statements and loops) where previously only dead code after loops was detected. Unreachable branches in all expressions are also detected where previously this was restricted to expressions inside assertions and contracts. NF-S702-060 Automatic target configuration for GNAT runtimes (2019-07-19) If the runtime used for a project analyzed with SPARK has a target configuration file (this is the case for recent GNAT runtimes), SPARK can use this file automatically to configure the SPARK analysis for the target and runtime. In that case, manual target configuration via the -gnateT switch is not necessary anymore. NF-S527-028 More precise handling of Size and Object_Size (2019-05-29) The value of attributes Size and Object_Size was not precisely known by GNATprove for composite types, which prevented proving some properties involving these attributes. NF-S521-038 Support for of iteration on formal vectors (2019-05-23) It is now possible to use for of iteration on formal vectors. NF-S517-001 New switch --prover=all for SPARK (2019-06-26) The existing switch --prover of SPARK now accepts the special string "all", which is equivalent to the provers cvc4,z3 and alt- ergo for SPARK Pro, and equivalent to alt-ergo for SPARK Discovery. NF-S516-005 Issue warning by proof on inconsistent pragma Assume (2019-05-17) When switch --proof-warnings is used, GNATprove now attempts to detect pragma Assume which are inconsistent (always False) and in consequence introduce a contradiction in their context of use. GNATprove issues a warning when such a case is detected. NF-S504-004 Support for volatile variables against optimization (2019-05-29) SPARK now supports volatile variables whose aim is not to interact with the physical world, but simply to prevent compiler optimizations. Such variables are used for examples to defend against fault injections by duplicating the guards to access a critical section of the code. This is now possible in SPARK when the volatile variable is marked with aspect or pragma No_Caching. See the complete description of this aspect in SPARK RM 7.1.2. NF-S423-033 Initial support for owning access types in SPARK (2019-05-13) GNATprove now supports access types provided they abide by single ownership rules (as explained in SPARK RM 3.10). With respect to the rules presented in the RM, the initial support in GNATprove imposes some restrictions. In particular, local borrowers as well as traversal functions are currently unsupported. Additionally, non-aliasing rules on subprogram parameters of an access type are not yet completely enforced by flow analysis and proof does not attempt yet to verify absence of memory leaks. However, programs using access types, and even recursive data structures such as lists and trees, can already be verified successfully for absence of runtime errors (for example, null pointer dereferences) and functional correctness. NF-S423-007 Support the Enum_Rep attribute (2019-05-21) The Enum_Rep attribute, used to access the representation of an enumeration literal, is now supported by the GNATprove tool. NF-S419-010 Improved floating-point support in Alt-Ergo prover (2019-07-10) The Alt-Ergo prover that is shipped with SPARK has been updated. It now includes improved support for reasoning about computations that involve floating point numbers. This enhancement may result in less unproved checks. To benefit from the enhancement, a level higher than 0 should be selected via the --level switch, or the alt-ergo prover should be selected explicitly by including it in the provers provided via the --prover switch. NF-S416-010 Trivial assertions are tagged with Trivial prover (2019-05-21) This changes provers used to prove checks. Each SPARK check is split in several goals. Previously, trivial goals were proved by the first prover used. Now, the trivial goals are reported as proven with "Trivial" prover. NF-S402-002 Subprograms are analyzed in parallel (2019-07-30) Subprograms in the same unit are now analyzed in parallel. This can lead to speedups especially in the case of few large units with many subprograms. NF-S326-003 Suppress warnings about assignments to dummy objects (2019-03-29) GNATprove no longer emits warnings about statements having no effect for assignments to objects whose name contains one of the substrings DISCARD, DUMMY, IGNORE, JUNK, UNUSED in any casing. Similar warnings were already suppressed when compiling the code with GNAT; now they are also suppressed when analyzing the code with GNATprove. NF-S322-052 Display counterexample values for Loop_Entry (2019-05-31) GNATprove now displays values for objects with the Loop_Entry attribute when they are mentioned in the check. NF-S314-023 Exit gracefully when no memory available (2019-03-25) Previously, SPARK would crash with a bugbox in many out-of-memory situations. We have improved SPARK now to report such situations as a regular error message to the user. NF-S308-019 Better tracking of slice bounds in loop invariants (2019-03-08) GNATprove now tracks the bounds of slices used inside loop invariants better, resulting in more proofs on code with slices in loop invariants. NF-S307-007 Faster execution on repeated runs of gnatprove (2019-05-17) When gnatprove is rerun with command-line options that are different, but this difference does not affect generation of the Global contracts (for example, with --pedantic), then the already- generated contracts are reused, and thus the overall tool performance is improved. NF-S222-009 New messages for verified Global and Depends aspects (2019-03-12) GNATprove now emits info messages "data dependencies proved" and "flow dependencies proved" respectively for every Global and Depends contract that has been verified. Also, the "Data Dependencies" and "Flow Dependencies" in the summary table produced in gnatprove.out file contain the total number of verified Global and Depends contracts, respectively. NF-S220-013 Annotation Terminating as package declaration aspect (2019-03-04) Annotation Terminating is now supported in aspect form on package declarations, which means it applies to all subprogram declarations in the package. NF-S206-030 Add contracts to Ada.Strings child packages (2019-04-29) SPARK no longer raises warnings about missing global contracts when using subprograms from Ada.Strings.Fixed, Ada.Strings.Bounded, and Ada.Strings.Unbounded. SPARK now generates new VCs for preconditions on these subprograms. NF-S129-011 Improved explanations for unproved checks in post (2019-01-30) Checks in postconditions (including the postcondition check itself) are now better handled by pointing to a possible explanation inside the body of a subprogram. Explanations about missing preconditions are also better located on the spec of the subprogram. NF-S123-014 Better explanations on unproved preconditions (2019-01-24) When a precondition check is not proved, the explanation part of the message pinpointing possible missing contracts is now more precisely pointing at variables involved in the precondition expression. Also, the mechanism has been extended for preconditions of procedure calls. NF-S122-027 Definite formal vectors are no longer limited (2019-01-28) The formal container API provides two versions of vectors, one for definite elements, and one that can hold indefinite elements. Both formerly supported unbounded vectors that were limited. Formal definite vectors are now bounded, so the type no longer needs to be declared limited. NF-S118-010 Decrease occurrences of spurious counterexamples (2019-01-22) Counterexamples displayed by GNATprove when a check is not proved are best efforts by the underlying provers, which may turn out to be spurious in some cases. This enhancement decreases the number of cases where the counterexample is spurious. NF-S117-042 Suppress no-effect warnings on CASE statements (2019-02-07) Flow analysis previously reported that a CASE statement with just one alternative has no effect. This feature silences the unhelpful warning. NF-S108-006 Add contracts to Ada.Text_IO (2019-02-14) SPARK no longer raises warnings about missing global contracts when using subprograms from Ada.Text_IO. SPARK now generates new VCs for preconditions on these subprograms. NF-RC17-047 Suppress warnings in generic instantiations (2019-01-09) Pragma Warnings Off/On can now be used around generic instances to suppress warnings from the specific instance. NF-RB30-003 Explanations on out parameters for unproved checks (2019-01-14) The explanations for unproved check messages may now point to the discriminants or bounds of unconstrained record/arrays, as these discriminants/bounds are passed as inputs even when the corresponding formal parameters are of mode OUT. NF-RB28-033 Added new lemma for prover (2018-11-30) A new lemma for provers was added which should help proof with Power: lemma Power_pos: forall x y. x > 0 /\ y >= 0 -> power x y > 0. NF-RB09-010 More values for discriminants in counterexamples (2018-11-12) Counterexamples for records now supply a value for discriminants and possibly the 'Constrained attribute in more cases. NF-RB04-002 Suppress warnings about intentionally unused objects (2018-11-04) GNATprove, just like GNAT, now suppresses warnings about unused variables if their name contains any of the substrings DISCARD, DUMMY, IGNORE, JUNK, UNUSED, in any casing. NF-RB01-007 Unused pragma Annotate in dead branch (2018-11-08) Gnatprove does not warn anymore that a pragma Annotate does not justify any failing check, if the pragma Annotate is in a statically dead branch. NF-RA30-034 Gnatprove now defines GPR_TOOL variable (2018-12-03) The GPR_TOOL variable is set by various Adacore tools and can be used to define tool-specific values of variables in the project file. Gnatprove now also sets this variable; it is set to the value "gnatprove". NF-RA23-013 Precise proof of Initial_Condition across units (2018-11-13) When the proof of the Initial_Condition for a unit depends on the Initial_Condition of another with'ed unit being satisfied, GNATprove can now use the condition of the with'ed unit in the proof provided the elaboration of this other unit is "known to precede" (as defined in SPARK RM 7.7(2)) the elaboration of the current unit. NF-RA19-012 Show maximum steps to reproduce full proof (2018-10-29) Gnatprove now records in the gnatprove.out file the maximum number of steps used in a successful proof. This is useful to reproduce a run of gnatprove that fully proved a project. NF-RA18-029 Provability of array length checks on modular (2018-10-22) GNATprove proves more length checks on arrays indexed by modular integer types. NF-RA17-008 More proofs of runtime errors in loop invariants (2018-10-22) Runtime errors that could be raised inside loop invariants are now proved more automatically thanks to the way formulas are generated by GNATprove for such checks. The prover has now access to the loop body information to prove that the loop invariant can be evaluated without runtime errors. NF-RA15-035 Better tracking of inputs of generic packages (2018-10-23) GNATprove now tracks better the value of the actual object used to instantiate the generic formal object of mode in of a generic package. It results in more checks discharged automatically for expressions that reference such a formal object. NF-RA14-002 More precise handling of exit paths in loops (2018-10-17) The effects that occur in exit paths of loops, either through unconditional exit statements or through return statements, are now not considered as effects of the loop. Thus, the provers know that variables that are otherwise not modified in the loop preserve their value across the loop. NF-RA12-018 Better tracking of subtype predicates in loops (2018-10-12) GNATprove is now better at tracking the values of variables modified in a loop. In particular, it is now able to know that the subtype predicate of such a value always holds in the loop when the variable is initialized at declaration or when it has at least one subcomponent with a default expression. NF-RA12-017 Locations of predicate checks on default values (2018-10-12) Checks ensuring that a subtype predicate holds on the default value of a variable with no initialization expression are now located on the variable declaration instead of on the predicate expression. NF-RA04-011 Support attribute Object_Size (2018-10-11) Attribute Object_Size can be used with GNAT to specify or query the default size of objects of a given subtype, unless the Size attribute is specified on the object itself. This was previously supported by querying X'Size for an object X of a subtype S. Now S'Object_Size is also supported. NF-R920-050 No default for size parameter in indefinite vectors (2018-09-26) The default value for the Max_Size_In_Storage_Elements parameter of the Formal_Indefinite_Vector package was using the Max_Size_In_Storage_Elements attribute which is not in SPARK. We have removed this default value to make it clearer that a value should be supplied for this parameter when instantiating formal vectors in SPARK code. NF-R906-030 Better support for recursive functions (2019-07-05) GNATprove now assumes the postcondition of recursive functions annotated with the Terminating pragma in more cases. In particular, it now assumes it for functions called from non- mutually recursive subprograms, and so, even when the function is called from a contract. NF-R807-003 Unproved parts of preconditions identified (2019-02-11) When the precondition of a call is unproved, SPARK can now identify the part of the precondition which was not proved. This feature was already available for other assertion types, but now it also works for preconditions. NF-R703-035 Ability to specify file-specific switches in SPARK (2019-01-11) In the SPARK tools, some commandline switches such as prover timeout, steps and memory limit can now be specified for specific files of the project only. To this end, a new project file attribute Proof_Switches has been introduced. It can be used in this way: package Prove is for Proof_Switches ("file.adb") use ("--timeout=10"); for Proof_Switches ("Ada") use ("--report=all"); end Prove; The existing "Switches" attribute is now deprecated and Proof_Switches should be used. More information about these attributes can be found in the SPARK User's Guide. NF-R511-031 Counterexamples for 'Old variables in contract case (2019-06-06) Variables that are tagged with a 'Old attribute inside a contract case now appear in counterexamples. NF-R329-039 Allow SPARK_Mode Off inside subprograms (2019-01-19) Aspect or pragma SPARK_Mode is now allowed with the value Off inside a subprogram, on a local package or subprogram spec/body. It is particularly useful for instantiating a generic whose body is marked SPARK_Mode Off inside a subprogram. NF-R129-007 Improve messages for wrong Depends contracts (2018-10-10) The messages about a missing self-dependency in a Depends contract are now improved. In particular, for formal parameters of mode Out and for global objects of mode Output that are of an unconstrained array or record types, the improved message explains that the self-dependency comes from preserving the array bounds or record discriminants. NF-R129-006 Simpler messages about uninitialized data (2019-04-11) GNATprove now emits either a check on each access to a possibly uninitialized object, or a single info message on the object's declaration when all accesses happen after the object has been initialized. Previously GNATprove could emit both info messages and checks, which was confusing, especially for arrays and objects accessed from different subprograms. NF-Q612-030 Why3 used by SPARK updated to version 1.2 (2019-03-04) GNATprove now uses the latest version of Why3, namely Why3 1.2. This was a major change, so users may experience various differences in the tool output, in particular in the number of verification conditions per checks, or the time needed to prove a check. Users who are storing session files and using the replay mechanism will probably need to regenerate the sessions. Since there were not backward compatible changes in the input syntax of Why3, the generated Why3 code as well as the generated verification conditions have changed. Advanced users, using for example interactive proof assistants or external axiomatizations, may have to adapt their scripts. Changes in standard theories provided by Why3 and supported version of external solvers are also expected. NF-Q512-018 Add contracts to Ada.Task_Identification (2019-01-25) SPARK generates new VCs for preconditions on subprograms from Ada.Task_Identification. NF-P412-009 Tag counterexamples of previous iteration of loop (2019-05-29) When proving assertions about loops (in particular for loop invariants), the proof tasks used to generate counterexamples often contain references to variables in different steps of a loop. Usually, we can distinguish variables from the current step of the loop and variables from the step of the loop just before this one. The counterexamples values that come from the previous step of the loop are now tagged accordingly.