:orphan: SPARK 26 Release Notes ====================== We present here a few highlights of the new features in SPARK 26. You can access the complete list `here `__. .. contents:: :local: Language Extensions ------------------- Multiple Levels of Ghost Code ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ SPARK now offers multiple levels of ghost code. Ghost entities, assertion expressions, and specification pragmas can be associated with named assertion levels. Assertion levels, defined using the `Assertion_Level` pragma can then be enabled or disabled through an `Assertion_Policy` pragma. Two levels of ghost code are predefined: `Runtime` and `Static`. Ghost code marked `Runtime` is always enabled; ghost code marked `Static` is never enabled. Assertion Levels for SPARKlib Containers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The SPARK library introduces several assertion levels that are used in the container libraries. The assertion level `SPARKlib_Defensive`` allows enabling preconditions on container operations. This level is useful in particular if these operations are called from unproved code. The assertion level `SPARKlib_Logic`` is for models of formal containers. It can be enabled in the full runtime. In the light runtime, it is also used for the ghost versions of the big numbers library and functional Containers library. As these libraries require finalization, the assertion level `SPARKlib_Logic`` cannot be enabled in the light runtime. New `Program_Exit` Aspect for Abrupt Program Termination ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ SPARK now offers a new `Program_Exit` aspect for specifying that the subprogram will terminate the whole program abruptly. The boolean expression given with this aspect, if any, shall be true when the program is terminated, which permits reasoning about intended program termination. New `Exit_Cases` for Termination Conditions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ SPARK now offers a new `Exit_Cases` aspect for specifying subprogram termination conditions. A subprogram can terminate by returning normally, by propagating an exception or by abruptly terminating the program. If a subprogram does not always terminate normally, then it can be annotated with an `Exit_Cases` aspect. This aspect allows partitioning the input state into cases and specifying for each case what the expected termination kind is: - `Normal_Return`, the subprogram shall return normally; - `Program_Exit`, the subprogram shall abruptly terminate the program; - `Exception_Raised`, the subprogram shall raise an (unspecified) exception; or - `(Exception_Raised => E)`, the subprogram shall raise the exception `E`. Support for Invalid Values ~~~~~~~~~~~~~~~~~~~~~~~~~~ SPARK now supports invalid values via a new `Potentially_Invalid` aspect. The `Potentially_Invalid` aspect can be used to annotate standalone objects, subprogram parameters, function result, and instances of `Ada.Unchecked_Conversion` to specify that they might have values that do not abide by the constraints of their type. A validity check is introduced whenever such objects are evaluated. The `'Valid` and `'Valid_Scalars` attributes can be used to assess their validity both in the code and in contracts. Support for the `finally` Construct ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ SPARK now supports the `finally`` keyword, a GNAT extension, which makes it possible to have a sequence of statements be executed when another sequence of statements is completed, whether normally or abnormally. User Experience --------------- Success Message After Full Verification ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Previously, when all checks were proved (or annotated), GNATprove exited quietly with no explicit success message. Now, SPARK outputs a success message and prints the number of checks that were proved. Support for Generics when Using `--limit` Switches ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Similar to the `--limit-subp` switch, the switches `--limit-line` and `--limit-region` now also support prefixing the location by a generic instantiation. The same is true for locations specified in a file passed to the `--limit-lines` switch. No Resource-Leak Checks in Nonexecutable Ghost Code ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Taking advantage of the new support for multiple levels of ghost code, GNATprove no longer emits checks for resource leaks inside assertion pragmas, specification aspects, and ghost code that is associated with an assertion level that cannot be enabled at run time. Warning Management via the Command Line ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In addition to the existing warning management capabilities, such as `pragma Warnings` and the `--warnings` switch, GNATProve now supports three switches `-W`, `-A` and `-D`, which allow users to enable warnings, suppress them, and promote them to errors, respectively. This can be done for predefined warning categories, which are identified by names appended to the warnings by default. SARIF Output ~~~~~~~~~~~~ GNATProve now generates a `gnatprove.sarif` file at the same location as the `gnatprove.out` file that contains a summary of the run in SARIF format. Improved Message with the `--info` Switch ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Previously, the `--info` switch could be used to enable a number of additional info messages, mostly related to proof. Now, a small number of these messages have been enabled by default (the messages related to inlining and loop unrolling), and the other info messages have been promoted into warnings that are disabled by default. Being warnings, they can be controlled by the `-A`, `-W` and `-D` switches and `pragma Warnings (Off)`. The `--info` switch remains available to enable these warnings collectively. Revised `--no-global-generation` Switch Behavior ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In previous versions of SPARK, the `--no-global-generation` switch prevented flow analysis from automatically generating Global contracts for subprograms without explicit global contracts. In this version of SPARK, the `--no-global-generation` switch has been modified to emit warnings when non-null Global contracts are generated for a subprogram with no explicit Global contracts. This change improves the stability of the feature, making it usable in more contexts. Improved Documentation of Proof Limitations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The section on proof limitations in the SPARK User's Guide has been extended to include cases where the verification might fail due to the tool imprecision. The GNATprove tool has also been extended to detect more of these cases and to emit warnings when the `--info` switch is used. Incompatible Changes in the SPARK Library ----------------------------------------- Renaming of Insertion Primitives in Formal Vectors ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Similarly to Ada standard containers, the ``Containers.Formal.Vectors`` and ``Containers.Formal.Unbounded_Vectors`` packages of the SPARK library provide versions of the ``Append``, ``Insert``, and ``Prepend`` primitives taking a vector as a new item. These primitives have been renamed ``Append_Vector``, ``Insert_Vector``, and ``Prepend_Vector`` to match what has been done for the standard vector packages of Ada. Simplification of Reference Function in Formal Containers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The mode of the first parameters of the ``Reference`` functions declared in the ``Containers.Formal.Vectors``, ``Containers.Formal.Doubly_Linked_Lists``, ``Containers.Formal.Hashed_Maps``, and ``Containers.Formal.Ordered_Maps`` packages of the SPARK library has been modified to simplify its usage. It is now an aliased parameter of mode IN OUT instead of an access parameter. Similarly, the mode of the first parameters of the ``Reference`` functions declared in the ``Containers.Formal.Unbounded_Vectors``, ``Containers.Formal.Unbounded_Doubly_Linked_Lists``, ``Containers.Formal.Unbounded_Hashed_Maps``, and ``Containers.Formal.Unbounded_Ordered_Maps`` packages of the SPARK library is now a parameter of mode IN instead of an access parameter. Change in Generic Instances for Models of Formal Containers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The actual parameter supplied for equality over elements of functional sequences and maps has been changed in the generic instances introduced for the various models of all formal containers. It is now the user-supplied equality function over keys or elements instead of a non-executable function standing for the logical equality. It makes it possible to enable these ghost models at run time, but it changes the meaning of comparison operators (``"="``, ``"<="``, and ``"<"``) over these models, since they make use of this equality function. This change cannot modify the execution of a SPARK program in any way, as this is non-executable ghost code. However, it might affect the provability of user code if it uses these operators in its contracts. The ghost functions ``Equal``, and ``Equal_Prefix`` on sequences, and ``Equal`` and ``Elements_Equal`` on functional maps are used as a replacement for these operators in the contracts of the container library so as to avoid degrading provability. User code might need to be changed in a similar way. Executable Ghost Code in Containers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is now possible to execute most preconditions in the functional and formal container library. Ghost models in the formal container library are also executable in the full runtime. As a result, enabling all assertions and ghost code, for example using ``-gnata``, now has the result of enabling these preconditions and ghost models as well. It is possible to disable them globally by adding ``pragma Check_Policy (SPARKlib_Defensive => Ignore);`` and ``pragma Check_Policy (SPARKlib_Logic => Ignore);`` to the global configuration switch of the user project.