diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 17fcb676c..2eb933640 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -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) 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 diff --git a/infer/man/man1/infer-capture.txt b/infer/man/man1/infer-capture.txt index 8faa80528..f6264d9da 100644 --- a/infer/man/man1/infer-capture.txt +++ b/infer/man/man1/infer-capture.txt @@ -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, diff --git a/infer/man/man1/infer-compile.txt b/infer/man/man1/infer-compile.txt index 956f6f8e7..b39a2e6cc 100644 --- a/infer/man/man1/infer-compile.txt +++ b/infer/man/man1/infer-compile.txt @@ -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, diff --git a/infer/man/man1/infer-explore.txt b/infer/man/man1/infer-explore.txt index 1e5495e7a..f2f84ce21 100644 --- a/infer/man/man1/infer-explore.txt +++ b/infer/man/man1/infer-explore.txt @@ -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 diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 16c14e5d6..e36b7f5b8 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -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 =(,,|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. diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 7e8293069..851b6889d 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -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 diff --git a/infer/man/man1/infer-reportdiff.txt b/infer/man/man1/infer-reportdiff.txt index ce135b86f..7160141dc 100644 --- a/infer/man/man1/infer-reportdiff.txt +++ b/infer/man/man1/infer-reportdiff.txt @@ -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, diff --git a/infer/man/man1/infer-run.txt b/infer/man/man1/infer-run.txt index 8a8c46e02..6a68e9e45 100644 --- a/infer/man/man1/infer-run.txt +++ b/infer/man/man1/infer-run.txt @@ -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 diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 37b8c4338..7ae210822 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -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 diff --git a/infer/src/absint/Mleak_buckets.ml b/infer/src/absint/Mleak_buckets.ml index f41087562..35c9aabc5 100644 --- a/infer/src/absint/Mleak_buckets.ml +++ b/infer/src/absint/Mleak_buckets.ml @@ -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 diff --git a/infer/src/absint/TaintTrace.ml b/infer/src/absint/TaintTrace.ml index 173efbb79..afe934ddd 100644 --- a/infer/src/absint/TaintTrace.ml +++ b/infer/src/absint/TaintTrace.ml @@ -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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 99c90e8b5..fc458d5f4 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -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 = =(,,|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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index b860d7381..1d1a51666 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -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 diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index 5171e2b21..11e85249d 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -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 diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index 6061ef2f6..6a49e4cd2 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -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 diff --git a/infer/src/biabduction/BiabductionConfig.ml b/infer/src/biabduction/BiabductionConfig.ml index 0f38b64bf..ef0bf3683 100644 --- a/infer/src/biabduction/BiabductionConfig.ml +++ b/infer/src/biabduction/BiabductionConfig.ml @@ -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 diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 4f450b0da..c31ccd971 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -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 = diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index d357bc3f5..8c8f123a7 100644 --- a/infer/src/biabduction/Dom.ml +++ b/infer/src/biabduction/Dom.ml @@ -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 () ) ; diff --git a/infer/src/biabduction/Match.ml b/infer/src/biabduction/Match.ml index 14c5fc790..e5f950a3f 100644 --- a/infer/src/biabduction/Match.ml +++ b/infer/src/biabduction/Match.ml @@ -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 diff --git a/infer/src/biabduction/Predicates.ml b/infer/src/biabduction/Predicates.ml index 71bb48237..2d979a4b9 100644 --- a/infer/src/biabduction/Predicates.ml +++ b/infer/src/biabduction/Predicates.ml @@ -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, _, _, _, _, _, _) -> diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 0b64c59f9..310e87639 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -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: " ; diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index a81421212..c097e4626 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -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 () ; diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index b9c9b1307..6d56124e7 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -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 = diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 1c5f9c4db..aee655c8b 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -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 diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 3f2c24849..fac9352f2 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -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 ) diff --git a/infer/tests/codetoanalyze/cpp/biabduction/Makefile b/infer/tests/codetoanalyze/cpp/biabduction/Makefile index ce5dcd8b4..559c881f4 100644 --- a/infer/tests/codetoanalyze/cpp/biabduction/Makefile +++ b/infer/tests/codetoanalyze/cpp/biabduction/Makefile @@ -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 = \ diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile index fb47df690..79e6ad54a 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile @@ -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) diff --git a/infer/tests/codetoanalyze/cpp/liveness/Makefile b/infer/tests/codetoanalyze/cpp/liveness/Makefile index 5ebd2db51..fd102a697 100644 --- a/infer/tests/codetoanalyze/cpp/liveness/Makefile +++ b/infer/tests/codetoanalyze/cpp/liveness/Makefile @@ -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) diff --git a/infer/tests/codetoanalyze/cpp/performance/Makefile b/infer/tests/codetoanalyze/cpp/performance/Makefile index eaf576948..e3a9dac6a 100644 --- a/infer/tests/codetoanalyze/cpp/performance/Makefile +++ b/infer/tests/codetoanalyze/cpp/performance/Makefile @@ -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 diff --git a/infer/tests/codetoanalyze/cpp/quandary/Makefile b/infer/tests/codetoanalyze/cpp/quandary/Makefile index 3677b492f..ce9f9178c 100644 --- a/infer/tests/codetoanalyze/cpp/quandary/Makefile +++ b/infer/tests/codetoanalyze/cpp/quandary/Makefile @@ -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 diff --git a/infer/tests/codetoanalyze/java/fb-immutability/Makefile b/infer/tests/codetoanalyze/java/fb-immutability/Makefile index e73badb3f..53e2b8ae5 100644 --- a/infer/tests/codetoanalyze/java/fb-immutability/Makefile +++ b/infer/tests/codetoanalyze/java/fb-immutability/Makefile @@ -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) diff --git a/infer/tests/codetoanalyze/java/immutability/Makefile b/infer/tests/codetoanalyze/java/immutability/Makefile index 89f5077ad..353073190 100644 --- a/infer/tests/codetoanalyze/java/immutability/Makefile +++ b/infer/tests/codetoanalyze/java/immutability/Makefile @@ -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) diff --git a/infer/tests/codetoanalyze/java/quandary/Makefile b/infer/tests/codetoanalyze/java/quandary/Makefile index fd63d5eca..0a3fbc387 100644 --- a/infer/tests/codetoanalyze/java/quandary/Makefile +++ b/infer/tests/codetoanalyze/java/quandary/Makefile @@ -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) diff --git a/infer/tests/codetoanalyze/objc/biabduction/Makefile b/infer/tests/codetoanalyze/objc/biabduction/Makefile index 237cd6989..bd7a9cc27 100644 --- a/infer/tests/codetoanalyze/objc/biabduction/Makefile +++ b/infer/tests/codetoanalyze/objc/biabduction/Makefile @@ -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