.. index:: SPARK_Mode; usage

**********************
Identifying SPARK Code
**********************

In general a program can have some parts that are in |SPARK| (and follow all
the rules in the |SPARK| Reference Manual), and some parts that are full
Ada. Pragma or aspect ``SPARK_Mode`` is used to identify which parts are
in |SPARK| (by default programs are in full Ada).

This section contains a simple description of pragma and aspect
``SPARK_Mode``. See :ref:`Pragma_SPARK_Mode` for the complete description.

Note that |GNATprove| only analyzes parts of the code that are identified as
being in |SPARK| using pragma or aspect ``SPARK_Mode``.

Mixing |SPARK| Code and Ada Code
================================

An Ada program unit or other construct is said to be "in |SPARK|"
if it complies with the restrictions required to permit formal verification
given  in the |SPARK| Reference Manual.
Conversely, an Ada program unit or other construct is "not in |SPARK|" if
it does not meet these requirements, and so is not amenable to formal
verification.

Within a single Ada unit, constructs which are "in" and "not in" |SPARK| may be
mixed at a fine level in accordance with the following two general principles:

* |SPARK| code shall only reference |SPARK| declarations, but a |SPARK|
  declaration which requires a completion may have a non-|SPARK| completion.

* |SPARK| code may enclose non-|SPARK| code.

* non-|SPARK| code may enclose |SPARK| code only at library level. A subprogram
  body which is not in |SPARK| cannot contain |SPARK| code.

More specifically, non-|SPARK| completions of |SPARK| declarations are
allowed for subprogram declarations, package declarations, task type
declarations, protected type declarations, private type declarations,
private extension declarations, and deferred constant declarations.
[Strictly speaking, the private part of a package, a task type or a
protected type is considered to be part of its completion for purposes
of the above rules; this is described in more detail below].

When a non-|SPARK| completion is provided for a |SPARK| declaration, the
user has an obligation to ensure that the non-|SPARK| completion is
consistent (with respect to the semantics of |SPARK|) with its |SPARK|
declaration. For example, |SPARK| requires that a function call has no
side effects. If the body of a given function is in |SPARK|, then this
rule is enforced via various language rules; otherwise, it is the
responsibility of the user to ensure that the function body does not
violate this rule. As with other such constructs (notably pragma
Assume), failure to meet this obligation can invalidate any or all
analysis (proofs and/or flow analysis) associated with the |SPARK|
portion of a program. A non-|SPARK| completion meets this obligation if
it is semantically equivalent (with respect to dynamic semantics) to
some notional completion that could have been written in |SPARK|.

When a non-|SPARK| package declaration or body is included in a |SPARK|
subprogram or package, the user has an obligation to ensure that the
non-|SPARK| declaration is consistent (with respect to the semantics of
|SPARK|) with a hypothetical equivalent |SPARK| declaration. For example,
|SPARK| requires that package elaboration code cannot modify variables defined
outside of the package.

The |SPARK| semantics (specifically including flow analysis and
proof) of a "mixed" program which meets the aforementioned
requirement are well defined - they are the semantics of the
equivalent 100% |SPARK| program. For the semantics of other "mixed"
programs refer to the Ada Reference Manual.

In the case of a package, a task type, or a protected type, the
specification/completion division described above is a simplification
of the true situation. For instance, a package is divided into 4
sections, not just 2: its visible part, its private part, the
declarations of its body, and the statement list of its body. For a
given package and any number N in the range 0 .. 4, the first N
sections of the package might be in |SPARK| while the remainder is
not.

For example, the following combinations may be typical:

- Package specification in |SPARK|. Package body not in |SPARK|.

- Visible part of package specification in |SPARK|. Private part and body not
  in |SPARK|.

- Package specification in |SPARK|. Package body almost entirely in |SPARK|,
  with a small number of subprogram bodies not in |SPARK|.

- Package specification in |SPARK|, with all subprogram bodies imported
  from another language.

- Package specification contains a mixture of declarations which are in |SPARK|
  and not in |SPARK|.  The latter declarations are only visible and usable from
  client units which are not in |SPARK|.

Task types and protected types are similar to packages but only have 3
sections instead of 4. The statement list section of the body is
missing.

Another typical use is to exempt part of a subprogram from analysis by
isolating it in a local subprogram whose body is not in |SPARK|.

