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