pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[CLI] rename biabduction-specific option

Browse Source 
Summary:
Back in the days©, biabduction was the only analysis in infer, so a lot
of things implicitly assume we are talking about biabduction. Update
option names that are biabduction-specific to start with
`--biabduction-`.

Also update a few other options in the same spirit, eg for quandary, and
amend some doc messages just because they were not informative enough.

Also do some alphabetisation and moved a *bunch* of options that were in
the wrong section of Config.mli.

Reviewed By: skcho

Differential Revision: D27268094

fbshipit-source-id: a1c784188
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent 7d0aa9ec1c
commit d9c037e062
34 changed files with 568 additions and 504 deletions
Show Stats Download Patch File Download Diff File

36
infer/man/man1/infer-analyze.txt
Unescape View File

@ -34,6 +34,10 @@ OPTIONS
Activates: Enable biabduction and disable all other checkers
(Conversely: --no-biabduction-only)
--biabduction-write-dotty
Activates: Produce dotty files for specs and retain cycles reports
in infer-out/captured. (Conversely: --no-biabduction-write-dotty)
--bufferoverrun
Activates: checker bufferoverrun: InferBO is a detector for
out-of-bounds array accesses. (Conversely: --no-bufferoverrun)
@ -92,7 +96,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,
@ -172,6 +176,11 @@ OPTIONS
Activates: Enable impurity and disable all other checkers
(Conversely: --no-impurity-only)
--impurity-report-immutable-modifications
Activates: Report modifications to immutable fields in the
Impurity checker (Conversely:
--no-impurity-report-immutable-modifications)
--no-inefficient-keyset-iterator
Deactivates: checker inefficient-keyset-iterator: Check for
inefficient uses of iterators that iterate on keys then lookup
@ -418,6 +427,17 @@ OPTIONS
Activates: Enable uninit and disable all other checkers
(Conversely: --no-uninit-only)
--write-html
Activates: Produce html debug output for the analyses in
infer-out/captured. This shows the abstract state of all analyses
at each program point in the source code. Each captured source
file has its own html page. This HTML file contains the source
file, and at each line of the file there are links to the nodes of the control flow graph
of Infer's translation of that line of code into its intermediate
representation (SIL). This way it's possible to see what the
translation is, and the details of the symbolic execution on each
node. (Conversely: --no-write-html)
--xcode-isysroot-suffix string
Specify the suffix of Xcode isysroot directory, to avoid absolute
paths in tests
@ -463,6 +483,10 @@ CLANG OPTIONS
Override sources in all cxx annotation reachability specs with the
given sources spec
--biabduction-unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-biabduction-unsafe-malloc)
--clang-compound-literal-init-limit int
Limit after which initialization of compound types (structs and
arrays) is not done element by element but using a builtin
@ -478,16 +502,6 @@ CLANG OPTIONS
these types (or common wrappers around these types such as
unique_ptr<type>) will count as dead stores when the variables are
not read explicitly by the program.
--ml-buckets ,-separated sequence of { all | cf | arc | narc | cpp |
unknown_origin }
Specify the memory leak buckets to be checked in C++:
- cpp from C++ code
--unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-unsafe-malloc)
JAVA OPTIONS
--annotation-reachability-custom-pairs json
Specify custom sources/sink for the annotation reachability

2
infer/man/man1/infer-capture.txt
Unescape View File

@ -34,7 +34,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,

2
infer/man/man1/infer-compile.txt
Unescape View File

@ -18,7 +18,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,

3
infer/man/man1/infer-explore.txt
Unescape View File

@ -29,7 +29,8 @@ OPTIONS
Write results and internal files in the specified directory
EXPLORE BUGS
--html
Activates: Generate html report. (Conversely: --no-html)
Activates: Generate an html report of issues found. (Conversely:
--no-html)
--max-nesting int
Level of nested procedure calls to show. Trace elements beyond the

231
infer/man/man1/infer-full.txt
Unescape View File