Such patterns are intended to allow for application of formal verification to a
subset of a program, and the combination of formal verification with more
traditional testing (see :ref:`Applying SPARK in Practice`).

.. index:: project file; and SPARK_Mode

Project File Setup
==================

The project file is used to identify coarsely which parts of a program are in
|SPARK|. To get more details on project file setup, see section :ref:`Setting
Up a Project File`.

Setting the Default SPARK_Mode
------------------------------

There are two possible defaults:

#. No value of ``SPARK_Mode`` is specified as a configuration pragma. In that
   case, only the parts of the program explicitly marked with ``SPARK_Mode =>
   On`` are in |SPARK|. This default is recommended if only a small number of
   units or subprograms are in |SPARK|.

#. A value of ``SPARK_Mode => On`` is specified as a configuration pragma. In
   that case, all the program should be in |SPARK|, except for those parts
   explicitly marked with ``SPARK_Mode => Off`` or a configuration pragma of
   ``Auto`` inside files. This mode is recommended if most of the program is in
   |SPARK|.

Here is how to specify a value of ``SPARK_Mode => On`` as a configuration
pragma:

.. code-block:: gpr

  project My_Project is
     package Compiler is
        for Local_Configuration_Pragmas use "spark.adc";
     end Compiler;
  end My_Project;

where ``spark.adc`` is a configuration file containing at least the following
line:

.. code-block:: ada

  pragma SPARK_Mode (On);

Specifying Files To Analyze
---------------------------

By default, all files from a project are analyzed by |GNATprove|. It may be
useful to restrict the set of files to analyze to speedup analysis if only a
subset of the files contain |SPARK| code.

The set of files to analyze can be identified by specifying a different value
of various project attributes in the mode used for formal verification:

 * ``Source_Dirs``: list of source directory names
 * ``Source_Files``: list of source file names
 * ``Source_List_File``: name of a file listing source file names

For example:

.. code-block:: gpr

  project My_Project is

    Mode := External ("GPR_TOOL", "");

    case Mode is
       when "gnatprove" =>
          for Source_Dirs use ("dir1", "dir2");
          for Source_Files use ("file1.ads", "file2.ads", "file1.adb", "file2.adb");
       when others =>
          for Source_Dirs use (...);
    end case;

    package Compiler is
       case Mode is
          when "gnatprove" =>
             for Switches ("Ada") use ...
          when others =>
             for Switches ("Ada") use ...
       end case;
    end Compiler;

  end My_Project;

Excluding Files From Analysis
-----------------------------

When choosing a default value of ``SPARK_Mode => On``, it may be needed to
exclude some files from analysis (for example, because they contain non-|SPARK|
code, or code that does not need to be formally analyzed).

The set of files to exclude can be identified by specifying a different value
of various project attributes in the mode used for formal verification:

 * ``Excluded_Source_Dirs``: list of excluded source directory names
 * ``Excluded_Source_Files``: list of excluded source file names
 * ``Excluded_Source_List_File``: name of a file listing excluded source file names

For example:

.. code-block:: gpr

  project My_Project is
     package Compiler is
        for Local_Configuration_Pragmas use "spark.adc";
     end Compiler;

    Mode := External ("GPR_TOOL", "");

    case Mode is
       when "gnatprove" =>
          for Excluded_Source_Files use ("file1.ads", "file1.adb", "file2.adb");
       when others =>
          null;
    end case;

  end My_Project;

Using Multiple Projects
-----------------------

Sometimes, it is more convenient to analyze a subset of the source files with
the default ``SPARK_Mode => On`` and the rest of the source files with no
setting for ``SPARK_Mode``. In that case, one can use two project files with
different defaults, with each source file in one of the projects only. Files in
one project can still refer to files in the other project by using a ``limited
with`` clause between projects, as follows:

.. code-block:: gpr

  limited with "project_b"
  project My_Project_A is
     package Compiler is
        for Local_Configuration_Pragmas use "spark.adc";
     end Compiler;
     for Source_Files use ("file1.ads", "file2.ads", "file1.adb", "file2.adb");
  end My_Project_A;

.. code-block:: gpr

  limited with "project_a"
  project My_Project_B is
     for Source_Files use ("file3.ads", "file4.ads", "file3.adb", "file4.adb");
  end My_Project_B;

where ``spark.adc`` is a configuration file containing at least the following
line:

.. code-block:: ada

  pragma SPARK_Mode (On);

.. _Using SPARK_Mode in Code:

