infer-analyze - analyze the files captured by infer
infer
analyze [options]
infer [options]
Analyze the files captured in the project results directory and report.
--annotation-reachability
Activates: annotation-reachability checker: Given pairs of source and sink annotations, e.g. ‘@A‘ and ‘@B‘, this checker will warn whenever some method annotated with ‘@A‘ calls, directly or indirectly, another method annotated with ‘@B‘. Besides the custom pairs, it is also possible to enable some built-in checks, such as ‘@PerformanceCritical‘ reaching ‘@Expensive‘ or ‘@NoAllocation‘ reaching ‘new‘. It is also possible to model methods as if they were annotated, using regular expressions. This should also work in languages where there are no annotations. See flags starting with ‘--annotation-reachability‘. (Conversely: --no-annotation-reachability)
--annotation-reachability-only
Activates: Enable annotation-reachability and disable all other checkers (Conversely: --no-annotation-reachability-only)
--biabduction
Activates: biabduction checker: This analysis deals with a range of issues, many linked to memory safety.
DEPRECATED: This has been
replaced by Pulse and will be removed
in the next release.
(Conversely: --no-biabduction)
--biabduction-only
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: bufferoverrun checker: InferBO is a detector for out-of-bounds array accesses. (Conversely: --no-bufferoverrun)
--bufferoverrun-only
Activates: Enable bufferoverrun and disable all other checkers (Conversely: --no-bufferoverrun-only)
--changed-files-index file
Specify the file containing the list of source files from which reactive analysis should start. Source files should be specified relative to project root or be absolute
--config-impact-analysis
Activates: config-impact-analysis checker: [EXPERIMENTAL] Collects function that are called without config checks. (Conversely: --no-config-impact-analysis)
--config-impact-analysis-only
Activates: Enable config-impact-analysis and disable all other checkers (Conversely: --no-config-impact-analysis-only)
--continue-analysis
Activates: Continue the analysis after more targets are captured by --continue. The other analysis options should be given the same before. Not compatible with --reanalyze and --incremental-analysis. (Conversely: --no-continue-analysis)
--cost
Activates: cost checker: Computes the asymptotic complexity of functions with respect to execution cost or other user defined resources. Can be used to detect changes in the complexity with ‘infer reportdiff‘. (Conversely: --no-cost)
--cost-only
Activates: Enable cost and disable all other checkers (Conversely: --no-cost-only)
--no-cost-suppress-func-ptr
Deactivates: Suppress printing function pointers in cost reports (Conversely: --cost-suppress-func-ptr)
--debug,-g
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-html) (Conversely: --no-debug | -G)
--debug-level level
Debug level (sets --bo-debug level, --debug-level-analysis level, --debug-level-capture level):
- 0: only basic debugging
enabled
- 1: verbose debugging enabled
- 2: very verbose debugging enabled
--debug-level-analysis int
Debug level for the analysis. See --debug-level for accepted values.
--debug-level-capture int
Debug level for the capture. See --debug-level for accepted values.
--debug-level-report int
Debug level for the report. See --debug-level for accepted values.
--no-deduplicate
Deactivates: Apply issue-specific deduplication during analysis and/or reporting. (Conversely: --deduplicate)
--no-default-checkers
Deactivates: Default checkers: --static-constructor-stall-checker, --fragment-retains-view, --inefficient-keyset-iterator, --liveness, --parameter-not-null-checked, --pulse, --racerd, --siof, --self-in-block, --starvation (Conversely: --default-checkers)
--detach-analysis-dependency
Activates: Detach analysis dependencies of checkers during the analysis, so that each checker triggers themselves only when analyzing a callee. This can save unnecessary analyses on the situation that NOT all of the captured data should be analyzed, e.g. --changed-files-index is given. (Conversely: --no-detach-analysis-dependency)
--dict-missing-key-var-block-list +string
Skip analyzing the variables in the dict-missing-key checker.
--files-to-analyze-index file
File containing a list of source files where analysis should start from. When used, the set of files given to this argument must be a subset of that passed to --changed-files-index (which must be specified).
--no-fragment-retains-view
Deactivates: fragment-retains-view checker: Detects when Android fragments are not explicitly nullified before becoming unreachable. (Conversely: --fragment-retains-view)
--fragment-retains-view-only
Activates: Enable fragment-retains-view and disable all other checkers (Conversely: --no-fragment-retains-view-only)
--help
Show this manual
--help-format { auto | groff | pager | plain }
Show this help in the specified format. auto sets the format to plain if the environment variable TERM is "dumb" or undefined, and to pager otherwise.
--help-full
Show this manual with all internal options in the INTERNAL OPTIONS section
--impurity
Activates: impurity checker: Detects functions with potential side-effects. Same as "purity", but implemented on top of Pulse.
ACTIVATES: pulse
(Conversely: --no-impurity)
--impurity-only
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)
--incremental-analysis
Activates: Use incremental analysis for changed files. Not compatible with --reanalyze and --continue-analysis. Also sets --mark-unchanged-procs. (Conversely: --no-incremental-analysis)
--no-inefficient-keyset-iterator
Deactivates: inefficient-keyset-iterator checker: Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly. (Conversely: --inefficient-keyset-iterator)
--inefficient-keyset-iterator-only
Activates: Enable inefficient-keyset-iterator and disable all other checkers (Conversely: --no-inefficient-keyset-iterator-only)
--invalidate-only
Activates: Remove any summaries from the results database that transitively depend on a changed procedure, then exit without doing any actual analysis. (Conversely: --no-invalidate-only)
--jobs,-j int
Run the specified number of analysis jobs simultaneously. Defaults to the minimum value of the max_jobs argument and the number of CPUs.
--keep-going
Activates: Keep going when the analysis or capture encounter a failure (Conversely: --no-keep-going)
--lineage
Activates: lineage checker: Computes a dataflow graph (Conversely: --no-lineage)
--lineage-only
Activates: Enable lineage and disable all other checkers (Conversely: --no-lineage-only)
--litho-required-props
Activates: litho-required-props checker: Checks that all non-optional ‘@Prop‘s have been specified when constructing Litho components. (Conversely: --no-litho-required-props)
--litho-required-props-only
Activates: Enable litho-required-props and disable all other checkers (Conversely: --no-litho-required-props-only)
--no-liveness
Deactivates: liveness checker: Detection of dead stores and unused variables. (Conversely: --liveness)
--liveness-ignored-constant +string
List of integer constants to be ignored by liveness analysis
--liveness-only
Activates: Enable liveness and disable all other checkers (Conversely: --no-liveness-only)
--log-missing-deps
Activates: Log analysis dependencies that cannot be found. (Conversely: --no-log-missing-deps)
--loop-hoisting
Activates: loop-hoisting checker: Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency. (Conversely: --no-loop-hoisting)
--loop-hoisting-only
Activates: Enable loop-hoisting and disable all other checkers (Conversely: --no-loop-hoisting-only)
--max-jobs int
Maximum number of analysis jobs running simultaneously. Experiments show current best value is 40 jobs.
--memtrace-analysis-profiling
Activates: Generate OCaml analysis allocation traces in ‘infer-out/memtrace‘. (Conversely: --no-memtrace-analysis-profiling)
--memtrace-sampling-rate float
Sampling rate for Memtrace allocation profiling. Default is 1e-6.
--modeled-expensive json
Matcher or list of matchers for methods that should be considered expensive by the performance critical checker.
--multicore
Activates: [EXPERIMENTAL] uses multi-threading for analysis, currently partially or not implemented. (Conversely: --no-multicore)
--never-returning-null json
[Java only, all analyses] Matcher or list of matchers for functions that never return null.
--noescaping-function-list +string
Useful for the check CXX_REF_CAPTURED_IN_BLOCK. It declares a list of functions that take blocks as arguments that are no escaping but we cannot annotate them accordingly.
--objc-block-execution-macro string
Macro for executing Objective-C blocks safely.
--ondemand-recursion-restart-limit int
In order to make the analysis of mutual recursion cycles deterministic in their output, the analysis of a cycle of mutually recursive functions may restart the analysis of the entire cycle from a deterministic place. If the graph of mutual recursion is more complex than a simple cycle this could potentially result in many restarts before finding the "right" procedure from which to start. This limits the number of restarts before we give up and analyze the cycle as-is instead.
--no-parameter-not-null-checked
Deactivates: parameter-not-null-checked checker: An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first. (Conversely: --parameter-not-null-checked)
--parameter-not-null-checked-only
Activates: Enable parameter-not-null-checked and disable all other checkers (Conversely: --no-parameter-not-null-checked-only)
--print-active-checkers
Activates: Print the active checkers before starting the analysis (Conversely: --no-print-active-checkers)
--print-logs
Activates: Also log messages to stdout and stderr (Conversely: --no-print-logs)
--procs-to-analyze-index file
Specify the file containing an Sexp representing a list of pairs of procedures and specializations to analyze. Only works with the restart scheduler.
--progress-bar-style { auto | plain | multiline }
Style of the progress bar. auto selects multiline if connected to a tty, otherwise plain.
--project-root,-C dir
Specify the root directory of the project
--no-pulse
Deactivates: pulse checker: General-purpose memory and value analysis engine. (Conversely: --pulse)
--pulse-only
Activates: Enable pulse and disable all other checkers (Conversely: --no-pulse-only)
--purity
Activates: purity checker: Detects pure (side-effect-free) functions. A different implementation of "impurity". (Conversely: --no-purity)
--purity-only
Activates: Enable purity and disable all other checkers (Conversely: --no-purity-only)
--qualified-cpp-name-block-list +string
Skip analyzing the procedures under the qualified cpp type name.
--quiet,-q
Activates: Do not print anything on standard output. (Conversely: --no-quiet | -Q)
--no-racerd
Deactivates: racerd checker: Thread safety analysis. (Conversely: --racerd)
--racerd-only
Activates: Enable racerd and disable all other checkers (Conversely: --no-racerd-only)
--reactive,-r
Activates: Reactive mode: the analysis starts from the files captured since the infer command started (Conversely: --no-reactive | -R)
--reactive-capture
Activates: Reactive capture: capture and analysis are interleaved. Currently this flag will only make the analysis generate a list of type names that were not found in the global tenv. The feature is only available for the Hack frontend for now. (Conversely: --no-reactive-capture)
--no-report
Deactivates: Run the reporting phase once the analysis has completed (Conversely: --report)
--report-force-relative-path
Activates: Force converting an absolute path to a relative path to the root directory (Conversely: --no-report-force-relative-path)
--results-dir,-o dir
Write results and internal files in the specified directory
--scope-leakage
Activates: scope-leakage checker: The Java/Kotlin checker takes into account a set of "scope" annotations and a must-not-hold relation over the scopes. The checker raises an alarm if there exists a field access path from object A to object B, with respective scopes SA and SB, such that must-not-hold(SA, SB). (Conversely: --no-scope-leakage)
--scope-leakage-only
Activates: Enable scope-leakage and disable all other checkers (Conversely: --no-scope-leakage-only)
--no-self-in-block
Deactivates: self-in-block checker: An Objective-C-specific analysis to detect when a block captures ‘self‘. (Conversely: --self-in-block)
--self-in-block-only
Activates: Enable self-in-block and disable all other checkers (Conversely: --no-self-in-block-only)
--shrink-analysis-db
Activates: After analysis, delete analysis summaries (but not report summaries) and vacuum analysis database. (Conversely: --no-shrink-analysis-db)
--sil-validation
Activates: sil-validation checker: This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL. (Conversely: --no-sil-validation)
--sil-validation-only
Activates: Enable sil-validation and disable all other checkers (Conversely: --no-sil-validation-only)
--no-siof
Deactivates: siof checker: Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors. (Conversely: --siof)
--siof-only
Activates: Enable siof and disable all other checkers (Conversely: --no-siof-only)
--sqlite-cache-size int
SQLite cache size in pages (if positive) or kB (if negative), follows formal of corresponding SQLite PRAGMA.
--sqlite-lock-timeout int
Timeout for SQLite results database operations, in milliseconds.
--sqlite-max-blob-size int
Maximum blob/string size for data written in SQLite.
--sqlite-mmap-size int
Size of memory map for mmaped SQLite databases, zero value disables memory mapping.
--sqlite-page-size int
SQLite page size in bytes, must be a power of two between 512 and 65536.
--no-starvation
Deactivates: starvation checker: Detect various kinds of situations when no progress is being made because of concurrency errors. (Conversely: --starvation)
--starvation-only
Activates: Enable starvation and disable all other checkers (Conversely: --no-starvation-only)
--no-static-constructor-stall-checker
Deactivates: static-constructor-stall-checker checker: Detect if dispatch_once is called from a static constructor. (Conversely: --static-constructor-stall-checker)
--static-constructor-stall-checker-only
Activates: Enable static-constructor-stall-checker and disable all other checkers (Conversely: --no-static-constructor-stall-checker-only)
--timeout float
Time after which any checker (except biabduction) should give up analysing the current function or method, in seconds
--top-longest-proc-duration-size int
Number of procedures for which we track longest analysis duration info.
--topl
Activates: topl checker: Detect errors based on user-provided state machines describing temporal properties over multiple objects.
ACTIVATES: pulse
(Conversely: --no-topl)
--topl-only
Activates: Enable topl and disable all other checkers (Conversely: --no-topl-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
--analysis-schedule-file path
The file where an analysis schedule is stored. The default is infer-out/analysis_dependency_graph
--replay-analysis-schedule
Activates: Replay the analysis schedule stored in --replay-analysis-schedule-file, which should analyze the procedures in the same order as the previous analysis. This should drastically limit non-determinism in the results, as well as prevent repeated work, leading to a faster second analysis. Only works if a previous analysis has just run on the same code. (Conversely: --no-replay-analysis-schedule)
--replay-ondemand-should-error
Activates: [debug] Whether triggering the analysis of a procedure via ondemand should log an error when replaying an analysis schedule with --replay-analysis-schedule. Enable when replaying the same analysis on the same capture data to debug cases where dependencies that were recorded are insufficient. (Conversely: --no-replay-ondemand-should-error)
--scheduler { file | restart | callgraph }
Specify the scheduler used for the analysis phase:
- file: schedules one job per
file
- callgraph: schedules one job per procedure, following the
syntactic call graph. Usually faster than "file".
- restart: schedules one job per procedure, using locking to
try
and avoid duplicate work between different analysis
processes and
thus performs generally better on high parallelism
--store-analysis-schedule
Activates: Store the analysis schedule for later replay, honoring --replay-analysis-schedule-file if present. This can be useful to store a schedule done with one version of infer to load with another version of infer. There is no guarantee infer will be able to load the previous schedule but using this mechanism gives a higher chance of success compared with having to read the previous results database successfully as fewer datatypes are involved. (Conversely: --no-store-analysis-schedule)
--no-bo-assume-void
Deactivates: Assume void type as a type of record fields not in type environment. (Conversely: --bo-assume-void)
--no-bo-bottom-as-default
Deactivates: Use bottom as a default value instead of unknown. (Conversely: --bo-bottom-as-default)
--bo-context-sensitive-allocsites
Activates: Assume that different calls to the same function creating an allocsite results in different allocsites imported to the caller. (Conversely: --no-bo-context-sensitive-allocsites)
--bo-debug int
Debug level for buffer-overrun checker (0-4)
--bo-exit-frontend-gener-vars
Activates: Put frontend generated variables out of scope when they are listed in exit scope instruction. (Conversely: --no-bo-exit-frontend-gener-vars)
--bo-field-depth-limit int
Limit of field depth of abstract location in buffer-overrun checker
--bo-max-cfg-size int
Larger CFGs than the max size are skipped in buffer overrun analysis.
--bo-sound-unknown-sets-join
Activates: Join with an unknown set always result in an unknown set. When disabled, unknown set behaves as bot. (Conversely: --no-bo-sound-unknown-sets-join)
--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 function that each analysis has to model.
--cxx-scope-guards json
Specify scope guard classes that can be read only by destructors without being reported as dead stores.
--dynamic-dispatch-json-file-path path
Dynamic dispatch file path to get the JSON used for method name substitution
--inline-func-pointer-for-testing string
Enables substituting global function pointers used for testing with the real function calls in the clang frontend. Pass the prefix used to build the global function pointers used for testing.
--liveness-block-list-var-regex string
Specify a regular expression for variable names that are ignored when reporting dead stores.
--liveness-dangerous-classes json
Specify classes where the destructor should be ignored when computing liveness. In other words, assignement to variables of these types (or common wrappers around these types such as unique_ptr<type>) will count as dead stores when the variables are not read explicitly by the program.
--lock-model json
Specify custom lock models for starvation analysis.
Example for pthreads (already
included in infer):
[{"lock":["pthread_mutex_lock"],"unlock":["pthread_mutex_unlock"]}]
--pulse-model-unreachable +string
Methods to be modeled as unreachable.
--pulse-unsafe-malloc
Activates: Assume that malloc(3) never returns null. (Conversely: --no-pulse-unsafe-malloc)
--erlang-list-unfold-depth int
Unfold Erlang lists up to depth int
--no-erlang-reliability
Deactivates: Analyze crashing executions. This flag affects both capture and analysis. At capture time, it encodes Erlang specs; at (Pulse) analysis time, it models Erlang exceptions (builtin or OTP ones). (Conversely: --erlang-reliability)
--no-annotation-reachability-apply-superclass-annotations
Deactivates: Applies annotations from superclasses and interfaces also on methods that are not overridden from the superclass or interface. (Conversely: --annotation-reachability-apply-superclass-annotations)
--annotation-reachability-check-loops
Activates: Highlights callsites in the trace that are nested in some loop. (Conversely: --no-annotation-reachability-check-loops)
--annotation-reachability-custom-models json
Specify a map from annotations to lists of regexps to treat matching methods as if they had the annotation.
Example format:
{"Annotation":
["com\\.Myclass\\.foo.*"]}
--annotation-reachability-custom-pairs json
Specify custom sources/sinks, and optionally sanitizers for the annotation reachability checker
Example format: for custom
annotations
com.my.annotation.{Source1,Source2,Sink1,Sanitizer1}
{ "sources" : ["Source1",
"Source2"], "sinks" :
["Sink1"],
"sanitizers": ["Sanitizer1"] }
--annotation-reachability-expensive
Activates: check if methods annotated with @PerformanceCritical can call expensive methods (annotated @Expensive or modeled, with annotation reachability checker) (Conversely: --no-annotation-reachability-expensive)
--no-annotation-reachability-minimize-sinks
Deactivates: do not report paths where a prefix is also a source to sink path. For example if there is a source() -> sink1() -> sink2() path then only source() -> sink1() will be reported. (Conversely: --annotation-reachability-minimize-sinks)
--annotation-reachability-minimize-sources
Activates: do not report paths where a suffix is also a source to sink path. For example if there is a source1() -> source2() -> sink() path then only source2() -> sink() will be reported. (Conversely: --no-annotation-reachability-minimize-sources)
--annotation-reachability-no-allocation
Activates: check if methods annotated with @NoAllocation can allocate (with annotation reachability checker) (Conversely: --no-annotation-reachability-no-allocation)
--annotation-reachability-report-source-and-sink
Activates: Reports methods that are marked as both a source and a sink at the same time. (Conversely: --no-annotation-reachability-report-source-and-sink)
--external-java-packages +prefix
Specify a list of Java package prefixes for external Java packages. If set, the analysis will not report non-actionable warnings on those packages.
--java-version int
The version of Java being used. Set it to your Java version if mvn is failing.
--no-lineage-dedup
Deactivates: In JSON output, attempt to print each entity at most once. This is the default. The only reason you may want to turn this off is to make hash collisions more visible; that is, cases in which distinct entities get assigned the same ID. (Conversely: --lineage-dedup)
--lineage-field-depth int
[EXPERIMENTAL] Maximal field depth sensitivity for lineage analysis. 0 will make the analysis field insensitive.
--lineage-field-max-cfg-size int
If set, field sensitivity is disabled on larger CFGs.
--lineage-field-width int
[EXPERIMENTAL] Maximal width of structures for field sensitive lineage analysis. Structure that have a higher number of fields will be smashed into a single element. 0 will make the analysis field insensitive.
--lineage-include-builtins
Activates: Include call/return edges to/from procedures that model primitive Erlang operations, such as constructing a list. (Conversely: --no-lineage-include-builtins)
--lineage-json-report
Activates: Enable lineage report in JSON format. (Conversely: --no-lineage-json-report)
--lineage-keep-temporaries
Activates: Normally, lineage summaries do not mention temporary variables introduced while compiling the high-level code to Infer's IR (intermediate representation). If this option is enabled, then the lineage graph produced corresponds to Infer's IR. (Conversely: --no-lineage-keep-temporaries)
--lineage-max-cfg-size int
If set, larger CFGs are skipped.
--no-lineage-prevent-cycles
Deactivates: [EXPERIMENTAL] If given, Lineage will not stop traversing the fields of a variable when it notices recursive types (that is, a sub-field having the same type as one of its "ancestors"). (Conversely: --lineage-prevent-cycles)
--lineage-seed int
Set the random seed used for hashing. (Various entities that get reported need unique identifiers. To generate these unique identifiers, in a distributed way without communication, we use hashing. If you are unlucky and get collisions, you can try a different seed.
--lineage-variant-width int
Maximal width of variant types for lineage analysis. A variant type is the type of a variable whose value is within a statically known atom set. The width of the type is the cardinal of that atom set.
--log-pulse-coverage
Activates: Log precisely where coverage stops, at the end of file stats/stats.txt. (Conversely: --no-log-pulse-coverage)
--log-pulse-disjunct-increase-after-model-call
Activates: Log which model did increase the current number of Pulse disjuncts. (Conversely: --no-log-pulse-disjunct-increase-after-model-call)
--pulse-cut-to-one-path-procedures-pattern string
Regex of methods for which pulse will only explore one path. Can be used on pathologically large procedures to prevent too-big states from being produced.
--pulse-inline-global-init-func-pointer
Activates: Inline the initializer of global variables that are of type function pointer in Pulse. (Conversely: --no-pulse-inline-global-init-func-pointer)
--pulse-log-summary-count
Activates: Log the number of summaries (grouped by summary kind) for each analyzed procedure in Pulse. Results are put in JSON files under a 'pulse' subdirectory, one corresponding to each analysis job. Note that when joining the files, deduplication might be needed. (Conversely: --no-pulse-log-summary-count)
--pulse-max-cfg-size int
Larger CFGs than the max size are skipped in Pulse.
--pulse-max-disjuncts int
Stop exploring new paths after int disjunctions in the domain
--pulse-max-heap int
Give up analysing a procedure if the number of words in the heap exceeds this limit. Intended use: avoid OutOfMemory crashes.
--pulse-model-abort +string
Methods that should be modelled as abort in Pulse
--pulse-model-alloc-pattern string
Regex of methods that should be modelled as allocs in Pulse
--pulse-model-cheap-copy-type regex
Regex of methods that should be cheap to copy in Pulse
--pulse-model-cheap-copy-type-list +regex
Regex of methods that should be cheap to copy in Pulse
--pulse-model-free-pattern string
Regex of methods that should be modelled as wrappers to free(3) in Pulse. The pointer to be freed should be the first argument of the function. This should only be needed if the code of the wrapper is not visible to infer or if Pulse somehow doesn't understand it (e.g. the call is dispatched to global function pointers).
--pulse-model-malloc-pattern string
Regex of methods that should be modelled as wrappers to malloc(3) in Pulse. The size to allocate should be the first argument of the function. See --pulse-model-free-pattern for more information.
--pulse-model-realloc-pattern string
Regex of methods that should be modelled as wrappers to realloc(3) in Pulse. The pointer to be reallocated should be the first argument of the function and the new size the second argument. See --pulse-model-free-pattern for more information.
--pulse-model-release-pattern string
Regex of methods that should be modelled as release in Pulse
--pulse-model-return-first-arg string
Regex of methods that should be modelled as returning the first argument in Pulse in terms of the source language semantics. Languages supported: Java, C, Objective-C
--pulse-model-return-nonnull string
Regex of methods that should be modelled as returning non-null in Pulse
--pulse-model-return-nonnull-list +string
Regex of methods that should be modelled as returning non-null in Pulse
--pulse-model-return-this string
Regex of methods that should be modelled as returning the ‘this‘ or ‘self‘ argument of an instance method in Pulse. Languages supported: Java, Objective-C
--pulse-model-returns-copy-pattern string
Regex of methods that should be modelled as creating copies in Pulse
--pulse-model-skip-pattern string
Regex of methods that should be modelled as "skip" in Pulse
--pulse-model-skip-pattern-list +string
Regex of methods that should be modelled as "skip" in Pulse
--pulse-model-transfer-ownership +string
Methods that should be modelled as transfering memory ownership in Pulse. Accepted formats are method or namespace::method
--pulse-model-unknown-pure +string
Regex of methods that should be modelled as unknown pure in Pulse
--pulse-models-for-erlang +path
Provide custom models for Erlang in JSON files or SQLite3. Files must end with ‘.json‘ or ‘.db‘ respectively. If a path to a directory is given then the subdirectories will be explored and names must follow the same convention. SQLite3 format is preferable when providing a large number of models because they will be internally indexed by mfa.
The format for JSON is
[SelectorBehavior, ...] where
SelectorBehavior := {"selector": Selector,
"behavior": Behavior}
Selector := ["MFA", {
"module": "<module_name>",
"function": "<function_name>",
"arity": <arity_int>
}]
Behavior := ReturnValue | ArgumentsReturnList
- ReturnValue models return regardless of the arguments
- ArgumentsReturnList maps arguments to return values
ReturnValue := ["ReturnValue", ErlangValue]
ArgumentsReturnList :=
["ArgumentsReturnList", [ArgumentsReturn, ...]]
ArgumentsReturn := {
"arguments": [ErlangValue, ...],
"return": ErlangValue
}
ErlangValue := ["Atom",
"<atom_name>"]
| ["IntLit", "<integer_value>"]
| ["List", [ErlangValue, ...]
| ["Tuple", [ErlangValue, ...]
| null
ErlangValue = null is to represent nondeterministic value
The format for SQLite3 is a DB with schema:
CREATE TABLE models(
"mfa" TEXT,
"behavior" TEXT
);
- ‘mfa‘ is module:function/arity, e.g.
"mymod:f/0"
- ‘behavior‘ is a JSON ‘Behavior‘
(see above)
--no-pulse-nullsafe-report-npe
Deactivates: Report null dereference issues on files marked @Nullsafe. (Conversely: --pulse-nullsafe-report-npe)
--pulse-nullsafe-report-npe-as-separate-issue
Activates: Report null dereference issues on files marked @Nullsafe as a separate NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS issue type. (Conversely: --no-pulse-nullsafe-report-npe-as-separate-issue)
--pulse-over-approximate-reasoning
Activates: [EXPERIMENTAL] add over-approximate reasoning on top of the under-approximate, disjunctive reasoning of Pulse. (Conversely: --no-pulse-over-approximate-reasoning)
--pulse-recency-limit int
Maximum number of array elements and structure fields to keep track of for a given address.
--pulse-skip-procedures regex
Regex of procedures that should not be analyzed by Pulse.
--pulse-specialization-iteration-limit int
Maximum number of iterative summary specialization at each call site.
--pulse-specialization-limit int
Maximum number of summary specialization by procedure.
--pulse-taint-config +path
Path to a taint analysis configuration file or a directory containing such files. This file can define --pulse-taint-sources, --pulse-taint-sanitizers, --pulse-taint-propagators, --pulse-taint-sinks, --pulse-taint-policies, and --pulse-taint-data-flow-kinds.
If a path to a directory is
given then the configuration files
must have the ‘.json‘ extension. Any other file
will be ignored.
The subdirectories will be explored and must follow the same
convention.
--pulse-taint-data-flow-kinds json
Specify which taint kinds should be used for data flow reporting only. If a source has such a kind, only data flows to sinks which originate at the source will be reported. If a sink has such a kind, only sensitive data flows to the sink will be reported.
--no-pulse-taint-follow-field-accesses
Deactivates: Specify if taint analysis should follow field accesses when propagating taints. (Conversely: --pulse-taint-follow-field-accesses)
--pulse-taint-opaque-files +path
Specify files that should be treated as opaque for taint analysis to make sure that procedure's belonging to these files are always free of any potential taint flows.
--pulse-taint-policies json
A description of which taint flows should be reported, following this JSON format:
{ "short_description":
"<a short description of the issue>",
"taint_flows": [{ "source_kinds":
[<kinds>],
"sink_kinds": [<kinds>],
"sanitizer_kinds": [<kinds>] }],
"exclude_in": [<paths>],
"exclude_matching": [<regexps>]
}
where <kinds> are specified in taint
source/sanitizer/sink
matchers (see --pulse-taint-sources). The fields
"sanitizer_kinds", "exclude_in" and
"exclude_matching" are
optional (assumed to be empty), and a single policy can
specify
several taint flows using a list. The following policy is
always
enabled:
{ "short_description": "...",
"taint_flows": [{ "source_kinds":
["Simple"],
"sink_kinds": ["Simple"],
"sanitizer_kinds": ["Simple"] }]
}
--pulse-taint-propagators json
Quick way to specify simple propagators as a JSON objects. See --pulse-taint-sources for the fields format documentation.
--pulse-taint-sanitizers json
Quick way to specify simple sanitizers as a JSON objects. See --pulse-taint-sources for the fields format documentation.
--pulse-taint-short-traces
Activates: Cut off taint traces as soon as a tainted value flows into a sink. This matters when the sink itself calls other sinks of the same kind and as long as the value flows from call to call, without this flag the trace would include the whole chain of calls. (Conversely: --no-pulse-taint-short-traces)
--pulse-taint-sinks json
Quick way to specify simple sinks as a JSON objects. See --pulse-taint-sources for the fields format documentation.
--pulse-taint-skip-sources
Activates: Skip the analysis of methods declared as sources in the taint. (Conversely: --no-pulse-taint-skip-sources)
--pulse-taint-sources json
Together with --pulse-taint-sanitizers, --pulse-taint-sinks, --pulse-taint-policies, and --pulse-taint-data-flow-kinds, specify taint properties. The JSON format of sources also applies to sinks and sanitizers. It consists of a list of objects, each with one of the following combinations of fields to identify relevant procedures:
- "field_regex": match
a field name using an OCaml regex
- "procedure": match a substring of the procedure
name
- "procedure_regex": as above, but match using an
OCaml regex
- "class_name_regex": match all methods of classes
whose names
match the OCaml regex
- "class_names" and "method_names":
match exact uses of methods of particular classes
- "class_names" and "procedure_regex":
match exact uses of methods of particular classes matching
specified OCaml regex
- "class_names" and "field_names":
match exact uses of fields of particular classes
- "class_names" and
"method_return_type_names":
match exact uses of methods with particular return types of
particular classes
- "class_name_regex" and
"procedure_regex":
match methods based on separate OCaml regexes for both
classes and procedure names
- "class_with_annotation":
match all procedures defined in a class annotated with
specified annotation
- "overrides_of_class_with_annotation":
match all procedures defined in classes which inherit
from a superclass with the specified annotation
- "method_with_annotation":
match all procedures marked by specified annotation
- "method_with_annotation" and
"annotation_values":
match all procedures marked by specified annotation with
specified values
- "class_with_annotation",
"class_name_regex" and
"procedure_regex":
match procedures based on specified class annotation and
separate OCaml regexes for both classes and procedure names
- "field_with_annotation":
match all fields marked by specified annotation
- "field_with_annotation" and
"annotation_values":
match all fields marked by specified annotation with
specified values
- "allocation": (for taint sources only)
match allocations of the exact class name supplied
- "block_passed_to": (for taint sources
only)
match a substring of the procedure name that the block is
passed to
- "block_passed_to_regex": (for taint sources
only)
as above, but match using an OCaml regex
Each object can also optionally specify:
- "kinds": the kinds of taint, used in
--pulse-taint-policies
to specify flows between sources/sanitizers/sinks
("Simple" by default).
- "taint_target":
where the taint should be applied in the procedure or
field.
- "ReturnValue": (default for taint sources and
propagators)
- "AllArguments": (default for taint sanitizers
and sinks)
- ["ArgumentPositions", [<int list>]]:
argument positions given by index (zero-indexed)
- ["AllArgumentsButPositions", [<int
list>]]:
all arguments except given indices (zero-indexed)
- ["ArgumentsMatchingTypes", [<type list>]]:
arguments with types containing supplied strings
- "InstanceReference": this/self references of
instance
methods
- ["FieldsOfValue", [<(string * taint_target)
list>]]:
fields given by name in return value, arguments or
other fields
- "GetField" : a given field is read
- "SetField" : a given field is set
N.B. for methods, index 0 is this/self.
For all the regex-based matchers, we can also specify:
- "exclude_from_regex_in" - to specify a list of
header files,
such that we exclude any classes, field or methods from
those
files from the regexes.
For field matchers, we can also specify:
- "sanitized_in" - to specify a list of files
where using the
source shouldn't be flagged.
--pulse-widen-threshold int
Stop exploring new paths after int loop iterations
--racerd-always-report-java
Activates: Every Java class analysed is treated as if it were annotated as @ThreadSafe. (Conversely: --no-racerd-always-report-java)
--racerd-guardedby
Activates: Check @GuardedBy annotations with RacerD (Conversely: --no-racerd-guardedby)
--racerd-ignore-classes +string
Any method in a class specified here will be ignored by RacerD.
--threadsafe-aliases json
Specify custom annotations that should be considered aliases of @ThreadSafe
--siof-check-iostreams
Activates: 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. (Conversely: --no-siof-check-iostreams)
--siof-safe-methods +string
Methods that are SIOF-safe; "foo::bar" will match "foo::bar()", "foo<int>::bar()", etc. (can be specified multiple times)
INFER_ARGS, INFERCONFIG, INFER_STRICT_MODE
See the ENVIRONMENT section in the manual of infer(1).
.inferconfig
See the FILES section in the manual of infer(1).
infer-report(1), infer-run(1)