@ -120,6 +120,15 @@ OPTIONS
Activates: Enable biabduction and disable all other checkers
(Conversely: --no-biabduction-only) See also infer-analyze(1).
--biabduction-unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-biabduction-unsafe-malloc) See also infer-analyze(1).
--biabduction-write-dotty
Activates: Produce dotty files for specs and retain cycles reports
in infer-out/captured. (Conversely: --no-biabduction-write-dotty)
See also infer-analyze(1).
--bo-debug int
Debug level for buffer-overrun checker (0-4) See also infer-analyze(1).
@ -344,8 +353,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
See also infer-analyze(1), infer-analyzejson(1),
--write-html) (Conversely: --no-debug | -G) See also infer-analyze(1), infer-analyzejson(1),
infer-capture(1), infer-compile(1), infer-report(1),
infer-reportdiff(1), and infer-run(1).
@ -706,8 +714,8 @@ OPTIONS
--hoisting-report-only-expensive) See also infer-report(1).
--html
Activates: Generate html report. (Conversely: --no-html)
See also infer-explore(1).
Activates: Generate an html report of issues found. (Conversely:
--no-html) See also infer-explore(1).
--immutable-cast
Activates: checker immutable-cast: Detection of object cast from
@ -729,6 +737,11 @@ OPTIONS
Activates: Enable impurity and disable all other checkers
(Conversely: --no-impurity-only) See also infer-analyze(1).
--impurity-report-immutable-modifications
Activates: Report modifications to immutable fields in the
Impurity checker (Conversely:
--no-impurity-report-immutable-modifications) See also infer-analyze(1).
--no-inefficient-keyset-iterator
Deactivates: checker inefficient-keyset-iterator: Check for
inefficient uses of iterators that iterate on keys then lookup
@ -881,13 +894,6 @@ OPTIONS
Activates: Merge the captured results directories specified in the
dependency file. (Conversely: --no-merge) See also infer-analyze(1).
--ml-buckets ,-separated sequence of { all | cf | arc | narc | cpp |
unknown_origin }
Specify the memory leak buckets to be checked in C++:
- cpp from C++ code
See also infer-analyze(1).
--pmd-xml
Activates: Output issues in (PMD) XML format in
infer-out/report.xml (Conversely: --no-pmd-xml) See also infer-run(1).
@ -1106,10 +1112,6 @@ OPTIONS
--report-formatter { none | phabricator }
Which formatter to use when emitting the report See also infer-report(1).
--report-immutable-modifications
Activates: Report modifications to immutable fields (Conversely:
--no-report-immutable-modifications) See also infer-report(1) and infer-run(1).
--report-previous path
Report of the base revision to use for comparison See also infer-reportdiff(1).
@ -1271,10 +1273,6 @@ OPTIONS
Activates: Enable uninit and disable all other checkers
(Conversely: --no-uninit-only) See also infer-analyze(1).
--unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-unsafe-malloc) See also infer-analyze(1).
--version
Print version information and exit See also infer-run(1).
@ -1288,6 +1286,18 @@ OPTIONS
relative to a common workspace. Usually a single project root is
enough, though. See also infer-capture(1).
--write-html
Activates: Produce html debug output for the analyses in
infer-out/captured. This shows the abstract state of all analyses
at each program point in the source code. Each captured source
file has its own html page. This HTML file contains the source
file, and at each line of the file there are links to the nodes of the control flow graph
of Infer's translation of that line of code into its intermediate
representation (SIL). This way it's possible to see what the
translation is, and the details of the symbolic execution on each
node. (Conversely: --no-write-html)
See also infer-analyze(1).
--write-website path_to_website_dir
Use to write website files documenting issue types and checkers
under path_to_website_dir/. Meant to be used within the Infer
@ -1327,26 +1337,33 @@ OPTIONS
INTERNAL OPTIONS
Use at your own risk.
--abs-struct int
--append-buck-flavors-reset
Set --append-buck-flavors to the empty list.
--backtrack-level int
Maximum level of backtracking to convert an absolute path to path
relative to the common prefix between the project root and the
path. For instance, with bactraking level 1, it will convert
/my/source/File.java with project root /my/root into
../source/File.java
--biabduction-abs-struct int
Specify abstraction level for fields of structs: - 0 = no
- 1 = forget some fields during matching (and so lseg
abstraction)
--abs-val int
--biabduction-abs-val int
Specify abstraction level for expressions: - 0 = no abstraction
- 1 = evaluate all expressions abstractly
- 2 = 1 + abstract constant integer values during join
--allow-leak
--biabduction-allow-leak
Activates: Forget leaked memory during abstraction (Conversely:
--no-allow-leak)
--append-buck-flavors-reset
Set --append-buck-flavors to the empty list.
--no-biabduction-allow-leak)
--array-level int
--biabduction-array-level int
Level of treating the array indexing and pointer arithmetic:
- 0 = treats both features soundly
- 1 = assumes that the size of every array is infinite
@ -1354,17 +1371,73 @@ INTERNAL OPTIONS
pointer arithmetic are correct
--backtrack-level int
Maximum level of backtracking to convert an absolute path to path
relative to the common prefix between the project root and the
path. For instance, with bactraking level 1, it will convert
/my/source/File.java with project root /my/root into
../source/File.java
--biabduction-coverage
analysis mode to maximize coverage (can take longer)
--biabduction-exit-node-bias
nodes nearest the exit node are analyzed first
--biabduction-iterations int
Specify the maximum number of operations for each function,
expressed as a multiple of symbolic operations and a multiple of
seconds of elapsed time
--biabduction-join-cond int
Set the strength of the final information-loss check used by the
join: - 0 = use the most aggressive join for preconditions
- 1 = use the least aggressive join for preconditions
--biabduction-memleak-buckets ,-separated sequence of { all | cf | arc
| narc | cpp | unknown_origin }
Specify the memory leak buckets to be checked in C++.
--biabduction-models-mode
Activates: Analysis of the biabduction models (Conversely:
--no-biabduction-models-mode)
--biabduction-monitor-prop-size
Activates: Monitor size of props, and print every time the current
max is exceeded (Conversely: --no-biabduction-monitor-prop-size)
--biabduction-nelseg
Activates: Use only nonempty lsegs (Conversely:
--no-biabduction-nelseg)
--biabduction-only-footprint
Activates: Skip the re-execution phase (Conversely:
--no-biabduction-only-footprint)
--biabduction-seconds-per-iteration float
Set the number of seconds per iteration (see
--biabduction-iterations)
--biabduction-seconds-per-iteration-reset
Cancel the effect of --biabduction-seconds-per-iteration.
--biabduction-symops-per-iteration int
Set the number of symbolic operations per iteration (see
--biabduction-iterations)
--biabduction-symops-per-iteration-reset
Cancel the effect of --biabduction-symops-per-iteration.
--biabduction-trace-join
Activates: Detailed tracing information during prop join
operations (Conversely: --no-biabduction-trace-join)
--biabduction-trace-rearrange
Activates: Detailed tracing information during prop re-arrangement
operations (Conversely: --no-biabduction-trace-rearrange)
--biabduction-type-size
Activates: Consider the size of types during analysis, e.g. cannot
use an int pointer to write to a char (Conversely:
--no-biabduction-type-size)
--biabduction-visits-bias
nodes visited fewer times are analyzed first
--bo-field-depth-limit-reset
Cancel the effect of --bo-field-depth-limit.
@ -1504,9 +1577,6 @@ INTERNAL OPTIONS
--costs-previous-reset
Cancel the effect of --costs-previous.
--coverage
analysis mode to maximize coverage (can take longer)
--debug-exceptions
Activates: Generate lightweight debugging information: just print
the internal exceptions during analysis (also sets
@ -1565,9 +1635,6 @@ INTERNAL OPTIONS
Activates: Print initial and final typestates (Conversely:
--no-eradicate-verbose)
--exit-node-bias
nodes nearest the exit node are analyzed first
--export-changed-functions
Activates: Make infer output changed functions, similar to
test-determinator. It is used together with the --modified-lines.
@ -1590,8 +1657,8 @@ INTERNAL OPTIONS
Cancel the effect of --file-renamings.
--no-filter-paths
Deactivates: Filters specified in .inferconfig (Conversely:
--filter-paths)
Deactivates: Apply filters specified in --report_* options.
Disable for debugging. (Conversely: --filter-paths)
--force-integration-reset
Cancel the effect of --force-integration.
@ -1653,11 +1720,6 @@ INTERNAL OPTIONS
--issues-tests-reset
Cancel the effect of --issues-tests.
--iterations int
Specify the maximum number of operations for each function,
expressed as a multiple of symbolic operations and a multiple of
seconds of elapsed time
--java-debug-source-file-info path
For debugging only: Call the Java declarations source file parser
on the given file and do not run anything else.
@ -1681,12 +1743,6 @@ INTERNAL OPTIONS
--job-id-reset
Cancel the effect of --job-id.
--join-cond int
Set the strength of the final information-loss check used by the
join: - 0 = use the most aggressive join for preconditions
- 1 = use the least aggressive join for preconditions
--linter-reset
Cancel the effect of --linter.
@ -1736,18 +1792,11 @@ INTERNAL OPTIONS
--modified-lines-reset
Cancel the effect of --modified-lines.
--monitor-prop-size
Activates: Monitor size of props, and print every time the current
max is exceeded (Conversely: --no-monitor-prop-size)
--nelseg
Activates: Use only nonempty lsegs (Conversely: --no-nelseg)
--never-returning-null json
Matcher or list of matchers for functions that never return null.
--nullable-annotation-name string
Specify custom nullable annotation name
Specify a custom nullable annotation name.
--nullable-annotation-name-reset
Cancel the effect of --nullable-annotation-name.
@ -1803,10 +1852,6 @@ INTERNAL OPTIONS
Deactivates: Disable expensive debugging output (Conversely:
--only-cheap-debug)
--only-footprint
Activates: Skip the re-execution phase (Conversely:
--no-only-footprint)
--oom-threshold int
Available memory threshold (in MB) below which multi-worker
scheduling throttles back work. Only for use on Linux.
@ -1814,11 +1859,6 @@ INTERNAL OPTIONS
--oom-threshold-reset
Cancel the effect of --oom-threshold.
--passthroughs
Activates: In error traces, show intermediate steps that propagate
data. When false, error traces are shorter and show only direct
flow via souces/sinks (Conversely: --no-passthroughs)
--print-buckets
Activates: Show the internal bucket of Infer reports in their
textual description (Conversely: --no-print-buckets)
@ -1844,8 +1884,9 @@ INTERNAL OPTIONS
Cancel the effect of --procedures-filter.
--process-clang-ast
Activates: process the ast to emit some info about the file (Not
available for Java) (Conversely: --no-process-clang-ast)
Activates: process the ast to emit some info about the file with
--test-determinator or --export-changed-functions (Not available
for Java) (Conversely: --no-process-clang-ast)
--profiler-samples path
File containing the profiler samples when Infer is run Test
@ -1916,6 +1957,12 @@ INTERNAL OPTIONS
Activates: [Purity]Consider unknown functions to be pure by
default (Conversely: --no-pure-by-default)
--quandary-show-passthroughs
Activates: In error traces, show intermediate steps that propagate
data. When false, error traces are shorter and show only direct
flow via souces/sinks (Conversely:
--no-quandary-show-passthroughs)
--reanalyze
Activates: Rerun the analysis. Not compatible with
--incremental-analysis and --continue-analysis. (Conversely:
@ -1968,12 +2015,6 @@ INTERNAL OPTIONS
add an extra set of strings (tagset) field to be set for each
sample of scuba, format <name>=(<value>,<value>,<value>|NONE)
--seconds-per-iteration float
Set the number of seconds per iteration (see --iterations)
--seconds-per-iteration-reset
Cancel the effect of --seconds-per-iteration.
--select-reset
Cancel the effect of --select.
@ -2029,8 +2070,8 @@ INTERNAL OPTIONS
--no-starvation-whole-program)
--no-subtype-multirange
Deactivates: Use the multirange subtyping domain (Conversely:
--subtype-multirange)
Deactivates: Use the multirange subtyping domain. Used in the Java
frontend and in biabduction. (Conversely: --subtype-multirange)
--summaries-caches-max-size int
The maximum amount of elements the summaries LRU caches can hold
@ -2041,13 +2082,6 @@ INTERNAL OPTIONS
annotations when deciding to suppress issues. Use for backwards
compatibility only! (Conversely: --no-suppress-lint-ignore-types)
--symops-per-iteration int
Set the number of symbolic operations per iteration (see
--iterations)
--symops-per-iteration-reset
Cancel the effect of --symops-per-iteration.
--tenv-json-reset
Cancel the effect of --tenv-json.
@ -2087,13 +2121,9 @@ INTERNAL OPTIONS
Activates: Emit Chrome performance trace events in
infer-out/perf_events.json (Conversely: --no-trace-events)
--trace-join
Activates: Detailed tracing information during prop join
operations (Conversely: --no-trace-join)
--trace-rearrange
Activates: Detailed tracing information during prop re-arrangement
operations (Conversely: --no-trace-rearrange)
--trace-ondemand
Activates: Emit debug information for the ondemand analysis
scheduler. (Conversely: --no-trace-ondemand)
--trace-topl
Activates: Detailed tracing information during TOPL analysis
@ -2112,10 +2142,6 @@ INTERNAL OPTIONS
The maximum number of traces for issues filtered out by
--report-filter to submit to Traceview
--type-size
Activates: Consider the size of types during analysis, e.g. cannot
use an int pointer to write to a char (Conversely: --no-type-size)
--uninit-interproc
Activates: Run uninit check in the experimental interprocedural
mode (Conversely: --no-uninit-interproc)
@ -2123,20 +2149,9 @@ INTERNAL OPTIONS
--version-vcs
Print version control system commit and exit
--visits-bias
nodes visited fewer times are analyzed first
--workspace-reset
Cancel the effect of --workspace.
--write-dotty
Activates: Produce dotty files for specs in the results directory
(Conversely: --no-write-dotty)
--write-html
Activates: Produce html debug output in the results directory
(Conversely: --no-write-html)
--write-html-whitelist-regex +string
Whitelist files that will have their html debug output printed
when --html is true.

6
infer/man/man1/infer-report.txt
Unescape View File

@ -58,7 +58,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,
@ -335,10 +335,6 @@ OPTIONS
--report-formatter { none | phabricator }
Which formatter to use when emitting the report
--report-immutable-modifications
Activates: Report modifications to immutable fields (Conversely:
--no-report-immutable-modifications)
--report-suppress-errors +error_name
do not report a type of errors

2
infer/man/man1/infer-reportdiff.txt
Unescape View File

@ -44,7 +44,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,

6
infer/man/man1/infer-run.txt
Unescape View File

@ -40,7 +40,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
--write-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level,
@ -118,10 +118,6 @@ OPTIONS
Activates: Force converting an absolute path to a relative path to
the root directory (Conversely: --no-report-force-relative-path)
--report-immutable-modifications
Activates: Report modifications to immutable fields (Conversely:
--no-report-immutable-modifications)
--report-suppress-errors +error_name
do not report a type of errors

48
infer/man/man1/infer.txt
Unescape View File

@ -120,6 +120,15 @@ OPTIONS
Activates: Enable biabduction and disable all other checkers
(Conversely: --no-biabduction-only) See also infer-analyze(1).
--biabduction-unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-biabduction-unsafe-malloc) See also infer-analyze(1).
--biabduction-write-dotty
Activates: Produce dotty files for specs and retain cycles reports
in infer-out/captured. (Conversely: --no-biabduction-write-dotty)
See also infer-analyze(1).
--bo-debug int
Debug level for buffer-overrun checker (0-4) See also infer-analyze(1).
@ -344,8 +353,7 @@ OPTIONS
Activates: Debug mode (also sets --debug-level 2,
--developer-mode, --print-buckets, --print-types,
--reports-include-ml-loc, --no-only-cheap-debug, --trace-error,
--write-dotty, --write-html) (Conversely: --no-debug | -G)
See also infer-analyze(1), infer-analyzejson(1),
--write-html) (Conversely: --no-debug | -G) See also infer-analyze(1), infer-analyzejson(1),
infer-capture(1), infer-compile(1), infer-report(1),
infer-reportdiff(1), and infer-run(1).
@ -706,8 +714,8 @@ OPTIONS
--hoisting-report-only-expensive) See also infer-report(1).
--html
Activates: Generate html report. (Conversely: --no-html)
See also infer-explore(1).
Activates: Generate an html report of issues found. (Conversely:
--no-html) See also infer-explore(1).
--immutable-cast
Activates: checker immutable-cast: Detection of object cast from
@ -729,6 +737,11 @@ OPTIONS
Activates: Enable impurity and disable all other checkers
(Conversely: --no-impurity-only) See also infer-analyze(1).
--impurity-report-immutable-modifications
Activates: Report modifications to immutable fields in the
Impurity checker (Conversely:
--no-impurity-report-immutable-modifications) See also infer-analyze(1).
--no-inefficient-keyset-iterator
Deactivates: checker inefficient-keyset-iterator: Check for
inefficient uses of iterators that iterate on keys then lookup
@ -881,13 +894,6 @@ OPTIONS
Activates: Merge the captured results directories specified in the
dependency file. (Conversely: --no-merge) See also infer-analyze(1).
--ml-buckets ,-separated sequence of { all | cf | arc | narc | cpp |
unknown_origin }
Specify the memory leak buckets to be checked in C++:
- cpp from C++ code
See also infer-analyze(1).
--pmd-xml
Activates: Output issues in (PMD) XML format in
infer-out/report.xml (Conversely: --no-pmd-xml) See also infer-run(1).
@ -1106,10 +1112,6 @@ OPTIONS
--report-formatter { none | phabricator }
Which formatter to use when emitting the report See also infer-report(1).
--report-immutable-modifications
Activates: Report modifications to immutable fields (Conversely:
--no-report-immutable-modifications) See also infer-report(1) and infer-run(1).
--report-previous path
Report of the base revision to use for comparison See also infer-reportdiff(1).
@ -1271,10 +1273,6 @@ OPTIONS
Activates: Enable uninit and disable all other checkers
(Conversely: --no-uninit-only) See also infer-analyze(1).
--unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely:
--no-unsafe-malloc) See also infer-analyze(1).
--version
Print version information and exit See also infer-run(1).
@ -1288,6 +1286,18 @@ OPTIONS
relative to a common workspace. Usually a single project root is
enough, though. See also infer-capture(1).
--write-html
Activates: Produce html debug output for the analyses in
infer-out/captured. This shows the abstract state of all analyses
at each program point in the source code. Each captured source
file has its own html page. This HTML file contains the source
file, and at each line of the file there are links to the nodes of the control flow graph
of Infer's translation of that line of code into its intermediate
representation (SIL). This way it's possible to see what the
translation is, and the details of the symbolic execution on each
node. (Conversely: --no-write-html)
See also infer-analyze(1).
--write-website path_to_website_dir
Use to write website files documenting issue types and checkers
under path_to_website_dir/. Meant to be used within the Infer

