========================== SPARK 21 NEW FEATURES LIST ========================== Copyright (C) 2021, AdaCore and Altran UK Limited This file contains a complete list of new features in version 21 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 21.0w wavefront subsequent to this date will contain the indicated feature, as will any subsequent 21 or later release. NF-TA20-027 Improve tracking of constant parts in loops (2020-10-27) GNATprove can now infer that the bounds or immutable discriminants of the designated value of an access part of an object modified in a loop are preserved if the designated value is assigned as a whole. Users no longer need to use a loop invariant to specify this. NF-TA15-006 Access to bounds and nullity check on borrowed path (2020-10-22) The checker for the ownership rules of SPARK is more permissive. It allows accessing the bounds of an array if one of its component is borrowed. In the same way, it allows checking the nullity of an access object whose content has been borrowed. NF-TA13-005 Support for Enum_Val attribute (2020-10-20) The Enum_Val attribute, which returns the enumeration value whose representation matches a given integer, is now supported by GNATprove. NF-T824-034 Support for 128-bit signed and modular integers (2020-09-08) GNATprove now supports 128-bit integers like GNAT on native platforms, provided either as standard type Long_Long_Long_Integer or as Interfaces.Integer_128 and Interfaces.Unsigned_128, when the Ada 2020 version of the language is selected (either through switch -gnat2020 or with pragma Ada_2020 in the code). NF-T727-032 Possible fix message for function call w/o contract (2020-07-31) When a function without contract (explicit or implicit) is called in an expression submitted to a check (whether it is a run-time check or an assertion), and the check cannot be proved, it is very likely that a postcondition needs to be added to the function, or the function needs to be turned into an expression function. Now GNATprove issues a possible fix message for this case, that works for direct calls, dispatching calls and indirect calls. NF-T722-011 New lemma for multiplication by less than one (2020-09-23) A lemma has been added to the floating point arithmetic lemmas of the SPARK library. It allows to prove that multiplying a positive floating point number by a number between zero and one yields a smaller result. NF-T623-013 Better command-line messages with additional info (2020-07-15) Messages from GNATprove on the command-line are now displayed over multiple line when they give extra information, instead of a single line. A new switch --output has been added, which default to value "pretty" for this multi-line display, and can be set to "brief" to only display the check message without additional information. The multi-line display also shows the corresponding source code for both the main message location and for the locations mentioned in subsequent associated messages. Here is an example of a multi-line message: incr.adb:3:11: medium: overflow check might fail | 3 | X := X + 1; | ^ here e.g. when X = Integer'Last reason for check: result of addition must fit in a 32-bits machine ... possible fix: subprogram at line 1 should mention X in a precondition | 1 |procedure Incr (X : in out Integer) is |^ here . NF-T618-021 Improve diagnostic for nonterminating subprograms (2020-07-15) Flow messages about potentially nonterminating subprograms are now located on the offending loops or calls and the explanation is more precise. NF-T610-004 New functions in SPARK lemma library for floats (2020-09-01) Five new ghost functions have been added in the SPARK lemma library to determine when a floating-point number is representable as an integer (32 or 64 bits) or is an integer at all, and when an integer (32 or 64 bits) is representable as a floating-point number. These can be used in specifications that need to refer to these conversion properties. NF-T609-022 Overflow checks on exponentiation w/ No_Wrap_Around (2020-08-07) On modular types annotated with No_Wrap_Around, GNATprove now checks the absence of overflows on exponentiation. This makes all arithmetic operations on such types checked for possible overflows. NF-T529-016 Improve handling of secondary messages (2020-06-17) In the GNAT Studio integration, improve the display of consecutive messages sharing a location: group them and create duplicated messages to easily navigate to secondary locations. NF-T514-020 Support for access to subprograms (2020-06-11) SPARK now supports declaring objects of an access-to-subprogram type, references to the Access attribute whose prefix is a subprogram name, and calls through dereferences. NF-T511-007 Support for iterated component associations (2020-09-15) In the upcoming version of Ada (Ada 202x), it is possible to use an iterator inside an array aggregate to specify values that depend on the associated index. This is now supported in SPARK for iterated component associations with a discrete choice list. NF-T506-047 Check constants in Global when body is not in SPARK (2020-06-18) GNATprove now emits a check if a constant without variable input appears in a Global or Depends contract of a program unit whose body has not yet been written or is annotated with SPARK_Mode => Off. Previously such a check was only emitted when the body is present and is annotated with SPARK_Mode => On. NF-T504-013 Attribute Update is obsolete (2020-07-23) SPARK-specific attribute Update is obsolete following the introduction of delta aggregates to the draft Ada 202x standard. A warning is now emitted when -gnatj is specified. NF-T501-004 Lemma Library available through GNAT Studio Help (2020-05-21) The header files for the SPARK Lemma Library are now available through menu Help-->SPARK-->Lemmas in GNAT Studio. This can be useful to decide whether to include these files as part of a project. NF-T430-026 Precise handling of fixed-point to integer type conv (2020-05-04) While conversions between fixed-points and integers follow in general the rules given in Annex G.2.3 of the Ada RM, which do not require rounding, conversions from fixed-points to integers also obey the rules given in Ada RM 4.6(33) which require rounding to nearest, ties away from zero. GNATprove now implements this more precise handling of fixed-point to integer conversion. NF-T422-013 Support for delta aggregates (2020-04-30) The upcoming Ada standard (Ada 202x) defines delta aggregates, which allow constructing a new composite value from an existing one by changing only the value of some components (like the SPARK- only 'Update attribute). These aggregates are now supported by GNATprove. The use of the equivalent SPARK-only attribute Update is now deprecated. It can be detected using the -gnatwj compilation switch. NF-T412-002 Better messages for illegal uses of Inline_For_Proof (2020-04-15) GNATprove now emits better messages in the case of illegal uses of pragma Annotate (GNATprove, Inline_For_Proof). NF-T408-027 Support for declare expressions (2020-04-21) GNATprove now supports declare expressions, part of the upcoming Ada 202x standard (and documented in AI12-0236). This feature allows including constants inside expressions. NF-T318-014 Support for the Ada 202x unit Big_Reals (2020-03-20) Special support has been introduced in GNATprove for most of the functionality of the Ada 202x Big_Numbers.Big_Reals unit. Conversions from big reals to standard real types as well as the Numerator and Denominator functions are currently omitted. NF-T303-036 Performance improvement for large aggregates (2020-03-12) SPARK Processing of large aggregates with many checks (such as predicate checks or range checks) is now faster. NF-T212-013 Introduce a relaxed data initialization policy (2020-06-03) By default, SPARK enforces a strict initialization policy at subprogram boundaries, where all inputs of a subprogram must be initialized on entry and all outputs must be initialized on exit. It is now possible to use the Relaxed_Initialization aspect to opt out of this initialization policy on a per-object basis. This aspect also has the effect of moving initialization checks from flow analysis to proof (from Bronze to Silver level). It can be used to verify complex initialization patterns (for arrays for example) that could not be verified by flow analysis. NF-T210-005 No warnings on calls to Delete on formal containers (2020-02-10) The Delete procedure on formal containers takes a cursor as a parameter and deletes the element it designates in the container. It also resets the cursor to No_Element. GNATprove used to emit a warning when the value of the cursor was not used after the call. This warning is no longer emitted. NF-T117-040 Warning suppression with a null dependency clause (2020-01-20) GNATprove was emitting a warning for a subprogram call that modifies its actual parameter when the value of the parameter is not used afterwards. Now this warning can be suppressed by adding an explicit Depends contract with a null dependency clause for the corresponding formal parameter. In particular, this suppression automatically applies to instances of Ada.Unchecked_Deallocation that assign the deallocated object with null. NF-T114-018 Improve handling of Default_Initial_Condition (2020-01-20) When the expression of a Default_Initial_Condition aspect does not mention the current type instance (except possibly its discriminants), GNATprove handles it as a precondition and uses it to prove the integrity of the default initialization of variables of the type. NF-T113-004 Detection of possible memory leaks by proof (2020-04-19) When using pointers (access types) in SPARK, GNATprove now detects when a value of access type may be assigned or reach the end of its lifetime while still owning the memory it points to, a.k.a. there is a possible memory leak at this point. GNATprove issues a check message when it cannot prove the absence of memory leak in such a case. NF-T107-022 Synthesis of a missing Default_Initial_Condition (2020-01-10) If a private type declaration has no Default_Initial_Condition aspect, but the corresponding full view defines default initialization, then GNATprove will now synthesize the missing aspect. This is especially useful when migrating an existing, unannotated code from Ada to SPARK. NF-SC16-099 Better flow diagnostics for volatile functions (2020-02-11) Before, volatile effects within nonvolatile functions were reported as a global effect, against the declaration of the function. Gnatprove now reports which variables within the function body are volatile, helping debugging. This includes use of volatile variables, and variables which are constituents of abstract external state (which are treated as effectively volatile). NF-SB29-015 Support for raise expressions (2020-03-25) Raise expressions are now supported by GNATprove. As for raise statements, checks are generated to make sure that no exceptions can be raised during execution. As a special case, raise expressions in preconditions are considered to be failures of the precondition, and not run-time errors. NF-SB22-010 Specialized support for Big_Integers library (2020-02-14) SPARK translates entities from Ada.Numerics.Big_Numbers.Big_Integers in a special way so they are usable in proof as mathematical integers. NF-SB22-003 New annotation to detect wrap-around on modular (2020-01-06) A new annotation No_Wrap_Around can be used to specify that the four arithmetic operations + - * / should not lead to wrap-around on a modular type. This annotation can be specified on a new type or a derived type declaration. An overflow check message is emitted by GNATprove if the absence of wrap-around cannot be proved. There is no corresponding check at runtime. NF-SB14-022 New lemma for Count of full array (2019-11-15) A new lemma has been added to the part of the lemma library dealing with counting functions. It gives the value of Count on arrays containing only elements with the expected property. NF-SB12-031 No more axiom guards for expression functions (2019-11-15) GNATprove no longer generates guards to protect against unsoundness of the body of non-recursive expression functions. This may result in faster proofs when the switch --no-axiom-guard is not used. NF-SB07-004 Better handling of equality on references to 'Update (2019-11-25) GNATprove now handles array equality better when it compares an object to a reference to the 'Update attribute whose prefix is a reference to the 'Old or 'Loop_Entry attributes on the same object, like X = X'Old'Update (I -> V). This can lead to faster proofs of assertions involving such operations, as well as faster proofs on properties using these assertions. NF-SA25-033 Variants for termination of recursive subprograms (2020-07-28) GNATprove now supports using aspect Subprogram_Variant to prove the termination of (mutually) recursive subprograms. This is similar to how loops can be proved to terminate using pragma Loop_Variant. NF-SA25-001 SPARK now checks safety of unchecked conversions (2020-03-23) Previously, instances of Ada.Unchecked_Conversions were silently accepted by SPARK, but it was left to users to check their correctness. Now, when processing an instantiation of Ada.Unchecked_Conversions, SPARK checks if the instance can lead to unsoundness, and issues a failing check message if it is the case. NF-SA23-039 Support forward goto statements (2019-12-06) Goto statements are now partially allowed in SPARK. The goto statement must refer to a label that comes after the goto in the subprogram. Other uses of goto are still rejected by SPARK. NF-SA13-005 Add reason for index/overflow/length/range checks (2020-07-01) Some check messages are harder for users to understand due to the combination of SPARK rules and the possible location of the message on the token for the top-level sub-expression (like symbol + for an addition) to which the check is attached. That's in particular the case for index/overflow/length/range. Thus, we add here an explanation in the form of a "reason for check" part of some of the check messages, similar to other explanations whose role is to help in understanding the cause for a message. NF-SA10-030 New SPARK submenus and key shortcuts in GNAT Studio (2019-12-11) Some submenus from the contextual SPARK menu have been added to the main SPARK menu in GNAT Studio, for easier access: "Examine Subprogram", "Prove Subprogram", "Prove Selected Region", and "Prove Line". Default key shortcuts have been added for Prove File/Subprogram/Region/Line using Ctrl+Alt+ where letter is f/s/r/l. NF-SA07-047 Improved support for exponentiation in Alt-Ergo (2019-11-11) The Alt-Ergo prover shipped with SPARK has now better support for exponentiation. This results in more proved checks if the Alt-Ergo prover is used. NF-S919-029 Prove Line/Region menu inside inlined subprograms (2019-10-28) The Prove Line/Region menus in GNAT Studio are now working to prove a single line or a set of lines from a subprogram, even when the subprogram is inlined for proof. This is especially convenient for proofs inside inlined ghost procedures. NF-S919-014 Support for pragma Overflow_Mode in source code (2019-12-12) Pragma Overflow_Mode, typically used to specify unbounded signed integer arithmetic in assertions, is now also supported by GNATprove in code source files (so no longer only within configuration files), but only when appearing as a configuration pragma (before the unit). NF-S918-060 More precise handling of Ada.Unchecked_Deallocation (2020-01-31) GNATprove now takes into account the fact that the argument to a call of an instance of Ada.Unchecked_Deallocation is null after the call. NF-S903-010 Better messages for user-defined operators (2019-10-23) When the SPARK toolset was emitting a message about a user-defined overriding of an operator, it was referring to an internal identifier like "Oeq". Now it refers to the overloaded operator exactly as it appears in the source code, e.g. "=". NF-S818-003 Better warnings for subprograms with no effects (2019-10-24) GNATprove used to emit a warning on each call to a subprogram with no effect, i.e. no formal and no global parameters. Now it only emits one warning, at that subprogram itself (unless the subprogram is explicitly annotated with Global => null or Depends => null, which indicates that the lack of effect is intentional). NF-S818-002 New annotation Might_Not_Return on procedures (2019-12-12) Procedures which may not return for legitimate reasons can now be analyzed safely by marking them with a GNATprove annotation Might_Not_Return (either the pragma or aspect form). It is legitimate for such procedures to call procedures marked No_Return, and callers of such procedures must also be marked Might_Not_Return. In particular, a function cannot call such a procedure. NF-R803-027 Predicates on types partially visible in SPARK (2019-11-05) GNATprove now supports subtype predicates specified on types whose full view is not in SPARK. NF-R101-003 Refine the notion of effective volatility (2020-06-26) The notion of effectively volatile object was overly restricting those objects that could be read without considering a side- effect, both from the program analyzed itself (because property Effective_Reads is False) and from the external word (because property Aync_Writers is False). For example, such objects could only be read from a so-called volatile function (marked with aspect Volatile_Function), among other restrictions. A new notion of objects that are "effectively volatile for reading" has been defined to define better rules governing the use of such objects. For example, a non-volatile function can now read an effectively volatile object which is not "effectively volatile for reading", among other permissions. NF-R101-002 Volatility refinement aspects supported for types (2020-03-17) Previously, the four volatility refinement aspects (Async_Readers, Async_Writers, Effective_Reads, and Effective_Writes) could only be specified for volatile variables and for state abstractions. These aspects can now be specified for volatile types as well, as per the rules described in the SPARK RM. NF-QA12-026 Add menus for transformations and provers (2019-10-28) In manual proof, menus are now available to trigger transformations. Right-clicking on the proof tree triggers the same behavior. NF-Q502-001 Support target name @ in assignments (2020-05-11) The next release of Ada introduces a symbol '@' to stand for the left-hand side of an assignment in its right-hand side. This symbol is now supported in SPARK.