In this section we discuss how to use Infer if you wish to make contributions to it or just look under the hood to learn more about how it is working. There are, for instance, debug options and ways to obtain the specs from the methods.
Structure of the results folder
After a successful Infer run, a directory is created to store the results of the
analysis. By default this directory is called
captured/contains information for each file analyzed by Infer. See below for more information.
specs/contains the specs of each function that was analyzed, as inferred by Infer.
log/and toplevel.log contains logs
report.jsoncontain the Infer reports in text and JSON formats
- there are other folders reserved for Infer's internal workings
Inside the folder
infer-out/captured there is a folder for each captured file.
Assume we captured a file called
example.c. Then, Infer creates the following
files inside the folder
.tenv contain the intermediate representation of
that file. This data is passed to the backend of Infer, which then performs the
analysis. The files contain serialized OCaml data structures. The
contains a control flow graph for each function or method implemented in the
file. The file
.cg contains the call graph of the functions defined or called
from that file. Finally, the file
.tenv contains all the types that are
defined or used in the file.
With the debug option enabled
infer run --debug -- <build command>, Infer
outputs debug information in infer-out/log/. The option
--stats provides only
light debug information, and
--print-logs outputs every message on the console
as well as in the log files.
In each captured folder, we obtain the file
icfg.dot, which is the graphical
representation of the file
.cfg and the file
call_graph.dot, that is the
graphical representation of the call graph.
Moreover, we obtain an HTML page for each captured file inside
infer-out/captured. This HTML file contains the source file. In each line of
the file there are links to the nodes of the control flow graph that correspond
to that line of code. So one can see what the translation looks like. Moreover,
when you click on those links you can see details of the symbolic execution of
that particular node.
Print the specs
It is also possible to print the specs created by Infer using the subcommand
infer report. You can print one particular spec that corresponds to one
method, or you can print all the specs in the results directory. Let us look at
We run Infer on this example with:
Infer saves the spec for the method
infer-out/specs and we can print
it with the command:
The convention for method names in Java is
<class name>.<method name>. This
outputs the following:
which expresses the fact that
this needs to be allocated at the beginning of
the method, and that at the end of the method the field
x is equal to
Moreover, you can print all the specs in the results directory with the command:
Run internal tests
There are many tests in the Infer code base that check that Infer behaves
correctly on small program examples. This is how you'd typically run the tests;
you can adapt the figure
8 depending on the number of cores available on your