6
infer/src/absint/Mleak_buckets.ml
Unescape View File

@ -15,9 +15,11 @@ let bucket_to_message bucket =
match bucket with `MLeak_cpp -> "[CPP]" | `MLeak_unknown -> "[UNKNOWN ORIGIN]"
let contains_cpp = List.mem ~equal:( = ) Config.ml_buckets `MLeak_cpp
let contains_cpp = List.mem ~equal:( = ) Config.biabduction_memleak_buckets `MLeak_cpp
let contains_unknown_origin =
List.mem ~equal:( = ) Config.biabduction_memleak_buckets `MLeak_unknown
let contains_unknown_origin = List.mem ~equal:( = ) Config.ml_buckets `MLeak_unknown
let should_raise_leak_unknown_origin = contains_unknown_origin

2
infer/src/absint/TaintTrace.ml
Unescape View File

@ -518,7 +518,7 @@ module Make (Spec : Spec) = struct
|> Sinks.of_list |> Sinks.union caller_trace.sinks
in
let passthroughs =
if Config.passthroughs then
if Config.quandary_show_passthroughs then
if phys_equal sources caller_trace.sources && phys_equal sinks caller_trace.sinks then
(* this callee didn't add any new sources or any news sinks; it's just a passthrough *)
Passthroughs.add (Passthrough.make callee_site) caller_trace.passthroughs

439
infer/src/base/Config.ml
Unescape View File

