7.3. How to Use GNATprove in a Team
The most common use of GNATprove is as part of a regular quality control or quality assurance activity inside a team. Usually, GNATprove is run every night on the current codebase, and during the day by developers either on their computer or on servers. For both nightly and daily runs, GNATprove results need to be shared between team members, either for viewing results or to compare new results with the shared results. These various processes are supported by specific ways to run GNATprove and share its results.
In all cases, the source code should not be shared directly (say, on a shared drive) between developers, as this is bound to cause problems with file access rights and concurrent accesses. Rather, the typical usage is for each user to do a check out of the sources/environment, and use therefore her own version/copy of sources and project files, instead of physically sharing sources across all users.
The project file should also always specify a local, non shared, user writable directory as object directory (whether explicitly or implicitly, as the absence of an explicit object directory means the project file directory is used as object directory).
7.3.1. Possible Workflows
Multiple workflows allow to use GNATprove in a team:
GNATprove is run on a server or locally, and no warnings or check messages should be issued. Typically this is achieved by suppressing spurious warnings and justifying unproved check messages.
GNATprove is run on a server or locally, and textual results are shared in Configuration Management.
GNATprove is run on a server, and textual results are sent to a third-party qualimetry tool (like GNATdashboard, SonarQube, SQUORE, etc.)
GNATprove is run on a server or locally, and the GNATprove session files are shared in Configuration Management.
In all workflows (but critically for the first workflow), messages can be suppressed or justified. Indeed, like every sound and complete verification tool, GNATprove may issue false alarms. A first step is to identify the type of message:
warnings can be suppressed, see Suppressing Warnings
check messages can be justified, see Justifying Check Messages
Check messages from proof may also correspond to provable checks, which require interacting with GNATprove to find the correct contracts and/or analysis switches, see How to Investigate Unproved Checks.
The textual output in workflow 3 corresponds to the compiler-like output
generated by GNATprove and controlled with switches --report
and
--warnings
(see Running GNATprove from the Command Line). By default
messages are issued only for unproved checks and warnings.
The textual output in workflow 2 comprises this compiler-like output, and
possibly additional output generated by GNATprove in file gnatprove.out
(see Effect of Mode on Output and Managing Assumptions).
Workflow 4 is explained in more detail in Sharing Proof Results with Others.
7.3.2. Suppressing Warnings
GNATprove warnings are controlled with switch --warnings
:
--warnings=off
suppresses all warnings--warnings=error
treats warnings as errors--warnings=continue
issues warnings but does not stop analysis (default)
The default is that GNATprove issues warnings but does not stop.
Warnings can be suppressed selectively by the use of pragma
Warnings
in the source code. For example, GNATprove issues three warnings
on procedure Warn
, which are suppressed by the three pragma Warnings
in
the source code:
1pragma Warnings (Off, "unused initial value of ""X""",
2 Reason => "Parameter mode is mandated by API");
3
4procedure Warn (X : in out Integer) with
5 SPARK_Mode
6is
7 pragma Warnings (Off, "initialization has no effect",
8 Reason => "Coding standard requires initialization");
9 Y : Integer := 0;
10 pragma Warnings (On, "initialization has no effect");
11
12begin
13 pragma Warnings (Off, "unused assignment",
14 Reason => "Test program requires double assignment");
15 X := Y;
16 pragma Warnings (On, "unused assignment");
17 X := Y;
18end Warn;
Warnings with the specified message are suppressed in the region starting at
pragma Warnings Off
and ending at the matching pragma Warnings On
or at
the end of the file (pragma Warnings
is purely textual, so its effect does
not stop at the end of the enclosing scope). The Reason
argument string is
optional. A regular expression can be given instead of a specific message in
order to suppress all warnings of a given form. Pragma Warnings Off
can be
added in a configuration file to suppress the corresponding warnings across all
units in the project. Pragma Warnings Off
can be specified for an entity to
suppress all warnings related to this entity.
Additionally, aspect Warnings Off
on a static stand-alone constant object
can be used to suppress warnings about unreachable code due to a “statically
disabled” condition of an IF statement. This is useful when using configuration
constants, which may trigger spurious warnings about unreachable code.
A “statically disabled” condition which evaluates to Value is either:
a static stand-alone constant when it is of a boolean type, has aspect
Warnings Off
and its initial value evaluates to Valuea relational_operator where one operand is static stand-alone constant with aspect
Warnings Off
, the other operand is a literal of the corresponding type and the operator evaluates to Valuean
and
orand then
operators when:Value is True and both operands are statically disabled conditions that evaluate to True
Value is False and at least one operand is a statically disabled condition that evaluates to False
an
or
oror else
operators when:Value is True and at least one operand is a statically disabled condition that evaluates to True
Value is False and both operands are statically disabled conditions that evaluate to False
a not operator when the right operand is a statically disabled condition that evaluates to the negation of Value
Pragma Warnings
can also take a first argument of GNATprove
to specify
that it applies only to GNATprove. For example, the previous example can be
modified to use these refined pragma Warnings
:
1pragma Warnings (GNATprove, Off, "unused initial value of ""X""",
2 Reason => "Parameter mode is mandated by API");
3
4procedure Warn2 (X : in out Integer) with
5 SPARK_Mode
6is
7 pragma Warnings (GNATprove, Off, "initialization has no effect",
8 Reason => "Coding standard requires initialization");
9 Y : Integer := 0;
10 pragma Warnings (GNATprove, On, "initialization has no effect");
11
12begin
13 pragma Warnings (GNATprove, Off, "unused assignment",
14 Reason => "Test program requires double assignment");
15 X := Y;
16 pragma Warnings (GNATprove, On, "unused assignment");
17 X := Y;
18end Warn2;
Besides the documentation benefit of using this refined version of pragma
Warnings
, it makes it possible to exclude such pragma Warnings
from the
detection of useless pragma Warnings
, that do not suppress any warning at
compilation, with compilation switch -gnatw.w
. Indeed, this switch can then
be used during compilation with GNAT, as pragma Warnings
that apply only to
GNATprove can be identified as such.
See the GNAT Reference Manual for more details.
Additionally, GNATprove can issue warnings as part of proof, on preconditions
or postconditions or pragma Assume
that are always false, unreachable
branches in complex Boolean expressions (typically in assertions and
contracts), dead code at branching points in the program. These warnings are
not enabled by default, as they require calling a prover for each potential
warning, which incurs a small cost (1 sec for each property thus checked). They
can be enabled with switch --proof-warnings=on
, and their effect is controlled
by switch --warnings
and pragma Warnings
as described previously.
There are two benefits of activating these warnings:
they may detect unintentional unreachable or useless code and assertions, which may originate from errors in either code or assertions;
they strengthen confidence in the tool output, acting as a smoke detector for cases where the tool would get into an inconsistent context by error, and report some unreachable code or branch where there is none.
Note that GNATprove, just like GNAT, suppresses warnings about unused variables if their name contains any of the substrings DISCARD, DUMMY, IGNORE, JUNK, UNUSED, in any casing.
7.3.3. Suppressing Information Messages
Information messages can be suppressed by the use of pragma Warnings
in the
source code, like for warnings.
7.3.4. Justifying Check Messages
GNATprove’s analysis relies on the fact that, at any given point in the program, previous checks on any execution reaching that program point have been successful. Thus, given two successive assertions of the same property:
pragma Assert (Prop); -- possibly not proved
pragma Assert (Prop); -- proved
The second assertion will be reported as proved by GNATprove, even if the first assertion is reported as not proved. This is because any execution that fails the first assertion is not analyzed further by GNATprove.
Similarly, consider two successive calls to the same procedure with a precondition:
Proc (Args); -- precondition possibly not proved
Proc (Args); -- precondition proved
The precondition of the second call will be reported as proved by GNATprove, even if the precondition of the first call is reported as not proved. This is because any execution that fails the first precondition is not analyzed further by GNATprove.
This applies to all proof checks, and to a lesser extent to flow analysis checks. For example, outputs of a subprogram are considered fully initialtized in a caller, as explained in Data Initialization Policy. In particular, such outputs are considered to have values that respect the constraints of their type, which is used during proof.
Thus, the user should be careful when justifying check messages, as the incorrect justification of a check message that could fail could also hide other possible failures later for the same execution of the analyzed program.
7.3.4.1. Direct Justification with Pragma Annotate
Check messages generated by GNATprove’s flow analysis or proof can be
selectively justified by adding a pragma Annotate
in the source code. For
example, the check message about a possible division by zero in the return
expression below can be justified as follows:
return (X + Y) / (X - Y);
pragma Annotate (GNATprove, False_Positive,
"divide by zero", "reviewed by John Smith");
The pragma has the following form:
pragma Annotate (GNATprove, Category, Pattern, Reason);
where the following table explains the different entries:
Item |
Explanation |
---|---|
GNATprove |
is a fixed identifier |
Category |
is one of |
Pattern |
is a string literal describing the pattern of the check messages which shall be justified |
Reason |
is a string literal providing a justification for reviews |
All arguments should be provided.
The Category currently has no impact on the behavior of the tool but serves a documentation purpose:
False_Positive
indicates that the check cannot fail, although GNATprove was unable to prove it.Intentional
indicates that the check can fail but that it is not considered to be a bug.
Pattern is a pattern that is used to match against the text of the check
message to justify (not including the initial "low: "
, "medium: "
or
"high: "
prefix). The pattern follows the same rules as for pragma
Warnings
. It may contain asterisks, which match zero or more characters in
the message, and no other characters are interpreted as regular expression
notations (it is not necessary to put an asterisk at the start and the end of
the message, since this is implied). The match is case insensitive.
Reason is a string provided by the user as a justification for reviews. This reason may be present in a GNATprove report.
Placement rules are as follows: in a statement list or declaration list, pragma
Annotate
applies to the preceding item in the list, ignoring other pragma
Annotate
. If there is no preceding item, the pragma applies to the
enclosing construct. For example, if the pragma is the first element of the
then-branch of an if-statement, it will apply to condition in the
if-statement.
If the preceding or enclosing construct is a subprogram body, the pragma applies to both the subprogram body and the spec including its contract. This allows to place a justification for a check message issued by GNATprove either on the spec when it is relevant for callers. Note that this placement of a justification is ineffective on subprograms analyzed only in the context of their calls (see details in Contextual Analysis of Subprograms Without Contracts).
An aspect on a package or subprogram declaration/body can be used instead of a pragma at the beginning of the corresponding declaration list inside the declaration/body:
package Pack with
Annotate => (GNATprove, False_Positive,
"divide by zero", "reviewed by John Smith")
is
...
procedure Proc with
Annotate => (GNATprove, False_Positive,
"divide by zero", "reviewed by John Smith")
is
...
As a point of caution, the following placements of pragma Annotate will apply the pragma to a possibly large range of source lines:
when the pragma appears in a statement list after a block, it will apply to the entire block (e.g. an if statement including all branches, or a loop including the loop body).
when the pragma appears directly after a subprogram body, it will apply to the entire body and the spec of the subprogram.
Users should take care to not justify checks which were not intended to be justified, when placing pragma Annotate in such places.
procedure Do_Something_1 (X, Y : in out Integer) with
Depends => ((X, Y) => (X, Y));
pragma Annotate (GNATprove, Intentional, "incorrect dependency ""Y => X""",
"Dependency is kept for compatibility reasons");
or on the body when it is an implementation choice that need not be visible to users of the unit:
procedure Do_Something_2 (X, Y : in out Integer) with
Depends => ((X, Y) => (X, Y));
procedure Do_Something_2 (X, Y : in out Integer) is
begin
X := X + Y;
Y := Y + 1;
end Do_Something_2;
pragma Annotate (GNATprove, Intentional, "incorrect dependency ""Y => X""",
"Currently Y does not depend on X, but may change later");
Pragmas Annotate
of the form above that do not justify any check message
are useless and result in a warning by GNATprove. Like other warnings emitted
by GNATprove, this warning is treated like an error if the switch
--warnings=error
is set.
7.3.4.2. Indirect Justification with Pragma Assume
Check messages generated by GNATprove’s proof can alternatively be justified indirectly by adding a Pragma Assume in the source code, which allows the check to be proved. For example, the check message about a possible integer overflow in the assignment statement below can be justified as follows:
procedure Next_Tick is
begin
pragma Assume (Clock_Ticks < Natural'Last,
"Device uptime is short enough that Clock_Ticks is less than 1_000 always");
Clock_Ticks := Clock_Ticks + 1;
end Next_Tick;
Using pragma Assume
is more powerful than using pragma Annotate
, as the
property assumed may be used to prove more than one check. Thus, one should in
general use pragma Annotate
rather than pragma Assume
to justify simple
runtime checks. There are some cases though where using a pragma Assume
may
be preferred. In particular:
To keep assumptions local:
pragma Assume (<External_Call's precondition>, "because for these internal reasons I know it holds"); External_Call;
If the precondition of
External_Call
changes, it may not be valid anymore to assume it here, though the assumption will stay True for the same reasons it used to be. Incompatible changes in the precondition ofExternal_Call
will lead to a failure in the proof of External_Call’s precondition.To sum up what is expected from the outside world so that it can be reviewed easily:
External_Find (A, E, X); pragma Assume (X = 0 or (X in A'Range and A (X) = E), "because of the documentation of External_Find");
Maintenance and review is easier with a single pragma
Assume
than if it is spread out into various pragmasAnnotate
. If the information is required at several places, the pragmaAssume
can be factorized into a procedure:function External_Find_Assumption (A : Array, E : Element, X : Index) return Boolean is (X = 0 or (X in A'Range and A (X) = E)) with Ghost; procedure Assume_External_Find_Assumption (A : Array, E : Element, X : Index) with Ghost, Post => External_Find_Assumption (A, E, X) is pragma Assume (External_Find_Assumption (A, E, X), "because of the documentation of External_Find"); end Assume_External_Find_Assumption; External_Find (A, E, X); Assume_External_Find_Assumption (A, E, X);
In general, assumptions should be kept as small as possible (only assume what
is needed for the code to work). Indirect justifications with pragma
Assume
should be carefully inspected as they can easily introduce errors
in the verification process.
7.3.7. Managing Assumptions
Because GNATprove analyzes separately subprograms and packages, its results depend on assumptions about other subprograms and packages. For example, the verification that a subprogram is free from run-time errors depends on the property that all the subprograms it calls implement their specified contract. If a program is completely analyzed with GNATprove, GNATprove will report messages on those other subprograms, if they might not implement their contract correctly. But in general, a program is partly in SPARK and partly in other languages, mostly Ada, C and assembly languages. Thus, assumptions on parts of the program that cannot be analyzed with GNATprove need to be recorded for verification by other means, like testing, manual analysis or reviews.
7.3.7.1. Partial Listing of Detailed Assumptions
When switch --assumptions
is used, GNATprove generates information about
remaining assumptions in its result file gnatprove.out
. These remaining
assumptions need to be justified to ensure that the desired verification
objectives are met. An assumption on a subprogram may be generated in various
cases:
the subprogram was not analyzed (for example because it is marked
SPARK_Mode => Off
)the subprogram was not completely verified by GNATprove (that is, some unproved checks remain)
Note that currently, only assumptions on called subprograms are output, and not assumptions on calling subprograms.
The following table explains the meaning of assumptions and claims which gnatprove may output:
Assumption |
Explanation |
---|---|
effects on parameters and global variables |
The subprogram does not read or write any other parameters or global variables than what is described in its spec (signature + data dependencies). |
absence of run-time errors |
The subprogram is free from run-time errors. |
the postcondition |
The postconditon of the subprogram holds after each call of the subprogram. |
7.3.7.2. Complete List of Assumptions
For the sake of these assumptions, we define a precisely supported address specification to be an address clause or aspect whose expression is a reference to the Address attribute on a part of a standalone object or constant. We define an imprecisely supported address specification to be an address clause or aspect that is not a precisely supported address specification.
For the sake of these assumptions, we define an object with an imprecisely supported address to be either a stand-alone object with an address clause or aspect that is an imprecisely supported address specification or an object that is a reachable part of an object with an imprecisely supported address (a component of a composite value or the designated object of an access value).
The following assumptions need to be addressed when using SPARK on all or part of a program:
[SPARK_JUSTIFICATION] All justifications of check messages should be reviewed (see Justifying Check Messages), both when using Direct Justification with Pragma Annotate and when using Indirect Justification with Pragma Assume.
[SPARK_EXTERNAL] The modeling of Interfaces to the Physical World needs to be reviewed for objects whose value may be modified concurrently.
They should be effectively volatile in SPARK (see SPARK RM 7.1.2), so that GNATprove takes into account possible concurrent changes in the object’s value. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is required.
They should be synchronized in SPARK (see SPARK RM 9) to prevent race conditions which could lead to reading invalid values. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is required.
They should have specified all necessary Properties of Volatile Variables corresponding to their usage. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is required.
[SPARK_ALIASING_ADDRESS] Aliases between objects with an imprecisely supported address specification are ignored by GNATprove. Reviews are necessary to ensure that:
The objects themselves are annotated with the
Asynchronous_Writers
volatile property if they can be affected by the modification of another object. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is required.Other objects visible from SPARK code which might be affected by a modification of such a variable have the
Asynchronous_Writers
volatile property set to True. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is needed.Other objects visible from SPARK code which might be affected by a modification of such a variable have valid values for their type when read. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is needed.
[SPARK_VALID] Attribute ‘Valid is currently assumed to always return True, as no invalid value can be constructed in SPARK (see Data Validity). If assumptions [SPARK_ALIASING_ADDRESS], [SPARK_EXTERNAL_VALID], and [ADA_EXTERNAL] are satisfied, then this assumption will be satisfied as well. However, it is valuable to explicitly state this assumption because it highlights an important consequence of compliance with the other assumptions.
[SPARK_EXTERNAL_VALID] Values read from objects whose address is specified are assumed to be valid values. This assumption is limited to objects with an imprecisely supported address (because an explicit check is emitted otherwise). Currently there is no model of invalidity or undefinedness. The onus is on the user to ensure that all values read from an external source are valid. The use of an invalid value invalidates any proofs associated with the value. The warning imprecisely supported address specification is guaranteed to be issued in cases where review is required.
[SPARK_STORAGE_ERROR] As explained in section Dealing with Storage_Error, GNATprove does not issue messages about possible memory exhaustion, which leads to raising exception
Storage_Error
at runtime. The computation of suitable stack and heap sizes should be performed independently.[SPARK_TARGET_AND_RUNTIME] When the target configuration and runtime library for running the program are different from those on the host when GNATprove is run, the target configuration (see Specifying the Target Architecture and Implementation-Defined Behavior) and runtime library (see Using the GNAT Target Runtime Directory) should be set, so that GNATprove correctly interprets the behavior of the program at runtime.
[SPARK_FLOATING_POINT] When using floating-point numbers, GNATprove relies on the Semantics of Floating Point Operations as defined in IEEE-754. The compiler, OS, and hardware should all be configured so that IEEE-754 semantics are respected.
[SPARK_COMPILATION_SWITCHES] Compilation switches that change the behavior of the program should be the same between compilation and analysis. This is in particular the case for Overflow Modes.
[SPARK_ITERABLE] When a type is annotated with an
Iterable
aspect:the function
Has_Element
shall be such that, for any container objectContainer
and cursor objectCursor
,Has_Element (Container, Cursor)
only evaluates to True ifCursor
is accessible fromFirst (Container)
using the functionNext
, andfor any container object
Container
, the iteration fromFirst (Container)
through the functionNext
shall reach a cursorCursor
for whichHas_Element (Container, Cursor)
evaluates to False in a finite number of steps.
[SPARK_ITERABLE_FOR_PROOF] When a type has an
Iterable_For_Proof
annotation,the function
Contains
shall be such that, for any container objectContainer
and any elementE
,Contains (Container, E)
evaluates to True if and only if there is a cursor objectCursor
such thatHas_Element (Container, Cursor)
evaluates to True andE
is the result ofElement (Container, Cursor)
, orthe function
Model
shall be such that, for any container objectContainer
and any elementE
, there is a cursor objectCursor
such thatHas_Element (Container, Cursor)
evaluates to True andE
is the result ofElement (Container, Cursor)
if and only if there is a cursor objectM_Cursor
for the model type such thatHas_Element (Model (Container), M_Cursor)
evaluates to True andE
is the result ofElement (Model (Container), M_Cursor)
.
[SPARK_INITIALIZED_ATTRIBUTE] GNATprove assumes that the
Initialized
attribute is not referenced in any SPARK code that is executed. This assumption is necessary because evaluation of theInitialized
attribute during execution is based onValid_Scalars
, andValid_Scalars
sometimes evaluates to True on uninitialized data. Note that, despite this assumption, it can be valuable during testing to execute contracts and other ghost code that references theInitialized
attribute, as long as the executable code of the product itself does not reference theInitialized
attribute.[SPARK_OVERRIDING_AND_TASKING] If there are overriding operations called using a dispatching call, then GNATprove assumes that the overriding operation does not have any adverse tasking-related effects. In particular, GNATprove assumes that the overriding operation:
does not call protected entries,
does not suspend on suspension objects,
does not lock protected objects with calls to protected subprograms,
does not call Ada.Task_Identification.Current_Task.
In addition, the following assumptions need to be addressed when using SPARK on only part of a program:
[ADA_TASKING] If entry points for concurrent tasks (either OS tasks or units of computations scheduled by a runtime component) are not identified as tasks in SPARK, then during each invocation of a SPARK subprogram from such a task such that the SPARK subprogram is not being called directly or indirectly from another SPARK subprogram in the same task, the Global contract and by-reference parameters of the subprogram shall not conflict with either (a) the Global contract and by-reference parameters of any other such subprogram executing concurrently in another such task or (b) the Global contract of any concurrent task identified as a task in SPARK. Two global objects and/or by-reference parameters referring to the same object are said to conflict if both (1) they are not both synchronized and (2) at least one can be modified by the callee.
In addition, calls from SPARK units to subprograms which are not analyzed by GNATprove should not have any adverse tasking-related effects. In particular, GNATprove assumes that such calls do not cause tasks visible from SPARK to:
call protected entries that they are not calling in a way which is visible from SPARK,
suspend on suspension objects on which they do not suspend in a way which is visible from SPARK.
[ADA_EXTERNAL] Objects accessed outside of SPARK, either directly for statically allocated objects, or through their address or a pointer for all objects, should comply with the assumptions described in [SPARK_EXTERNAL], [SPARK_ALIASING_ADDRESS] and [SPARK_EXTERNAL_VALID].
[ADA_EXTERNAL_ABSTRACT_STATE] The modeling of Interfaces to the Physical World needs to be reviewed for abstract states whose value may be modified concurrently, when their refinement is not in SPARK. These abstract states should comply with the assumptions described in [SPARK_EXTERNAL].
[ADA_EXTERNAL_NAME] Objects annotated with an aspect
External_Name
orLink_Name
should comply with the assumptions described in [SPARK_EXTERNAL], [SPARK_ALIASING_ADDRESS] and [SPARK_EXTERNAL_VALID].[ADA_PRIVATE_TYPES] Private types whose full view is not analyzed, yet are used in SPARK code, need to comply with the implicit or explicit contracts used by GNATprove to analyze references to these types. This concerns:
private types and private type extensions declared in a package with a
pragma SPARK_Mode (Off);
in its private part,type completions in a non-SPARK package body.
The (explicit or implicit) type contract to check is made up of:
Default Initial Condition (explicit or implicit, no runtime error shall occur during default initialization of an object of this type unless its default initial condition does not refer to the current type instance or only refers to its discriminants and it evaluates to False)
Ownership annotations (implicit, if a type is not annotated with Ownership, copying it around shall not create visible aliasing and if it is not annotated with Needs_Reclamation, its finalization shall not leak resources or memory).
In addition, the default initialization of values of the type and the evaluation of its potential type invariant or subtype predicate shall not access any mutable state.
[ADA_TAGGED_TYPES] When a tagged type
T
visible in SPARK is extended outside of SPARK code, extensions ofT
whose full view is not analyzed by GNATprove shall not break the assumptions on values of typeT'Class
. In particular, they should abide by its Default Initial Condition, and should not add components which require a specific handling with respect to ownership.[ADA_RECURSIVE_TYPES] Recursive data-structures accessed by SPARK code but created out of SPARK should not be cyclic even if they are constant (but sharing is OK).
[ADA_ELABORATION] If a package is not analyzed but is part of the application code, its elaboration:
shall not modify any global state visible from SPARK unless it is part of the package’s own state.
shall always terminate normally.
In addition, if the package specification is referenced, directly or indirectly, from a SPARK unit, it needs to comply with the implicit or explicit contracts used by GNATprove to analyze these user packages.
The (explicit or implicit) package contract to check is made up of:
Initializes
contracts (explicit or implicitly generated by GNATprove)Initial_Condition
(only explicit)the aliases constraints of SPARK (implicit - there shall not be any aliases in the global state visible from SPARK after the package elaboration)
[ADA_SUBPROGRAMS] Subprograms that are not analyzed, yet are called from SPARK code, need to comply with the implicit or explicit contracts used by GNATprove to analyze calls to these subprograms. This concerns:
subprograms whose body is not given for analysis; and
subprograms whose body is marked
SPARK_Mode => Off
, either explicitly or implicitly (inherited from the enclosing scope).
Note that we consider here both non-generic subprograms and instantiations of generic subprograms, never generic subprograms themselves.
The (explicit or implicit) subprogram contract to check is made up of:
Type Contracts of parameters, result (for a function) and global objects produced as outputs from the non-SPARK callee to the SPARK caller
Postconditions (only explicit)
Contract Cases (only explicit)
Data Dependencies (explicit or implicitly generated by GNATprove)
Flow Dependencies (explicit or implicitly generated by GNATprove)
Exceptional Contracts (explicit or implicit) - the exceptional contract should list all exceptions that might be propagated by the subprogram and the associated postconditions should hold whenever an exception is propagated
Subprogram Termination (only explicit except for functions without side effects which should always return in SPARK) - subprograms annotated with
Always_Terminates
should terminate (return normally or raise an exception) whenever the associated boolean condition evaluates to True on entry of the subprogram, assuming that primary stack, secondary stack, and heap memory allocations never fail. Other subprograms are not restrictedthe aliasing constraints of SPARK (implicit - the subprogram shall not introduce any visible aliases between its parameters, accessed global objects, and return value if any, unless it is a traversal function, in which case its return value shall be a part of its traversed parameter, or unless the aliases introduced are compatible with assumption [SPARK_ALIASING_ADDRESS])
parameter modes - in particular, parameters of mode in which are not considered to be variable should not be modified, including the values designated by their potential access-to-variable subcomponents, and parameters of mode out which are not subject to relaxed initialization (see Aspect Relaxed_Initialization and Ghost Attribute Initialized) should be entirely initialized.
Note that this also applies to subprograms which are called indirectly from SPARK code, either through a dispatching call or through a call to an access-to-subprogram, and to (predefined) operators like
"="
.[ADA_CALLS] Calls to SPARK subprograms from subprograms that are not analyzed need to comply with the implicit or explicit preconditions used by GNATprove to analyze the called SPARK subprograms. This concerns the same subprograms as considered in [ADA_SUBPROGRAMS].
The (explicit or implicit) precondition to check is made up of:
Type Contracts of both parameters and global objects taken as input by the SPARK callee from the non-SPARK caller
Preconditions (explicit)
the aliasing constraints of SPARK (implicit) - the context shall not alias the callee’s parameters and accessed global objects in ways that are not allowed in SPARK
the initialization of inputs (implicit) - parameters of mode in or in out and global variables of mode Input or In_Out which are not subject to relaxed initialization (see Aspect Relaxed_Initialization and Ghost Attribute Initialized) should be entirely initialized
[ADA_OBJECT_ADDRESSES] When the body of a function is not analyzed by GNATprove, its result should not depend on the address of parts of its parameters or global inputs unless it is annotated with
Volatile_Function
. When the body of a procedure, entry or function with side effects is not analyzed by GNATprove, none of its outputs should depend on the address of parts of its parameters or global inputs unless the output is volatile for reading, or its value depends on an input which is volatile for reading as stated in a Depends contract.[ADA_STATE_ABSTRACTION] Units whose body is not analyzed, yet are used from SPARK code, need to declare suitable State Abstraction, and subprograms defining the API of such a unit should have correct Data Dependencies describing how a subprogram reads or writes parts of the state abstraction. The state abstraction may represent program variables, but also states of the OS, aspects of the file system, attributes of the underlying hardware, etc.
All entities that are part of the SPARK-compatible spec of the unit need to comply with the implicit or explicit contracts used by GNATprove to analyze use of these entities. This concerns:
the package itself (see Package Contracts); and
the API of the package.
[ADA_LOGICAL_EQUAL] If the aspect or pragma
Logical_Equal
is used on a function whose implementation is not analyzed, yet called from SPARK code, the implementation of this function should correspond to the logical equality for the corresponding type as used by GNATprove. See Annotation for Accessing the Logical Equality for a Type for information about the logical equality. Note that this assumption does not apply to functions without any implementation.[ADA_INLINE_FOR_PROOF] If the aspect or pragma
Inline_For_Proof
is used on a function with a postcondition whose implementation is not analyzed, yet called from SPARK code, and the function has a postcondition whose expression is syntactically a relation using the ‘=’ relational_operator (or an expression that parenthesizes such a relation), where one side of the relation is syntactically an attribute_reference to the Result attribute of the function, then GNATprove assumes that the value of the postcondition expression is true if and only if the function return value is logically equal to an Ada copy of the value of the other side of the relation.
In addition, the following assumptions need to be addressed when calling GNATprove on only part of a SPARK program at a time (either on an individual unit or on a group of units), while providing only the specs of those units that are not analyzed (not their bodies), so that the complete SPARK program is analyzed by calling GNATprove multiple times with different sets of unit bodies being available:
[PARTIAL_GLOBAL] Subprograms which are called across the boundary of those units analyzed together should have a Global contract describing their effect on global data, otherwise they will be assumed to have no effect on global data. The warning assumed Global null is guaranteed to be issued in cases where review is required.
[PARTIAL_TERMINATION] Procedures, entries and functions with side effects which are called across the boundary of those units analyzed together should be annotated to specify under which condition they shall terminate using the
Always_Terminates
aspect. Otherwise, these subprograms will be assumed to never terminate (if they are annotated withNo_Return
) or always terminate (otherwise). The warning assumed Always_Terminates is guaranteed to be issued in cases where review is required.[PARTIAL_TASKING] If no single run of GNATprove analyzes all units that define tasks, then for each run of GNATprove, all tasks not defined in units analyzed during that run of GNATprove must comply with [ADA_TASKING] as if those tasks were not SPARK tasks. Note: The environment task, which is present in every Ada partition, is considered by GNATprove to be defined by the unit that defines the main subprogram of that Ada partition. Note also: If an Ada partition defines no tasks other than the environment task, then that Ada partition is trivially in compliance with this assumption.
[PARTIAL_ACYCLIC_ANALYSIS] Consider the directed graph where the nodes are the compilation units and there is an edge from a unit A to a unit B if there is a with clause for B in the specification or the body of A. All (bodies of) units of a strongly connected component in this graph should be analyzed as part of a single analysis of GNATprove. This is so GNATprove can detect that the analyses of strongly connected units depend on each other and use its internal mechanism to avoid unsoundness.
In addition, the following assumptions need to be addressed when compiling the program with another compiler than GNAT:
[GNAT_SPARKLIB_LEMMAS] When using lemmas from the SPARK Lemma Library, GNAT-specific lemmas (e.g. on fixed-point arithmetic) should be reviewed to ensure that the same semantics is used in the compiler. The name of such lemmas starts with “GNAT” and the associated comment explains how it is specific to GNAT.
[GNAT_PEDANTIC] The switch
--pedantic
should be used as explained in section Specifying the Target Architecture and Implementation-Defined Behavior to warn about possible implementation-defined behavior, and the resulting warnings if any should be reviewed.[GNAT_PORTABILITY] The section Ensure Portability of Programs should be reviewed for possible differences in implementation defined behavior between GNAT/GNATprove and the chosen compiler (e.g. regarding choice of base type for scalars).