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
--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
(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 issues two kinds of warnings, which are controlled separately:
Compiler warnings are controlled with the usual GNAT compilation switches:
-gnatwssuppresses all warnings
-gnatwaenables all optional warnings
-gnatw?enables a specific warning denoted by the last character
See the GNAT User’s Guide for more details. These should passed through the compilation switches specified in the project file.
GNATprove specific warnings are controlled with switch
--warnings=offsuppresses all warnings
--warnings=errortreats warnings as errors
--warnings=continueissues warnings but does not stop analysis (default)
The default is that GNATprove issues warnings but does not stop.
Both types of warnings can be suppressed selectively by the use of pragma
Warnings in the source code. For example, GNATprove issues three warnings
Warn, which are suppressed by the three pragma
the source code:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
pragma Warnings (Off, "unused initial value of ""X""", Reason => "Parameter mode is mandated by API"); procedure Warn (X : in out Integer) with SPARK_Mode is pragma Warnings (Off, "initialization has no effect", Reason => "Coding standard requires initialization"); Y : Integer := 0; pragma Warnings (On, "initialization has no effect"); begin pragma Warnings (Off, "unused assignment", Reason => "Test program requires double assignment"); X := Y; pragma Warnings (On, "unused assignment"); X := Y; end Warn;
Warnings with the specified message are suppressed in the region starting at
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.
Warnings can also take a first argument of
to specify that it applies only to GNAT compiler or GNATprove. For example, the
previous example can be modified to use these refined pragma
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
pragma Warnings (GNATprove, Off, "unused initial value of ""X""", Reason => "Parameter mode is mandated by API"); procedure Warn2 (X : in out Integer) with SPARK_Mode is pragma Warnings (GNATprove, Off, "initialization has no effect", Reason => "Coding standard requires initialization"); Y : Integer := 0; pragma Warnings (GNATprove, On, "initialization has no effect"); begin pragma Warnings (GNATprove, Off, "unused assignment", Reason => "Test program requires double assignment"); X := Y; pragma Warnings (GNATprove, On, "unused assignment"); X := Y; end Warn2;
Besides the documentation benefit of using this refined version of pragma
Warnings, it makes it possible to detect useless pragma
do not suppress any warning, with switch
-gnatw.w. Indeed, this switch can
then be used both during compilation with GNAT and formal verification with
GNATprove, as pragma
Warnings that apply to only one tool can be identified
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, and their effect is controlled
--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.
22.214.171.124. 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:
is a fixed identifier
is one of
is a string literal describing the pattern of the check messages which shall be justified
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_Positiveindicates that the check cannot fail, although GNATprove was unable to prove it.
Intentionalindicates 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
"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 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");
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.
126.96.36.199. 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;
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
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_Callchanges, 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 of
External_Callwill 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
Assumethan if it is spread out into various pragmas
Annotate. If the information is required at several places, the pragma
Assumecan 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.
--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
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:
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 postconditon of the subprogram holds after each call of the subprogram.