@ -496,27 +496,6 @@ let () =
CLOpt.mk_subcommand cmd ~name ?deprecated_long ~on_unknown_arg (Some command_doc) )
let abs_struct =
CLOpt.mk_int ~deprecated:["absstruct"] ~long:"abs-struct" ~default:1 ~meta:"int"
{|Specify abstraction level for fields of structs:
- 0 = no
- 1 = forget some fields during matching (and so lseg abstraction)
|}
and abs_val =
CLOpt.mk_int ~deprecated:["absval"] ~long:"abs-val" ~default:2 ~meta:"int"
{|Specify abstraction level for expressions:
- 0 = no abstraction
- 1 = evaluate all expressions abstractly
- 2 = 1 + abstract constant integer values during join
|}
and allow_leak =
CLOpt.mk_bool ~deprecated:["leak"] ~long:"allow-leak" "Forget leaked memory during abstraction"
and analyzer =
CLOpt.mk_symbol ~deprecated:["analyzer"; "-analyzer"; "a"] ~long:"" ~default:Checkers
~eq:equal_analyzer ~symbols:string_to_analyzer
@ -638,8 +617,30 @@ and append_buck_flavors =
$(b,--buck-compilation-database) option."
and array_level =
CLOpt.mk_int ~deprecated:["arraylevel"] ~long:"array-level" ~default:0 ~meta:"int"
let biabduction_abs_struct =
CLOpt.mk_int ~deprecated:["-abs-struct"] ~long:"biabduction-abs-struct" ~default:1 ~meta:"int"
{|Specify abstraction level for fields of structs:
- 0 = no
- 1 = forget some fields during matching (and so lseg abstraction)
|}
and biabduction_abs_val =
CLOpt.mk_int ~deprecated:["-abs-val"] ~long:"biabduction-abs-val" ~default:2 ~meta:"int"
{|Specify abstraction level for expressions:
- 0 = no abstraction
- 1 = evaluate all expressions abstractly
- 2 = 1 + abstract constant integer values during join
|}
and biabduction_allow_leak =
CLOpt.mk_bool ~deprecated:["-allow-leak"] ~long:"biabduction-allow-leak"
"Forget leaked memory during abstraction"
and biabduction_array_level =
CLOpt.mk_int ~deprecated:["-array-level"] ~long:"biabduction-array-level" ~default:0 ~meta:"int"
{|Level of treating the array indexing and pointer arithmetic:
- 0 = treats both features soundly
- 1 = assumes that the size of every array is infinite
@ -647,10 +648,93 @@ and array_level =
|}
and biabduction_iterations =
CLOpt.mk_int ~deprecated:["-iterations"] ~long:"biabduction-iterations" ~default:1 ~meta:"int"
"Specify the maximum number of operations for each function, expressed as a multiple of \
symbolic operations and a multiple of seconds of elapsed time"
and biabduction_join_cond =
CLOpt.mk_int ~deprecated:["-join-cond"] ~long:"biabduction-join-cond" ~default:1 ~meta:"int"
{|Set the strength of the final information-loss check used by the join:
- 0 = use the most aggressive join for preconditions
- 1 = use the least aggressive join for preconditions
|}
and biabduction_memleak_buckets =
CLOpt.mk_symbol_seq ~deprecated:["-ml-buckets"] ~long:"biabduction-memleak-buckets"
~default:[`MLeak_cf] ~symbols:ml_bucket_symbols ~eq:PolyVariantEqual.( = )
"Specify the memory leak buckets to be checked in C++."
and biabduction_models_mode =
CLOpt.mk_bool ~long:"biabduction-models-mode" "Analysis of the biabduction models"
and biabduction_monitor_prop_size =
CLOpt.mk_bool ~deprecated:["-monitor-prop-size"] ~long:"biabduction-monitor-prop-size"
"Monitor size of props, and print every time the current max is exceeded"
and biabduction_nelseg =
CLOpt.mk_bool ~deprecated:["-nelseg"] ~long:"biabduction-nelseg" "Use only nonempty lsegs"
and biabduction_only_footprint =
CLOpt.mk_bool ~deprecated:["-only-footprint"] ~long:"biabduction-only-footprint"
"Skip the re-execution phase"
and biabduction_seconds_per_iteration =
CLOpt.mk_float_opt ~deprecated:["-seconds-per-iteration"]
~long:"biabduction-seconds-per-iteration" ~meta:"float"
"Set the number of seconds per iteration (see $(b,--biabduction-iterations))"
and biabduction_symops_per_iteration =
CLOpt.mk_int_opt ~deprecated:["-symops-per-iteration"] ~long:"biabduction-symops-per-iteration"
~meta:"int"
"Set the number of symbolic operations per iteration (see $(b,--biabduction-iterations))"
and biabduction_trace_join =
CLOpt.mk_bool ~deprecated:["-trace-join"] ~long:"biabduction-trace-join"
"Detailed tracing information during prop join operations"
and biabduction_trace_rearrange =
CLOpt.mk_bool ~deprecated:["-trace-rearrange"] ~long:"biabduction-trace-rearrange"
"Detailed tracing information during prop re-arrangement operations"
and biabduction_type_size =
CLOpt.mk_bool ~deprecated:["-type-size"] ~long:"biabduction-type-size"
"Consider the size of types during analysis, e.g. cannot use an int pointer to write to a char"
and biabduction_unsafe_malloc =
CLOpt.mk_bool ~deprecated:["-unsafe-malloc"] ~long:"biabduction-unsafe-malloc"
~in_help:InferCommand.[(Analyze, manual_clang)]
"Assume that malloc(3) never returns null."
(** visit mode for the worklist:
- 0 depth - fist visit
- 1 bias towards exit node
- 2 least visited first *)
and biabduction_worklist_mode =
let var = ref 0 in
CLOpt.mk_set var 2 ~deprecated:["-coverage"] ~long:"biabduction-coverage"
"analysis mode to maximize coverage (can take longer)" ;
CLOpt.mk_set var 1 ~deprecated:["-exit-node-bias"] ~long:"biabduction-exit-node-bias"
"nodes nearest the exit node are analyzed first" ;
CLOpt.mk_set var 2 ~deprecated:["-visits-bias"] ~long:"biabduction-visits-bias"
"nodes visited fewer times are analyzed first" ;
var
and bo_field_depth_limit =
CLOpt.mk_int_opt ~long:"bo-field-depth-limit"
~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
@ -992,14 +1076,6 @@ and cost_tests_only_autoreleasepool =
"[EXPERIMENTAL] Report only autoreleasepool size results in cost tests"
and siof_check_iostreams =
CLOpt.mk_bool ~long:"siof-check-iostreams"
~in_help:InferCommand.[(Analyze, manual_siof)]
"Do not assume that iostreams (cout, cerr, ...) are always initialized. The default is to \
assume they are always initialized to avoid false positives. However, if your program \
compiles against a recent libstdc++ then it is safe to turn this option on."
and cxx_scope_guards =
CLOpt.mk_json ~long:"cxx-scope-guards"
~in_help:InferCommand.[(Analyze, manual_clang)]
@ -1019,7 +1095,8 @@ and custom_symbols =
"Specify named lists of symbols available to rules"
and ( bo_debug
and ( biabduction_write_dotty
, bo_debug
, deduplicate
, developer_mode
, debug
@ -1040,8 +1117,7 @@ and ( bo_debug
, print_types
, reports_include_ml_loc
, trace_error
, write_html
, write_dotty ) =
, write_html ) =
let all_generic_manuals =
List.filter_map InferCommand.all_commands ~f:(fun (command : InferCommand.t) ->
match command with
@ -1050,7 +1126,12 @@ and ( bo_debug
| (Analyze | AnalyzeJson | Capture | Compile | Report | ReportDiff | Run) as command ->
Some (command, manual_generic) )
in
let bo_debug =
let biabduction_write_dotty =
CLOpt.mk_bool ~long:"biabduction-write-dotty"
~in_help:InferCommand.[(Analyze, manual_generic)]
(Printf.sprintf "Produce dotty files for specs and retain cycles reports in %s."
(ResultsDirEntryName.get_path ~results_dir:"infer-out" Debug))
and bo_debug =
CLOpt.mk_int ~default:0 ~long:"bo-debug"
~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
"Debug level for buffer-overrun checker (0-4)"
@ -1099,9 +1180,16 @@ and ( bo_debug
and trace_error =
CLOpt.mk_bool ~long:"trace-error" "Detailed tracing information during error explanation"
and write_html =
CLOpt.mk_bool ~long:"write-html" "Produce html debug output in the results directory"
and write_dotty =
CLOpt.mk_bool ~long:"write-dotty" "Produce dotty files for specs in the results directory"
CLOpt.mk_bool ~long:"write-html"
~in_help:InferCommand.[(Analyze, manual_generic)]
(Printf.sprintf
"Produce html debug output for the analyses in %s. This shows the abstract state of all \
analyses at each program point in the source code. Each captured source file has its own \
html page. This HTML file contains the source file, and at each line of\n\
the file there are links to the nodes of the control flow graph of Infer's translation \
of that line of code into its intermediate representation (SIL). This way it's possible \
to see what the translation is, and the details of the symbolic execution on each node."
(ResultsDirEntryName.get_path ~results_dir:"infer-out" Debug))
in
let set_debug_level level =
bo_debug := level ;
@ -1115,18 +1203,12 @@ and ( bo_debug
~in_help:all_generic_manuals
"Debug mode (also sets $(b,--debug-level 2), $(b,--developer-mode), $(b,--print-buckets), \
$(b,--print-types), $(b,--reports-include-ml-loc), $(b,--no-only-cheap-debug), \
$(b,--trace-error), $(b,--write-dotty), $(b,--write-html))"
$(b,--trace-error), $(b,--write-html))"
~f:(fun debug ->
if debug then set_debug_level 2 else set_debug_level 0 ;
CommandLineOption.keep_args_file := debug ;
debug )
[ developer_mode
; print_buckets
; print_types
; reports_include_ml_loc
; trace_error
; write_html
; write_dotty ]
[developer_mode; print_buckets; print_types; reports_include_ml_loc; trace_error; write_html]
[only_cheap_debug]
and (_ : int option ref) =
CLOpt.mk_int_opt ~long:"debug-level" ~in_help:all_generic_manuals ~meta:"level"
@ -1175,7 +1257,8 @@ and ( bo_debug
debug )
[debug; developer_mode] [default_linters; keep_going]
in
( bo_debug
( biabduction_write_dotty
, bo_debug
, deduplicate
, developer_mode
, debug
@ -1196,8 +1279,7 @@ and ( bo_debug
, print_types
, reports_include_ml_loc
, trace_error
, write_html
, write_dotty )
, write_html )
and dependencies =
@ -1300,6 +1382,13 @@ and eradicate_return_over_annotated =
and eradicate_verbose = CLOpt.mk_bool ~long:"eradicate-verbose" "Print initial and final typestates"
and export_changed_functions =
CLOpt.mk_bool ~deprecated:["test-determinator-clang"] ~long:"export-changed-functions"
~default:false
"Make infer output changed functions, similar to test-determinator. It is used together with \
the $(b,--modified-lines)."
and external_java_packages =
CLOpt.mk_string_list ~long:"external-java-packages"
~in_help:InferCommand.[(Analyze, manual_java)]
@ -1328,7 +1417,8 @@ and file_renamings =
and filter_paths =
CLOpt.mk_bool ~long:"filter-paths" ~default:true "Filters specified in .inferconfig"
CLOpt.mk_bool ~long:"filter-paths" ~default:true
"Apply filters specified in $(b,--report_*) options. Disable for debugging."
and force_delete_results_dir =
@ -1438,7 +1528,7 @@ and help_issue_type =
and html =
CLOpt.mk_bool ~long:"html"
~in_help:InferCommand.[(Explore, manual_explore_bugs)]
"Generate html report."
"Generate an html report of issues found."
and hoisting_report_only_expensive =
@ -1454,6 +1544,14 @@ and icfg_dotty_outfile =
options that would generate icfg file otherwise"
and impurity_report_immutable_modifications =
CLOpt.mk_bool
~deprecated:["-report-immutable-modifications"]
~long:"impurity-report-immutable-modifications" ~default:false
~in_help:InferCommand.[(Analyze, manual_generic)]
"Report modifications to immutable fields in the Impurity checker"
and inclusive_cost =
CLOpt.mk_bool ~long:"inclusive-cost" ~default:true "Computes the inclusive cost"
@ -1474,12 +1572,6 @@ and issues_tests =
~meta:"file" "Write a list of issues in a format suitable for tests to $(i,file)"
and iterations =
CLOpt.mk_int ~deprecated:["iterations"] ~long:"iterations" ~default:1 ~meta:"int"
"Specify the maximum number of operations for each function, expressed as a multiple of \
symbolic operations and a multiple of seconds of elapsed time"
and java_debug_source_file_info =
CLOpt.mk_path_opt ~long:"java-debug-source-file-info" ~meta:"path"
"For debugging only: Call the Java declarations source file parser on the given file and do \
@ -1512,14 +1604,6 @@ and jobs =
~meta:"int" "Run the specified number of analysis jobs simultaneously"
and join_cond =
CLOpt.mk_int ~deprecated:["join_cond"] ~long:"join-cond" ~default:1 ~meta:"int"
{|Set the strength of the final information-loss check used by the join:
- 0 = use the most aggressive join for preconditions
- 1 = use the least aggressive join for preconditions
|}
and liveness_dangerous_classes =
CLOpt.mk_json ~long:"liveness-dangerous-classes"
~in_help:InferCommand.[(Analyze, manual_clang)]
@ -1655,31 +1739,14 @@ and method_decls_info =
method name, etc.) when Infer is run Test Determinator mode with $(b,--test-determinator)."
and ml_buckets =
CLOpt.mk_symbol_seq ~deprecated:["ml_buckets"; "-ml_buckets"] ~long:"ml-buckets"
~default:[`MLeak_cf]
~in_help:InferCommand.[(Analyze, manual_clang)]
{|Specify the memory leak buckets to be checked in C++:
- $(b,cpp) from C++ code
|}
~symbols:ml_bucket_symbols ~eq:PolyVariantEqual.( = )
and modified_lines =
CLOpt.mk_path_opt ~long:"modified-lines"
"Specifies the file containing the modified lines when Infer is run Test Determinator mode \
with $(b,--test-determinator)."
and monitor_prop_size =
CLOpt.mk_bool ~deprecated:["monitor_prop_size"] ~long:"monitor-prop-size"
"Monitor size of props, and print every time the current max is exceeded"
and nelseg = CLOpt.mk_bool ~deprecated:["nelseg"] ~long:"nelseg" "Use only nonempty lsegs"
and nullable_annotation =
CLOpt.mk_string_opt ~long:"nullable-annotation-name" "Specify custom nullable annotation name"
CLOpt.mk_string_opt ~long:"nullable-annotation-name" "Specify a custom nullable annotation name."
and nullsafe_annotation_graph =
@ -1725,22 +1792,12 @@ and nullsafe_strict_containers =
"Warn when containers are used with nullable keys or values"
and only_footprint =
CLOpt.mk_bool ~deprecated:["only_footprint"] ~long:"only-footprint" "Skip the re-execution phase"
and oom_threshold =
CLOpt.mk_int_opt ~long:"oom-threshold"
"Available memory threshold (in MB) below which multi-worker scheduling throttles back work. \
Only for use on Linux."
and passthroughs =
CLOpt.mk_bool ~long:"passthroughs" ~default:false
"In error traces, show intermediate steps that propagate data. When false, error traces are \
shorter and show only direct flow via souces/sinks"
and patterns_modeled_expensive =
let long = "modeled-expensive" in
( long
@ -1869,7 +1926,8 @@ and procedures_summary_json =
and process_clang_ast =
CLOpt.mk_bool ~long:"process-clang-ast" ~default:false
"process the ast to emit some info about the file (Not available for Java)"
"process the ast to emit some info about the file with $(b,--test-determinator) or \
$(b,--export-changed-functions) (Not available for Java)"
and progress_bar =
@ -2018,6 +2076,12 @@ and quandary_sanitizers =
"Specify custom sanitizers for Quandary"
and quandary_show_passthroughs =
CLOpt.mk_bool ~deprecated:["-passthroughs"] ~long:"quandary-show-passthroughs" ~default:false
"In error traces, show intermediate steps that propagate data. When false, error traces are \
shorter and show only direct flow via souces/sinks"
and quandary_sources =
CLOpt.mk_json ~long:"quandary-sources"
~in_help:InferCommand.[(Analyze, manual_quandary)]
@ -2042,7 +2106,7 @@ and racerd_guardedby =
"Check @GuardedBy annotations with RacerD"
and[@warning "-32"] racerd_unknown_returns_owned =
and _racerd_unknown_returns_owned =
CLOpt.mk_bool ~deprecated:["racerd-unknown-returns-owned"] ~long:"racerd-unknown-returns-owned"
~default:true
~in_help:InferCommand.[(Analyze, manual_racerd)]
@ -2133,12 +2197,6 @@ and report_formatter =
~eq:PolyVariantEqual.( = ) "Which formatter to use when emitting the report"
and report_immutable_modifications =
CLOpt.mk_bool ~long:"report-immutable-modifications" ~default:false
~in_help:InferCommand.[(Report, manual_generic); (Run, manual_generic)]
"Report modifications to immutable fields"
and report_previous =
CLOpt.mk_path_opt ~long:"report-previous"
~in_help:InferCommand.[(ReportDiff, manual_generic)]
@ -2167,9 +2225,16 @@ and results_dir =
~meta:"dir" "Write results and internal files in the specified directory"
and seconds_per_iteration =
CLOpt.mk_float_opt ~deprecated:["seconds_per_iteration"] ~long:"seconds-per-iteration"
~meta:"float" "Set the number of seconds per iteration (see $(b,--iterations))"
and scheduler =
CLOpt.mk_symbol ~long:"scheduler" ~default:File ~eq:equal_scheduler
~in_help:InferCommand.[(Analyze, manual_generic)]
~symbols:[("file", File); ("restart", Restart); ("callgraph", SyntacticCallGraph)]
"Specify the scheduler used for the analysis phase:\n\
- file: schedule one job per file\n\
- callgraph: schedule one job per procedure, following the syntactic call graph. Usually \
faster than \"file\".\n\
- restart: same as callgraph but uses locking to try and avoid duplicate work between \
different analysis processes and thus performs better in some circumstances"
and select =
@ -2199,6 +2264,14 @@ and scuba_tags =
<name>=(<value>,<value>,<value>|NONE)"
and siof_check_iostreams =
CLOpt.mk_bool ~long:"siof-check-iostreams"
~in_help:InferCommand.[(Analyze, manual_siof)]
"Do not assume that iostreams (cout, cerr, ...) are always initialized. The default is to \
assume they are always initialized to avoid false positives. However, if your program \
compiles against a recent libstdc++ then it is safe to turn this option on."
and siof_safe_methods =
CLOpt.mk_string_list ~long:"siof-safe-methods"
~in_help:InferCommand.[(Analyze, manual_siof)]
@ -2352,7 +2425,7 @@ and (_ : bool ref) =
and subtype_multirange =
CLOpt.mk_bool ~deprecated:["subtype_multirange"] ~long:"subtype-multirange" ~default:true
"Use the multirange subtyping domain"
"Use the multirange subtyping domain. Used in the Java frontend and in biabduction."
and summaries_caches_max_size =
@ -2360,36 +2433,12 @@ and summaries_caches_max_size =
"The maximum amount of elements the summaries LRU caches can hold"
and symops_per_iteration =
CLOpt.mk_int_opt ~deprecated:["symops_per_iteration"] ~long:"symops-per-iteration" ~meta:"int"
"Set the number of symbolic operations per iteration (see $(b,--iterations))"
and test_determinator =
CLOpt.mk_bool ~long:"test-determinator" ~default:false
"Run infer in Test Determinator mode. It is used together with the $(b,--modified-lines) and \
$(b,--profiler-samples) flags, which specify the relevant arguments."
and export_changed_functions =
CLOpt.mk_bool ~deprecated:["test-determinator-clang"] ~long:"export-changed-functions"
~default:false
"Make infer output changed functions, similar to test-determinator. It is used together with \
the $(b,--modified-lines)."
and scheduler =
CLOpt.mk_symbol ~long:"scheduler" ~default:File ~eq:equal_scheduler
~in_help:InferCommand.[(Analyze, manual_generic)]
~symbols:[("file", File); ("restart", Restart); ("callgraph", SyntacticCallGraph)]
"Specify the scheduler used for the analysis phase:\n\
- file: schedule one job per file\n\
- callgraph: schedule one job per procedure, following the syntactic call graph. Usually \
faster than \"file\".\n\
- restart: same as callgraph but uses locking to try and avoid duplicate work between \
different analysis processes and thus performs better in some circumstances"
and test_filtering =
CLOpt.mk_bool ~deprecated:["test_filtering"] ~long:"test-filtering"
"List all the files Infer can report on (should be called from the root of the project)"
@ -2446,16 +2495,8 @@ and trace_events =
(ResultsDirEntryName.get_path ~results_dir:"infer-out" PerfEvents))
and trace_join =
CLOpt.mk_bool ~deprecated:["trace_join"] ~long:"trace-join"
"Detailed tracing information during prop join operations"
and trace_ondemand = CLOpt.mk_bool ~long:"trace-ondemand" ""
and trace_rearrange =
CLOpt.mk_bool ~deprecated:["trace_rearrange"] ~long:"trace-rearrange"
"Detailed tracing information during prop re-arrangement operations"
and trace_ondemand =
CLOpt.mk_bool ~long:"trace-ondemand" "Emit debug information for the ondemand analysis scheduler."
and trace_topl =
@ -2476,21 +2517,10 @@ and tv_limit_filtered =
"The maximum number of traces for issues filtered out by --report-filter to submit to Traceview"
and type_size =
CLOpt.mk_bool ~deprecated:["type_size"] ~long:"type-size"
"Consider the size of types during analysis, e.g. cannot use an int pointer to write to a char"
and uninit_interproc =
CLOpt.mk_bool ~long:"uninit-interproc" "Run uninit check in the experimental interprocedural mode"
and unsafe_malloc =
CLOpt.mk_bool ~long:"unsafe-malloc"
~in_help:InferCommand.[(Analyze, manual_clang)]
"Assume that malloc(3) never returns null."
and incremental_analysis =
CLOpt.mk_bool ~long:"incremental-analysis" ~default:false
"[EXPERIMENTAL] Use incremental analysis for changed files. Not compatible with \
@ -2509,21 +2539,6 @@ and version =
var
(** visit mode for the worklist:
- 0 depth - fist visit
- 1 bias towards exit node
- 2 least visited first *)
and worklist_mode =
let var = ref 0 in
CLOpt.mk_set var 2 ~long:"coverage" "analysis mode to maximize coverage (can take longer)" ;
CLOpt.mk_set var 1 ~long:"exit-node-bias" ~deprecated:["exit_node_bias"]
"nodes nearest the exit node are analyzed first" ;
CLOpt.mk_set var 2 ~long:"visits-bias" ~deprecated:["visits_bias"]
"nodes visited fewer times are analyzed first" ;
var
and workspace =
CLOpt.mk_path_opt ~long:"workspace"
~in_help:InferCommand.[(Capture, manual_generic)]
@ -2725,15 +2740,17 @@ let post_parsing_initialization command_opt =
Gc.set {ctrl with minor_heap_size; allocation_policy; space_overhead}
in
set_gc_params () ;
let symops_timeout, seconds_timeout =
let biabd_symops_timeout, biabd_seconds_timeout =
let default_symops_timeout = 1100 in
let default_seconds_timeout = 10.0 in
if !biabduction_models_mode then (* disable timeouts when analyzing models *)
(None, None)
else (Some default_symops_timeout, Some default_seconds_timeout)
in
if is_none !symops_per_iteration then symops_per_iteration := symops_timeout ;
if is_none !seconds_per_iteration then seconds_per_iteration := seconds_timeout ;
if is_none !biabduction_symops_per_iteration then
biabduction_symops_per_iteration := biabd_symops_timeout ;
if is_none !biabduction_seconds_per_iteration then
biabduction_seconds_per_iteration := biabd_seconds_timeout ;
clang_compilation_dbs :=
RevList.rev_map ~f:(fun x -> `Raw x) !compilation_database
|> RevList.rev_map_append ~f:(fun x -> `Escaped x) !compilation_database_escaped ;
@ -2777,11 +2794,43 @@ let process_linters_doc_url args =
let rest = !rest
and abs_struct = !abs_struct
and biabduction_abs_struct = !biabduction_abs_struct
and biabduction_abs_val = !biabduction_abs_val
and biabduction_allow_leak = !biabduction_allow_leak
and biabduction_array_level = !biabduction_array_level
and biabduction_models_mode = !biabduction_models_mode
and biabduction_iterations = !biabduction_iterations
and biabduction_join_cond = !biabduction_join_cond
and biabduction_memleak_buckets = !biabduction_memleak_buckets
and biabduction_monitor_prop_size = !biabduction_monitor_prop_size
and biabduction_nelseg = !biabduction_nelseg
and biabduction_only_footprint = !biabduction_only_footprint
and biabduction_seconds_per_iteration = !biabduction_seconds_per_iteration
and biabduction_symops_per_iteration = !biabduction_symops_per_iteration
and biabduction_trace_join = !biabduction_trace_join
and biabduction_trace_rearrange = !biabduction_trace_rearrange
and biabduction_type_size = !biabduction_type_size
and biabduction_unsafe_malloc = !biabduction_unsafe_malloc
and abs_val = !abs_val
and biabduction_worklist_mode = !biabduction_worklist_mode
and allow_leak = !allow_leak
and biabduction_write_dotty = !biabduction_write_dotty
and annotation_reachability_cxx = !annotation_reachability_cxx
@ -2791,10 +2840,6 @@ and annotation_reachability_custom_pairs = !annotation_reachability_custom_pairs
and append_buck_flavors = RevList.to_list !append_buck_flavors
and array_level = !array_level
and biabduction_models_mode = !biabduction_models_mode
and bootclasspath = !bootclasspath
and bo_debug = !bo_debug
@ -3040,14 +3085,16 @@ and global_tenv = !global_tenv
and icfg_dotty_outfile = !icfg_dotty_outfile
and impurity_report_immutable_modifications = !impurity_report_immutable_modifications
and inclusive_cost = !inclusive_cost
and incremental_analysis = !incremental_analysis
and issues_tests = !issues_tests
and issues_tests_fields = !issues_tests_fields
and iterations = !iterations
and java_debug_source_file_info = !java_debug_source_file_info
and java_jar_compiler = !java_jar_compiler
@ -3062,8 +3109,6 @@ and job_id = !job_id
and jobs = Option.fold !max_jobs ~init:!jobs ~f:min
and join_cond = !join_cond
and linter = !linter
and linters_def_file = RevList.to_list !linters_def_file
@ -3098,14 +3143,8 @@ and merge = !merge
and method_decls_info = !method_decls_info
and ml_buckets = !ml_buckets
and modified_lines = !modified_lines
and monitor_prop_size = !monitor_prop_size
and nelseg = !nelseg
and nullable_annotation = !nullable_annotation
and nullsafe_annotation_graph = !nullsafe_annotation_graph
@ -3132,10 +3171,6 @@ and oom_threshold = !oom_threshold
and only_cheap_debug = !only_cheap_debug
and only_footprint = !only_footprint
and passthroughs = !passthroughs
and patterns_modeled_expensive = match patterns_modeled_expensive with k, r -> (k, !r)
and patterns_never_returning_null = match patterns_never_returning_null with k, r -> (k, !r)
@ -3150,6 +3185,8 @@ and print_active_checkers = !print_active_checkers
and print_builtins = !print_builtins
and print_jbir = !print_jbir
and print_logs = !print_logs
and print_types = !print_types
@ -3255,6 +3292,8 @@ and quandary_endpoints = !quandary_endpoints
and quandary_sanitizers = !quandary_sanitizers
and quandary_show_passthroughs = !quandary_show_passthroughs
and quandary_sources = !quandary_sources
and quandary_sinks = !quandary_sinks
@ -3283,8 +3322,6 @@ and report_force_relative_path = !report_force_relative_path
and report_formatter = !report_formatter
and report_immutable_modifications = !report_immutable_modifications
and report_path_regex_blacklist = RevList.to_list !report_path_regex_blacklist
and report_path_regex_whitelist = RevList.to_list !report_path_regex_whitelist
@ -3305,8 +3342,6 @@ and scuba_normals = !scuba_normals
and scuba_tags = String.Map.map !scuba_tags ~f:(fun v -> String.split v ~on:',')
and seconds_per_iteration = !seconds_per_iteration
and select =
match !select with
| None ->
@ -3321,8 +3356,6 @@ and select =
and show_buckets = !print_buckets
and print_jbir = !print_jbir
and siof_check_iostreams = !siof_check_iostreams
and siof_safe_methods = RevList.to_list !siof_safe_methods
@ -3388,8 +3421,6 @@ and custom_symbols =
(Yojson.Basic.to_string !custom_symbols)
and symops_per_iteration = !symops_per_iteration
and keep_going = !keep_going
and tenv_json = !tenv_json
@ -3418,10 +3449,6 @@ and trace_events = !trace_events
and trace_ondemand = !trace_ondemand
and trace_join = !trace_join
and trace_rearrange = !trace_rearrange
and trace_topl = !trace_topl
and tv_commit = !tv_commit
@ -3430,20 +3457,10 @@ and tv_limit = !tv_limit
and tv_limit_filtered = !tv_limit_filtered
and type_size = !type_size
and uninit_interproc = !uninit_interproc
and unsafe_malloc = !unsafe_malloc
and incremental_analysis = !incremental_analysis
and worklist_mode = !worklist_mode
and workspace = !workspace
and write_dotty = !write_dotty
and write_html = !write_html
and write_html_whitelist_regex = RevList.to_list !write_html_whitelist_regex

150
infer/src/base/Config.mli
Unescape View File

@ -39,8 +39,6 @@ val anonymous_block_num_sep : string
val anonymous_block_prefix : string
val append_buck_flavors : string list
val assign : string
val biabduction_models_sql : string
@ -51,8 +49,6 @@ val bin_dir : string
val bound_error_allowed_in_procedure_call : bool
val buck_java_flavor_suppress_config : bool
val clang_exe_aliases : string list
val clang_initializer_prefix : string
@ -61,8 +57,6 @@ val clang_inner_destructor_prefix : string
val clang_plugin_path : string
val classpath : string option
val default_failure_name : string
val dotty_frontend_output : string
@ -82,9 +76,9 @@ val ivar_attributes : string
val java_lambda_marker_infix : string
(** marker to recognize methods generated by javalib to eliminate lambdas *)
val lib_dir : string
val kotlin_source_extension : string
val load_average : float option
val lib_dir : string
val max_narrows : int
@ -96,75 +90,76 @@ val nsnotification_center_checker_backend : bool
val os_type : os_type
val passthroughs : bool
val pp_version : Format.formatter -> unit -> unit
val patterns_modeled_expensive : string * Yojson.Basic.t
val property_attributes : string
val patterns_never_returning_null : string * Yojson.Basic.t
val report_nullable_inconsistency : bool
val patterns_skip_implementation : string * Yojson.Basic.t
val save_compact_summaries : bool
val patterns_skip_translation : string * Yojson.Basic.t
val smt_output : bool
val pp_version : Format.formatter -> unit -> unit
val source_file_extentions : string list
val property_attributes : string
val unsafe_unret : string
val relative_path_backtrack : int
val weak : string
val report : bool
val whitelisted_cpp_classes : string list
val report_custom_error : bool
val whitelisted_cpp_methods : string list
val report_force_relative_path : bool
val wrappers_dir : string
val report_immutable_modifications : bool
(** {2 Configuration values specified by command-line options} *)
val report_nullable_inconsistency : bool
val annotation_reachability_cxx : Yojson.Basic.t
val save_compact_summaries : bool
val annotation_reachability_cxx_sources : Yojson.Basic.t
val smt_output : bool
val annotation_reachability_custom_pairs : Yojson.Basic.t
val source_file_extentions : string list
val append_buck_flavors : string list
val kotlin_source_extension : string
val biabduction_abs_struct : int
val sourcepath : string option
val biabduction_abs_val : int
val sources : string list
val biabduction_allow_leak : bool
val trace_absarray : bool
val biabduction_array_level : int
val unsafe_unret : string
val biabduction_models_mode : bool
val incremental_analysis : bool
val biabduction_iterations : int
val weak : string
val biabduction_join_cond : int
val whitelisted_cpp_classes : string list
val biabduction_memleak_buckets :
[`MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown] list
val whitelisted_cpp_methods : string list
val biabduction_monitor_prop_size : bool
val wrappers_dir : string
val biabduction_nelseg : bool
(** {2 Configuration values specified by command-line options} *)
val biabduction_only_footprint : bool
val abs_struct : int
val biabduction_seconds_per_iteration : float option
val abs_val : int
val biabduction_symops_per_iteration : int option
val allow_leak : bool
val biabduction_trace_join : bool
val annotation_reachability_cxx : Yojson.Basic.t
val biabduction_trace_rearrange : bool
val annotation_reachability_cxx_sources : Yojson.Basic.t
val biabduction_type_size : bool
val annotation_reachability_custom_pairs : Yojson.Basic.t
val biabduction_unsafe_malloc : bool
val array_level : int
val biabduction_worklist_mode : int
val biabduction_models_mode : bool
val biabduction_write_dotty : bool
val bo_debug : int
@ -182,6 +177,8 @@ val buck_build_args_no_inline : string list
val buck_cache_mode : bool
val buck_java_flavor_suppress_config : bool
val buck_java_heap_size_gb : int option
val buck_merge_all_deps : bool
@ -198,10 +195,10 @@ val capture : bool
val capture_blacklist : string option
val cfg_json : string option
val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
val cfg_json : string option
val changed_files_index : string option
val check_version : string option
@ -216,6 +213,8 @@ val clang_blacklisted_flags : string list
val clang_blacklisted_flags_with_arg : string list
val clang_frontend_action_string : string
val clang_ignore_regex : string option
val clang_isystem_to_override_regex : Str.regexp option
@ -224,6 +223,8 @@ val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val classpath : string option
val command : InferCommand.t
val config_impact_current : string option
@ -338,6 +339,10 @@ val global_tenv : bool
val icfg_dotty_outfile : string option
val impurity_report_immutable_modifications : bool
val incremental_analysis : bool
val infer_is_clang : bool
val infer_is_javac : bool
@ -356,8 +361,6 @@ val issues_tests : string option
val issues_tests_fields : IssuesTestField.t list
val iterations : int
val java_debug_source_file_info : string option
val java_jar_compiler : string option
@ -372,8 +375,6 @@ val job_id : string option
val jobs : int
val join_cond : int
val keep_going : bool
val linter : string option
@ -396,6 +397,8 @@ val liveness_dangerous_classes : Yojson.Basic.t
val liveness_ignored_constant : string list
val load_average : float option
val max_nesting : int option
val memtrace_analysis : bool
@ -406,15 +409,8 @@ val merge : bool
val method_decls_info : string option
val ml_buckets :
[`MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown] list
val modified_lines : string option
val monitor_prop_size : bool
val nelseg : bool
val no_translate_libs : bool
val nullable_annotation : string option
@ -435,7 +431,13 @@ val oom_threshold : int option
val only_cheap_debug : bool
val only_footprint : bool
val patterns_modeled_expensive : string * Yojson.Basic.t
val patterns_never_returning_null : string * Yojson.Basic.t
val patterns_skip_implementation : string * Yojson.Basic.t
val patterns_skip_translation : string * Yojson.Basic.t
val pmd_xml : bool
@ -471,8 +473,6 @@ val procedures_summary_json : bool
val process_clang_ast : bool
val clang_frontend_action_string : string
val profiler_samples : string option
val progress_bar : [`MultiLine | `Plain | `Quiet]
@ -519,6 +519,8 @@ val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
val quandary_show_passthroughs : bool
val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
@ -531,12 +533,20 @@ val reactive_mode : bool
val reanalyze : bool
val relative_path_backtrack : int
val report : bool
val report_blacklist_files_containing : string list
val report_console_limit : int option
val report_current : string option
val report_custom_error : bool
val report_force_relative_path : bool
val report_formatter : [`No_formatter | `Phabricator_formatter]
val report_path_regex_blacklist : string list
@ -561,8 +571,6 @@ val scuba_normals : string String.Map.t
val scuba_tags : string list String.Map.t
val seconds_per_iteration : float option
val select : [`All | `Select of int] option
val show_buckets : bool
@ -595,6 +603,10 @@ val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
@ -615,8 +627,6 @@ val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val symops_per_iteration : int option
val tenv_json : string option
val test_determinator : bool
@ -635,16 +645,14 @@ val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_join : bool
val trace_ondemand : bool
val trace_rearrange : bool
val trace_topl : bool
val tv_commit : string option
@ -653,18 +661,10 @@ val tv_limit : int
val tv_limit_filtered : int
val type_size : bool
val uninit_interproc : bool
val unsafe_malloc : bool
val worklist_mode : int
val workspace : string option
val write_dotty : bool
val write_html : bool
val write_html_whitelist_regex : string list

7
infer/src/base/SymOp.ml
Unescape View File

@ -57,12 +57,15 @@ let pp_failure_kind fmt = function
(** Timeout in seconds for each function *)
let timeout_seconds =
ref
(Option.map Config.seconds_per_iteration ~f:(fun sec -> sec *. float_of_int Config.iterations))
(Option.map Config.biabduction_seconds_per_iteration ~f:(fun sec ->
sec *. float_of_int Config.biabduction_iterations ))
(** Timeout in SymOps *)
let timeout_symops =
ref (Option.map Config.symops_per_iteration ~f:(fun symops -> symops * Config.iterations))
ref
(Option.map Config.biabduction_symops_per_iteration ~f:(fun symops ->
symops * Config.biabduction_iterations ))
let get_timeout_seconds () = !timeout_seconds

4
infer/src/biabduction/Abs.ml
Unescape View File

@ -242,7 +242,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
let mk_rules_for_sll tenv (para : Predicates.hpara) : rule list =
if not Config.nelseg then
if not Config.biabduction_nelseg then
let pts_pts = mk_rule_ptspts_ls tenv true true para in
let pts_pels = mk_rule_ptsls_ls tenv Lseg_PE true false para in
let pels_pts = mk_rule_lspts_ls tenv Lseg_PE false true para in
@ -450,7 +450,7 @@ let mk_rule_dlldll_dll tenv k1 k2 impl_ok1 impl_ok2 para =
let mk_rules_for_dll tenv (para : Predicates.hpara_dll) : rule list =
if not Config.nelseg then
if not Config.biabduction_nelseg then
let pts_pts = mk_rule_ptspts_dll tenv true true para in
let pts_pedll = mk_rule_ptsdll_dll tenv Lseg_PE true false para in
let pedll_pts = mk_rule_dllpts_dll tenv Lseg_PE false true para in

6
infer/src/biabduction/BiabductionConfig.ml
Unescape View File

@ -27,10 +27,10 @@ let run_in_footprint_mode f x = set_reference_and_call_function footprint true f
let run_in_re_execution_mode f x = set_reference_and_call_function footprint false f x
let abs_val = ref Config.abs_val
let abs_val = ref Config.biabduction_abs_val
let reset_abs_val () = abs_val := Config.abs_val
let reset_abs_val () = abs_val := Config.biabduction_abs_val
let run_with_abs_val_equal_zero f x = set_reference_and_call_function abs_val 0 f x
let allow_leak = ref Config.allow_leak
let allow_leak = ref Config.biabduction_allow_leak

5
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -475,7 +475,7 @@ let execute_free_nonzero_ mk ?(mark_as_freed = true)
in
List.rev prop_list
with Rearrange.ARRAY_ACCESS ->
if Int.equal Config.array_level 0 then assert false
if Int.equal Config.biabduction_array_level 0 then assert false
else (
L.d_strln ".... Array containing allocated heap cells ...." ;
L.d_str " Instr: " ;
@ -949,7 +949,8 @@ let fscanf = Builtin.register BuiltinDecl.fscanf (execute_scan_function 2)
let fwscanf = Builtin.register BuiltinDecl.fwscanf (execute_scan_function 2)
let malloc =
Builtin.register BuiltinDecl.malloc (execute_alloc PredSymb.Mmalloc (not Config.unsafe_malloc))
Builtin.register BuiltinDecl.malloc
(execute_alloc PredSymb.Mmalloc (not Config.biabduction_unsafe_malloc))
let malloc_no_fail =

20
infer/src/biabduction/Dom.ml
Unescape View File

@ -263,7 +263,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct
| Exp.Var id when Ident.is_normal id ->
List.length es >= 1
| Exp.Var _ ->
if Int.equal Config.join_cond 0 then List.exists ~f:(Exp.equal Exp.zero) es
if Int.equal Config.biabduction_join_cond 0 then List.exists ~f:(Exp.equal Exp.zero) es
else if Dangling.check side e then (
let r = List.exists ~f:(fun e' -> not (Dangling.check side_op e')) es in
if r then (
@ -779,7 +779,7 @@ end = struct
let get_other_atoms tenv side atom_in =
let build_other_atoms construct side e =
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "build_other_atoms: " ;
Exp.d_exp e ;
L.d_ln () ) ;
@ -791,7 +791,7 @@ end = struct
| Some (e_res, e_op) ->
let a_res = construct e_res in
let a_op = construct e_op in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "build_other_atoms (successful) " ;
Predicates.d_atom a_res ;
L.d_str ", " ;
@ -1618,7 +1618,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
try
let todo_curr = Todo.pop () in
let e1, e2, e = todo_curr in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_strln ".... sigma_partial_join' ...." ;
L.d_str "TODO: " ;
Exp.d_exp e1 ;
@ -1641,7 +1641,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
sigma_partial_join' tenv mode sigma_acc sigma1 sigma2
| Some (Predicates.Hlseg (k, _, _, _, _) as lseg), None
| Some (Predicates.Hdllseg (k, _, _, _, _, _, _) as lseg), None ->
if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
if (not Config.biabduction_nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else (
@ -1649,7 +1649,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
raise Predicates.JoinFail )
| None, Some (Predicates.Hlseg (k, _, _, _, _) as lseg)
| None, Some (Predicates.Hdllseg (k, _, _, _, _, _, _) as lseg) ->
if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
if (not Config.biabduction_nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else (
@ -1899,7 +1899,7 @@ let pi_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Pr
| Some a' ->
a' :: atom_list
in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "pi1: " ;
Prop.d_pi pi1 ;
L.d_ln () ;
@ -1910,7 +1910,7 @@ let pi_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Pr
let p2 = Prop.normalize tenv ep2 in
List.fold ~f:(handle_atom_with_widening Lhs p2 pi2) ~init:[] pi1
in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "atom_list1: " ;
Prop.d_pi atom_list1 ;
L.d_ln () ) ;
@ -1918,12 +1918,12 @@ let pi_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Pr
let p1 = Prop.normalize tenv ep1 in
List.fold ~f:(handle_atom_with_widening Rhs p1 pi1) ~init:[] pi2
in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "atom_list2: " ;
Prop.d_pi atom_list2 ;
L.d_ln () ) ;
let atom_list_combined = IList.inter ~cmp:Predicates.compare_atom atom_list1 atom_list2 in
if Config.trace_join then (
if Config.biabduction_trace_join then (
L.d_str "atom_list_combined: " ;
Prop.d_pi atom_list_combined ;
L.d_ln () ) ;

4
infer/src/biabduction/Match.ml
Unescape View File

@ -125,7 +125,7 @@ and fsel_match fsel1 sub vars fsel2 =
| [], _ ->
None
| _, [] ->
if Config.abs_struct <= 0 then None
if Config.biabduction_abs_struct <= 0 then None
else Some (sub, vars) (* This can lead to great information loss *)
| (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' ->
let n = Fieldname.compare fld1 fld2 in
@ -135,7 +135,7 @@ and fsel_match fsel1 sub vars fsel2 =
None
| Some (sub', vars') ->
fsel_match fsel1' sub' vars' fsel2'
else if n < 0 && Config.abs_struct > 0 then fsel_match fsel1' sub vars fsel2
else if n < 0 && Config.biabduction_abs_struct > 0 then fsel_match fsel1' sub vars fsel2
(* This can lead to great information loss *)
else None

2
infer/src/biabduction/Predicates.ml
Unescape View File

@ -1195,7 +1195,7 @@ let exp_add_offsets exp offsets =
(** Convert all the lseg's in sigma to nonempty lsegs. *)
let sigma_to_sigma_ne sigma : (atom list * hpred list) list =
if Config.nelseg then
if Config.biabduction_nelseg then
let f eqs_sigma_list hpred =
match hpred with
| Hpointsto _ | Hlseg (Lseg_NE, _, _, _, _) | Hdllseg (Lseg_NE, _, _, _, _, _, _) ->

3
infer/src/biabduction/Prover.ml
Unescape View File

@ -1884,7 +1884,8 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
of length given by its type only active in type_size mode *)
let sexp_imply_preprocess se1 texp1 se2 =
match (se1, texp1, se2) with
| Predicates.Eexp (_, inst), Exp.Sizeof _, Predicates.Earray _ when Config.type_size ->
| Predicates.Eexp (_, inst), Exp.Sizeof _, Predicates.Earray _ when Config.biabduction_type_size
->
let se1' = Predicates.Earray (texp1, [(Exp.zero, se1)], inst) in
L.d_strln ~color:Orange "sexp_imply_preprocess" ;
L.d_str " se1: " ;

41
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -68,7 +68,7 @@ let check_bad_index {InterproceduralAnalysis.proc_desc; err_log; tenv} pname p l
(** Perform bounds checking *)
let bounds_check analysis_data pname prop len e =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_str "Bounds check index:" ;
Exp.d_exp e ;
L.d_str " len: " ;
@ -80,7 +80,7 @@ let bounds_check analysis_data pname prop len e =
let rec create_struct_values analysis_data pname tenv orig_prop footprint_part kind max_stamp
(t : Typ.t) (off : Predicates.offset list) inst :
Predicates.atom list * Predicates.strexp * Typ.t =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_increase_indent () ;
L.d_strln "entering create_struct_values" ;
L.d_str "typ: " ;
@ -181,7 +181,7 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k
| Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun, _ | Tptr _, _ | TVar _, _ ->
fail t off __POS__
in
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
let _, se, _ = res in
L.d_strln "exiting create_struct_values, returning" ;
Predicates.d_sexp se ;
@ -271,7 +271,7 @@ let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part
| Predicates.Eexp (_, Predicates.Ialloc) ->
Exp.one (* if allocated explicitly, we know len is 1 *)
| _ ->
if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *)
if Config.biabduction_type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *)
else Exp.Var (new_id ())
in
let se_new = Predicates.Earray (len, [(Exp.zero, se)], inst) in
@ -415,7 +415,7 @@ let strexp_extend_values analysis_data pname tenv orig_prop footprint_part kind
if footprint_part then (off', List.map ~f:(fun (id, e) -> Prop.mk_eq tenv (Exp.Var id) e) eqs)
else (off, [])
in
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_str "entering strexp_extend_values se: " ;
Predicates.d_sexp se ;
L.d_str " typ: " ;
@ -432,7 +432,7 @@ let strexp_extend_values analysis_data pname tenv orig_prop footprint_part kind
let check_not_inconsistent (atoms, _, _) = not (List.exists ~f:check_neg_atom atoms) in
List.filter ~f:check_not_inconsistent atoms_se_typ_list
in
if Config.trace_rearrange then L.d_strln "exiting strexp_extend_values" ;
if Config.biabduction_trace_rearrange then L.d_strln "exiting strexp_extend_values" ;
let sizeof_data =
match te with
| Exp.Sizeof sizeof_data ->
@ -545,7 +545,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
fields to follow the path in [lexp] -- field splitting model. It also materializes all indices
accessed in lexp. *)
let prop_iter_extend_ptsto analysis_data pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_str "entering prop_iter_extend_ptsto lexp: " ;
Exp.d_exp lexp ;
L.d_ln () ) ;
@ -593,7 +593,7 @@ let prop_iter_extend_ptsto analysis_data pname tenv orig_prop iter lexp inst =
Prop.prop_iter_update_current iter' (Predicates.Hpointsto (e, se, te))
in
let do_extend e se te =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_strln "entering do_extend" ;
L.d_str "e: " ;
Exp.d_exp e ;
@ -725,7 +725,7 @@ let prop_iter_add_hpred_footprint_to_prop analysis_data pname tenv prop (lexp, t
with the allowed footprint variables. This function ensures that [root(lexp): typ] is the
current hpred of the iterator. typ is the type of the root of lexp. *)
let prop_iter_add_hpred_footprint analysis_data pname tenv orig_prop iter (lexp, typ) inst =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_strln "entering prop_iter_add_hpred_footprint" ;
L.d_str "lexp: " ;
Exp.d_exp lexp ;
@ -754,7 +754,7 @@ let prop_iter_add_hpred_footprint analysis_data pname tenv orig_prop iter (lexp,
exception ARRAY_ACCESS
let rearrange_arith tenv lexp prop =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_strln "entering rearrange_arith" ;
L.d_str "lexp: " ;
Exp.d_exp lexp ;
@ -764,7 +764,7 @@ let rearrange_arith tenv lexp prop =
Prop.d_prop prop ;
L.d_ln () ;
L.d_ln () ) ;
if Config.array_level >= 2 then raise ARRAY_ACCESS
if Config.biabduction_array_level >= 2 then raise ARRAY_ACCESS
else
let root = Exp.root_of_lexp lexp in
if Prover.check_allocatedness tenv prop root then raise ARRAY_ACCESS
@ -785,7 +785,7 @@ let pp_rearrangement_error message prop lexp =
(** do re-arrangement for an iter whose current element is a pointsto *)
let iter_rearrange_ptsto analysis_data pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_increase_indent () ;
L.d_strln "entering iter_rearrange_ptsto" ;
L.d_str "lexp: " ;
@ -832,7 +832,7 @@ let iter_rearrange_ptsto analysis_data pname tenv orig_prop iter lexp inst =
| _ ->
[iter] )
in
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_strln "exiting iter_rearrange_ptsto, returning results" ;
Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ;
L.d_decrease_indent () ;
@ -843,7 +843,7 @@ let iter_rearrange_ptsto analysis_data pname tenv orig_prop iter lexp inst =
(** do re-arrangment for an iter whose current element is a nonempty listseg *)
let iter_rearrange_ne_lseg tenv recurse_on_iters iter para e1 e2 elist =
if Config.nelseg then
if Config.biabduction_nelseg then
let iter_inductive_case =
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let _, para_inst1 = Predicates.hpara_instantiate para e1 n' elist in
@ -984,7 +984,7 @@ let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter in
match fld_typ.desc with
| Tstruct _ ->
(* access through field: get the struct type from the field *)
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_increase_indent () ;
L.d_printfln "iter_rearrange: root of lexp accesses field %a" Fieldname.pp f ;
L.d_str " struct type from field: " ;
@ -1001,7 +1001,7 @@ let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter in
typ_from_instr
in
let typ = root_typ_of_offsets (Predicates.exp_get_offsets lexp) in
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_increase_indent () ;
L.d_strln "entering iter_rearrange" ;
L.d_str "lexp: " ;
@ -1021,10 +1021,13 @@ let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter in
L.d_ln () ;
L.d_ln () ) ;
let default_case_iter (iter' : unit Prop.prop_iter) =
if Config.trace_rearrange then L.d_strln "entering default_case_iter" ;
if Config.biabduction_trace_rearrange then L.d_strln "entering default_case_iter" ;
if !BiabductionConfig.footprint then
prop_iter_add_hpred_footprint analysis_data pname tenv prop iter' (lexp, typ) inst
else if Config.array_level >= 1 && (not !BiabductionConfig.footprint) && Exp.pointer_arith lexp
else if
Config.biabduction_array_level >= 1
&& (not !BiabductionConfig.footprint)
&& Exp.pointer_arith lexp
then rearrange_arith tenv lexp prop
else (
pp_rearrangement_error "cannot find predicate with root" prop lexp ;
@ -1090,7 +1093,7 @@ let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter in
iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter para_dll e1
e2 e3 e4 elist ) )
in
if Config.trace_rearrange then (
if Config.biabduction_trace_rearrange then (
L.d_strln "exiting iter_rearrange, returning results" ;
Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ;
L.d_decrease_indent () ;

5
infer/src/biabduction/SymExec.ml
Unescape View File

@ -931,7 +931,7 @@ let execute_load ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv; _
let undef = Exp.get_undefined !BiabductionConfig.footprint in
[Prop.conjoin_eq tenv (Exp.Var id) undef prop] )
with Rearrange.ARRAY_ACCESS ->
if Int.equal Config.array_level 0 then assert false
if Int.equal Config.biabduction_array_level 0 then assert false
else
let undef = Exp.get_undefined false in
[Prop.conjoin_eq tenv (Exp.Var id) undef prop_]
@ -983,7 +983,8 @@ let execute_store ?(report_deref_errors = true) ({InterproceduralAnalysis.tenv;
List.rev (List.fold ~f:(execute_store_ analysis_data tenv n_rhs_exp) ~init:[] iter_list)
in
prop_list
with Rearrange.ARRAY_ACCESS -> if Int.equal Config.array_level 0 then assert false else [prop_]
with Rearrange.ARRAY_ACCESS ->
if Int.equal Config.biabduction_array_level 0 then assert false else [prop_]
let is_variadic_procname callee_pname =

8
infer/src/biabduction/interproc.ml
Unescape View File

@ -51,7 +51,7 @@ module NodeVisitSet = Caml.Set.Make (struct
let compare x1 x2 =
if !BiabductionConfig.footprint then
match Config.worklist_mode with
match Config.biabduction_worklist_mode with
| 0 ->
compare_ids x1.node x2.node
| 1 ->
@ -342,7 +342,7 @@ let check_prop_size_ p _ =
(* Check prop size and filter out possible unabstracted lists *)
let check_prop_size edgeset_todo =
if Config.monitor_prop_size then Paths.PathSet.iter check_prop_size_ edgeset_todo
if Config.biabduction_monitor_prop_size then Paths.PathSet.iter check_prop_size_ edgeset_todo
let reset_prop_metrics () =
@ -819,7 +819,7 @@ let perform_analysis_phase ({InterproceduralAnalysis.proc_desc; err_log; tenv} a
DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source)
[Procname.to_filename pname]
in
if Config.write_dotty then DotBiabduction.emit_specs_to_file filename specs ;
if Config.biabduction_write_dotty then DotBiabduction.emit_specs_to_file filename specs ;
(specs, BiabductionSummary.RE_EXECUTION)
in
(go, get_results)
@ -1015,7 +1015,7 @@ let analyze_proc analysis_data summary_opt proc_cfg : BiabductionSummary.t =
(** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
let transition_footprint_re_exe summary tenv joined_pres : BiabductionSummary.t =
if Config.only_footprint then
if Config.biabduction_only_footprint then
if BiabductionSummary.equal_phase summary.BiabductionSummary.phase FOOTPRINT then
{summary with BiabductionSummary.phase= RE_EXECUTION}
else summary

2
infer/src/checkers/impurity.ml
Unescape View File

@ -256,6 +256,6 @@ let checker {IntraproceduralAnalysis.proc_desc; tenv; err_log}
ImpurityDomain.join acc impurity_astate )
in
if PurityChecker.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then (
if Config.report_immutable_modifications then
if Config.impurity_report_immutable_modifications then
report_immutable_field_modifications tenv impurity_astate proc_desc err_log ;
report_impure_all proc_desc err_log impurity_astate )

5
infer/tests/codetoanalyze/cpp/biabduction/Makefile
Unescape View File

@ -7,8 +7,9 @@ TESTS_DIR = ../../..
# use our own clang's standard library so that the tests are uniform across distributions
CLANG_OPTIONS = -x c++ -std=c++1y -isystem$(ROOT_DIR) -c --stdlib=libc++
INFER_OPTIONS = --biabduction-only --ml-buckets cpp --debug-exceptions --project-root $(TESTS_DIR) \
--report-custom-error
INFER_OPTIONS = \
--biabduction-only --biabduction-memleak-buckets cpp --debug-exceptions --report-custom-error \
--project-root $(TESTS_DIR)
INFERPRINT_OPTIONS = --issues-tests
SOURCES = \

5
infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile
Unescape View File

@ -7,8 +7,9 @@ TESTS_DIR = ../../..
# see explanations in cpp/biabduction/Makefile for the custom isystem
CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --bufferoverrun-only --ml-buckets cpp --no-filtering --debug-exceptions \
--project-root $(TESTS_DIR) --report-force-relative-path
INFER_OPTIONS = \
--bufferoverrun-only --no-filtering --debug-exceptions --project-root $(TESTS_DIR) \
--report-force-relative-path
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.cpp)

2
infer/tests/codetoanalyze/cpp/liveness/Makefile
Unescape View File

@ -7,7 +7,7 @@ TESTS_DIR = ../../..
# see explanations in cpp/biabduction/Makefile for the custom isystem
CLANG_OPTIONS = -x c++ -std=c++14 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --liveness-only --ml-buckets cpp --debug-exceptions --project-root $(TESTS_DIR)
INFER_OPTIONS = --liveness-only --debug-exceptions --project-root $(TESTS_DIR)
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.cpp)

2
infer/tests/codetoanalyze/cpp/performance/Makefile
Unescape View File

@ -7,7 +7,7 @@ TESTS_DIR = ../../..
# see explanations in cpp/biabduction/Makefile for the custom isystem
CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --cost-only --ml-buckets cpp --no-filtering --debug-exceptions \
INFER_OPTIONS = --cost-only --no-filtering --debug-exceptions \
--project-root $(TESTS_DIR) --report-force-relative-path --debug \
--no-cost-suppress-func-ptr
INFERPRINT_OPTIONS = --issues-tests

2
infer/tests/codetoanalyze/cpp/quandary/Makefile
Unescape View File

@ -8,7 +8,7 @@ TESTS_DIR = ../../..
# see explanations in cpp/biabduction/Makefile for the custom isystem
CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(ROOT_DIR) -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --function-pointer-specialization \
--quandary-only --passthroughs --debug-exceptions \
--quandary-only --quandary-show-passthroughs --debug-exceptions \
--project-root $(TESTS_DIR) \
INFERPRINT_OPTIONS = --issues-tests

6
infer/tests/codetoanalyze/java/fb-immutability/Makefile
Unescape View File

@ -6,8 +6,10 @@
TESTS_DIR = ../../..
ANALYZER = checkers
INFER_OPTIONS = --impurity-only --report-immutable-modifications --disable-issue-type IMPURE_FUNCTION \
--disable-issue-type NULLPTR_DEREFERENCE --report-force-relative-path
INFER_OPTIONS = \
--impurity-only --impurity-report-immutable-modifications --report-force-relative-path \
--disable-issue-type IMPURE_FUNCTION \
--disable-issue-type NULLPTR_DEREFERENCE
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java)

2
infer/tests/codetoanalyze/java/immutability/Makefile
Unescape View File

@ -6,7 +6,7 @@
TESTS_DIR = ../../..
ANALYZER = checkers
INFER_OPTIONS = --impurity-only --report-immutable-modifications --disable-issue-type IMPURE_FUNCTION
INFER_OPTIONS = --impurity-only --impurity-report-immutable-modifications --disable-issue-type IMPURE_FUNCTION
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java)

2
infer/tests/codetoanalyze/java/quandary/Makefile
Unescape View File

@ -5,7 +5,7 @@
TESTS_DIR = ../../..
INFER_OPTIONS = --quandary-only --passthroughs --debug-exceptions
INFER_OPTIONS = --quandary-only --quandary-show-passthroughs --debug-exceptions
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java)

6
infer/tests/codetoanalyze/objc/biabduction/Makefile
Unescape View File

@ -123,17 +123,17 @@ $(OBJECTS_BASE) $(OBJECTS_BUCKETS_ALL): $(SOURCES_BASE) $(SOURCES_BUCKET_ALL)
infer-out-all/report.json: $(CLANG_DEPS) $(SOURCES_BUCKET_ALL)
$(QUIET)$(call silent_on_success,Testing infer/Objective-C with all memleak buckets,\
$(INFER_BIN) $(INFER_OPTIONS) --ml-buckets all -o infer-out-all -- \
$(INFER_BIN) $(INFER_OPTIONS) --biabduction-memleak-buckets all -o infer-out-all -- \
clang $(CLANG_OPTIONS) $(SOURCES_BUCKET_ALL))
infer-out-arc/report.json: $(CLANG_DEPS) $(SOURCES_ARC)
$(QUIET)$(call silent_on_success,Testing infer/Objective-C with arc memleak buckets,\
$(INFER_BIN) $(INFER_OPTIONS) --ml-buckets cf -o infer-out-arc -- \
$(INFER_BIN) $(INFER_OPTIONS) --biabduction-memleak-buckets cf -o infer-out-arc -- \
clang $(CLANG_OPTIONS) -fobjc-arc $(SOURCES_ARC))
infer-out/report.json: $(CLANG_DEPS) $(SOURCES_DEFAULT)
$(QUIET)$(call silent_on_success,Testing infer/Objective-C with CF memleak buckets,\
$(INFER_BIN) $(INFER_OPTIONS) --ml-buckets cf -o infer-out -- \
$(INFER_BIN) $(INFER_OPTIONS) --biabduction-memleak-buckets cf -o infer-out -- \
clang $(CLANG_OPTIONS) $(SOURCES_DEFAULT))
issues.exp.test: infer-out-all/report.json infer-out-arc/report.json infer-out/report.json

Write Preview
Loading…
Cancel
Save