Using ``SPARK_Mode`` in Code
============================

The pragma or aspect ``SPARK_Mode`` can be used in the code to identify
precisely which parts of a program are in |SPARK|.

Basic Usage
-----------

The form of a pragma SPARK_Mode is as follows:

.. code-block:: ada

   pragma SPARK_Mode [ (Auto | On | Off) ]

For example:

.. code-block:: ada

   pragma SPARK_Mode (On);
   package P is

The value ``Auto`` is only allowed in configuration pragmas, either in a
configuration pragma file, or inside a source file. Thus, value ``Auto`` is not
allowed in aspect ``SPARK_Mode``. Having a value ``Auto`` means that the
file is analyzed as if no value of ``SPARK_Mode`` was specified, which is
useful in cases where ``SPARK_Mode => On`` is specified in a configuration
pragma file for the complete project, but a file contains both entities
compatible with SPARK and entities not in SPARK.

The form of an aspect SPARK_Mode is as follows:

.. code-block:: ada

   with SPARK_Mode => [ On | Off ]

For example:

.. code-block:: ada

   package P with
     SPARK_Mode => On
   is

A default argument of On is assumed for any SPARK_Mode pragma or
aspect for which no argument is explicitly specified.

For example:

.. code-block:: ada

   package P is
      pragma SPARK_Mode;  --  On is implicit here

or

.. code-block:: ada

   package P with
     SPARK_Mode  --  On is implicit here
   is

We say that a package or a subprogram is library-level if it is either
top-level (i.e. it is a library unit; its declaration is the outermost program
unit declared in a given compilation unit) or declared immediately within
another library-level package (which excludes, for example, declarations inside
subprogram bodies). For example, all the packages in the following code snippet
are library-level packages:

.. code-block:: ada

   package P is
      package Q is
         package R is
   ...
   package body P is
      package S is
         package T is

The ``SPARK_Mode`` pragma can be used in the following places in the code:

* as a configuration pragma at unit level (even before with-clauses) in
  particular for unit-level generic instantiations

* immediately within a library-level package spec

* immediately within a library-level package body

* immediately following the ``private`` keyword of a library-level package spec

* immediately following the ``begin`` keyword of a library-level package body

* immediately following a library-level subprogram spec

* immediately within a library-level subprogram body

* immediately within a library-level task spec

* immediately within a library-level task body

* immediately following the ``private`` keyword of a library-level task spec

* immediately within a library-level protected spec

* immediately within a library-level protected body

* immediately following the ``private`` keyword of a library-level
  protected spec

The ``SPARK_Mode`` aspect can be used in the following places in the code:

* on a library-level package spec or body

* on a library-level subprogram spec or body

* on a library-level task spec or body

* on a library-level protected spec or body

If a ``SPARK_Mode`` pragma or aspect is not specified for a
subprogram, package, task or protected spec/body, then its
value is inherited from the current mode that is active at the point
where the declaration occurs.

Note that a generic package instance is considered to be declared
at its instantiation point. For example, a generic package
cannot be both marked ``SPARK_Mode`` and instantiated in
a subprogram body.

Consistency Rules
-----------------

The basic rule is that you cannot turn ``SPARK_Mode`` back On, once you have
explicitly turned if Off. So the following rules apply:

If a subprogram spec has ``SPARK_Mode`` Off, then the body cannot have
``SPARK_Mode`` On.

For a package, we have four parts:

#. the package public declarations
#. the package private part
#. the body of the package
#. the elaboration code after ``begin``

For a package, the rule is that if you explicitly turn ``SPARK_Mode`` Off for
any part, then all the following parts cannot have ``SPARK_Mode`` On. Note that
this may require repeating a pragma ``SPARK_Mode (Off)`` in the body. For
example, if we have a configuration pragma ``SPARK_Mode (On)`` that turns the
mode On by default everywhere, and one particular package spec has pragma
``SPARK_Mode (Off)``, then that pragma will need to be repeated in the package
body.

Task types and protected types are handled similarly. If ``SPARK_Mode`` is set
to Off on one part, it cannot be set to On on the following parts, among the
three parts:

#. the spec
#. the private part
#. the body

There is an exception to this rule, when ``SPARK_Mode`` occurs in the code of a
generic instantiated in code where ``SPARK_Mode`` is Off. In that case,
occurrences of ``SPARK_Mode`` in the generic are ignored for this instance.

Examples of Use
---------------

Verifying Selected Subprograms
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If only a few selected subprograms are in |SPARK|, then it makes sense to set no
default for ``SPARK_Mode``, and instead set ``SPARK_Mode => On`` directly on
the subprograms of interest. For example:

.. literalinclude:: /examples/ug__selected_subprograms/selected_subprograms.ads
   :language: ada
   :linenos:

Note that, although the bodies of procedures ``Sub_Action`` and
``Non_Critical_Action`` are not analyzed, it is valid to call ``Sub_Action`` in
the body of procedure ``Critical_Action``, even without specifying ``SPARK_Mode
=> On`` on the spec of ``Sub_Action``. Indeed, |GNATprove| checks in that case
that the spec of ``Sub_Action`` is in |SPARK|.

.. literalinclude:: /examples/ug__selected_subprograms/selected_subprograms.adb
   :language: ada
   :linenos:

Verifying Selected Units
^^^^^^^^^^^^^^^^^^^^^^^^

If only a few selected units are in |SPARK|, then it makes sense to set no
default for ``SPARK_Mode``, and instead set ``SPARK_Mode => On`` directly on
the units of interest. For example:

.. literalinclude:: /examples/ug__selected_units/selected_units.ads
   :language: ada
   :linenos:

Note that procedure ``Sub_Action`` can be called inside |SPARK| code, because
its spec is in |SPARK|, even though its body is marked ``SPARK_Mode =>
Off``. On the contrary, procedure ``Non_Critical_Action`` whose spec is marked
``SPARK_Mode => Off`` cannot be called inside |SPARK| code.

.. literalinclude:: /examples/ug__selected_units/selected_units.adb
   :language: ada
   :linenos:

Excluding Selected Unit Bodies
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If a unit spec is in |SPARK|, but its body is not in |SPARK|, the spec can be
marked with ``SPARK_Mode => On`` and the body with ``SPARK_Mode => Off``. This
allows client code in |SPARK| to use this unit. If ``SPARK_Mode`` is On by
default, then it need not be repeated on the unit spec.

.. literalinclude:: /examples/ug__exclude_unit_body/exclude_unit_body.adb
   :language: ada
   :linenos:

Note that the private part of the spec (which is physically in the spec file,
but is logically part of the implementation) can be excluded as well, by using
a pragma ``SPARK_Mode (Off)`` at the start of the private part.

.. literalinclude:: /examples/ug__exclude_unit_body/exclude_unit_body.ads
   :language: ada
   :linenos:

This scheme also works on generic units, which can then be instantiated both in
code where ``SPARK_Mode`` is On, in which case only the body of the
instantiated generic is excluded, or in code where ``SPARK_Mode`` is Off, in
which case both the spec and the body of the instantiated generic are excluded.

.. literalinclude:: /examples/ug__use_generic/exclude_generic_unit_body.ads
   :language: ada
   :linenos:

.. literalinclude:: /examples/ug__use_generic/exclude_generic_unit_body.adb
   :language: ada
   :linenos:

.. literalinclude:: /examples/ug__use_generic/use_generic.ads
   :language: ada
   :linenos:

.. literalinclude:: /examples/ug__use_generic/use_generic.adb
   :language: ada
   :linenos:

Excluding Selected Parts of a Unit
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

If most units are in |SPARK| except from some subprograms and packages, it
makes sense to set the default to ``SPARK_Mode (On)``, and set ``SPARK_Mode =>
Off`` on non-|SPARK| declarations. We assume here that a value of ``SPARK_Mode
=> On`` is specified as a configuration pragma.

.. literalinclude:: /examples/ug__exclude_selected_parts/exclude_selected_parts.ads
   :language: ada
   :linenos:

Note that procedure ``Non_Critical_Action`` can be called inside |SPARK| code,
because its spec is in |SPARK|, even though its body is marked ``SPARK_Mode =>
Off``.

Note also that the local package ``Non_Critical_Data`` can contain any
non-|SPARK| types, variables and subprograms, as it is marked ``SPARK_Mode =>
Off``. It may be convenient to define such a local package to gather
non-|SPARK| declarations, which allows to mark globally the unit
``Exclude_Selected_Parts`` with ``SPARK_Mode => On``.

.. literalinclude:: /examples/ug__exclude_selected_parts/exclude_selected_parts.adb
   :language: ada
   :linenos:
