# Technical Documentation: facebook/infer

> ℹ️ **Provenance:** Multi-Tier Ingestion · [CodeWiki Reference](https://codewiki.google/github.com/facebook/infer)

### Overview (README.md)

<img src="website/static/img/logo.png" alt="logo" width="15%" />

# Infer  

[Infer](http://fbinfer.com/) is a static analysis tool for Java,
C++, Objective-C, and C. Infer is written in [OCaml](https://ocaml.org/).

## Installation

Read our [Getting
Started](http://fbinfer.com/docs/getting-started) page for
details on how to install packaged versions of Infer. To build Infer
from source, see [INSTALL.md](./INSTALL.md).

## Contributing

See [CONTRIBUTING.md](./CONTRIBUTING.md).

## License

Infer is MIT-licensed.

Note: Enabling Java support may require you to download and install 
components licensed under the GPL.

---

### 00 Getting Started (`website/docs/00-getting-started.md`)

---
id: getting-started
title: Getting started with Infer
---

## Get Infer

You can use our binary releases, build infer from source, or use our Docker image.

Find our latest [binary release here](https://github.com/facebook/infer/releases/latest). Download
the tarball then extract it anywhere on your system to start using infer. For example, this
downloads infer in /opt on Linux (replace `VERSION` with the latest release, eg `VERSION=1.0.0`):

```bash
VERSION=0.XX.Y; \
curl -sSL "https://github.com/facebook/infer/releases/download/v$VERSION/infer-linux-x86_64-v$VERSION.tar.xz" \
| sudo tar -C /opt -xJ && \
sudo ln -s "/opt/infer-linux-x86_64-v$VERSION/bin/infer" /usr/local/bin/infer
```

If the binaries do not work for you, or if you would rather build infer from
source, follow the
[install from source](https://github.com/facebook/infer/blob/main/INSTALL.md#install-infer-from-source)
instructions to install Infer on your system.

Alternatively, use our [Docker images](https://github.com/facebook/infer/tree/main/docker).

## Try Infer in your browser

Try Infer on a small example on
[Codeboard](https://codeboard.io/projects/11587?view=2.1-21.0-22.0).

---

### 00 Hello World (`website/docs/00-hello-world.md`)

---
id: hello-world
title: Hello, World!
---

Follow the instructions in this page to try Infer on a few small examples. You
should be able to see the bugs reported by Infer, fix the bugs and run Infer
again to check that they are not reported anymore. This should give you a first
idea of how Infer works. See the [User Guide](infer-workflow) for more details
about the use of Infer.

All these examples can be found in the
[`infer/examples`](https://github.com/facebook/infer/tree/main/examples)
directory distributed with Infer.

## Hello world Java

Here is a simple Java example to illustrate Infer at work.

```java
// Hello.java
class Hello {
  int test() {
    String s = null;
    return s.length();
  }
}
```

To run Infer, type the following in your terminal from the same directory as
[`Hello.java`](https://github.com/facebook/infer/tree/main/examples/Hello.java).

```bash
infer run -- javac Hello.java
```

You should see the following error reported by Infer.

```bash
Hello.java:5: error: NULL_DEREFERENCE
  object s last assigned on line 4 could be null and is dereferenced at line 5
```

Now edit the file to add null checks:

```java
  int test() {
    String s = null;
    return s == null ? 0 : s.length();
  }
```

Run Infer again. This time we get no error: Infer reports `No issues found`.

## Hello world Objective-C

Here is a simple Objective-C example to illustrate Infer at work.

```objectivec
// Hello.m
#import <Foundation/Foundation.h>

@interface Hello: NSObject
@property NSString* s;
@end

@implementation Hello
NSString* m() {
    Hello* hello = nil;
    return hello->_s;
}
@end
```

To run Infer, type the following in your terminal from the same directory as
[`Hello.m`](https://github.com/facebook/infer/tree/main/examples/Hello.m).

```bash
infer run -- clang -c Hello.m
```

You should see the following error reported by Infer.

```
Hello.m:10 NULL_DEREFERENCE
  pointer hello last assigned on line 9 could be null and is dereferenced at line 10, column 12
```

Now edit the file to use the getter instead of accessing the instance variable:

```objectivec
NSString* m() {
    Hello* hello = nil;
    return hello.s;
}
```

Run Infer again. This time we get no error: Infer reports `No issues found`.

## Hello world C

Here is a simple C example to illustrate Infer at work.

```c
// hello.c
#include <stdlib.h>

void test() {
  int *s = NULL;
  *s = 42;
}
```

To run Infer, type the following in your terminal from the same directory as
[`hello.c`](https://github.com/facebook/infer/tree/main/examples/hello.c).

```bash
infer run -- gcc -c hello.c
```

You should see the following error reported by Infer.

```
hello.c:5: error: NULL_DEREFERENCE
  pointer s last assigned on line 4 could be null and is dereferenced at line 5, column 10
```

Now edit the file to add null checks:

```c
void test() {
  int *s = NULL;
  if (s != NULL) {
    *s = 42;
  }
}
```

Run Infer again. This time we get no error: Infer reports `No issues found`.

When analyzing C files, Infer captures the gcc command and runs clang instead to
parse them. Thus you may get compiler errors and warnings that differ from
gcc's. So in particular, the following two commands are equivalent:

```bash
infer run -- gcc -c hello.c
infer run -- clang -c hello.c
```

## Hello world C (tree-sitter, no build system)

The tree-sitter frontend analyzes C files directly, without requiring a
compiler, headers, or build system. It is useful for quick checks, IDE
integration, and files that may not compile.

```c
// hello.c
#include <stdlib.h>

void test() {
  int *s = NULL;
  *s = 42;
}
```

```bash
infer --capture-tree-sitter hello.c --pulse
```

You should see the following error reported by Infer:

```
hello.c:6: error: NULLPTR_DEREFERENCE
  null dereference of `s`
```

Unlike the clang frontend, tree-sitter does not need headers or a compilation
database. It parses the source directly and analyzes what it can, even if the
file has syntax errors or missing includes. For full precision with type-aware
analysis, use the clang frontend instead (`infer run -- clang -c hello.c`).

## Hello world Android

To be able to analyze the sample Android app, make sure that you have the
[Android SDK](https://developer.android.com/sdk/installing/index.html) 22
installed and up to date, as well as the "Android SDK Build-tools" and "Android
Support Repository" components.

Go to the sample Android app in
[`infer/examples/android_hello`](https://github.com/facebook/infer/tree/main/examples/android_hello/)
and create a `local.properties` file with a single line
`sdk.dir=<location of your Android SDK>`. This sample Android app uses
[gradle](https://gradle.org/) as its build system. You do not need to install
gradle to try it out though, thanks to the
[`gradlew`](https://docs.gradle.org/current/userguide/gradle_wrapper.html)
script in the project that will download gradle and the project's dependencies
for you.

After editing `local.properties`, run

```bash
infer run -- ./gradlew build
```

Infer will output the list of found bugs:

```bash
app/src/main/java/infer/inferandroidexample/MainActivity.java:29: error: NULL_DEREFERENCE
  object s last assigned on line 28 could be null and is dereferenced at line 29
  27.           setContentView(R.layout.activity_main);
  28.           String s = getDay();
  29. >         int length = s.length();
  30.           writeToFile();
  31.       }
  32.

app/src/main/java/infer/inferandroidexample/MainActivity.java:46: error: RESOURCE_LEAK
   resource of type java.io.FileOutputStream acquired to fis by call to FileOutputStream(...) at line 43 is not released after line 46
  44.               fis.write(arr);
  45.               fis.close();
  46. >         } catch (IOException e) {
  47.               //Deal with exception
  48.           }
  49.

app/src/main/java/infer/other/MainActivity.java:23: error: NULL_DEREFERENCE
  object returned by source() could be null and is dereferenced at line 23
  21.     @Override
  22.     protected void onCreate(Bundle savedInstanceState) {
  23. >     source().toString();
  24.     }
  25.

```

### Differential analysis

If you run Infer again without changing any files, you will notice that this
time nothing gets analyzed. This is because gradle is _incremental_: everything
was compiled already so nothing gets recompiled. Infer captures the compilation
commands to know which files to analyze, hence it analyzes nothing in this case.
There are three solutions to remedy this:

1. Run gradlew clean in between Infer runs.

   ```bash
   ./gradlew clean
   ```

   This causes gradle to recompile everything each time, and subsequently Infer
   to capture all the files again.

2. Run Infer indicating that the capture of compilation commands should
   continue, using option `--continue` (or `-c` for short).

   ```bash
   infer run --continue -- ./gradlew build
   ```

This makes Infer add the effects of the new compilation commands to the previous
ones, and start a new analysis of the entire code.

3. Run Infer in reactive mode after a code change, using option `--reactive` (or
   `-r` for short).

   ```bash
   infer run --reactive -- ./gradlew build
   ```

This makes Infer analyze the effects of the code change, without re-analyzing
everything. Note that only the modified files, and those dependent on them, are
re-analyzed. This analysis mode can be significantly faster.

You can learn more about the particulars of each solution in the
[Infer workflow](infer-workflow) page.

## Hello world iOS

Go to the sample iOS app in
[`infer/examples/ios_hello`](https://github.com/facebook/infer/tree/main/examples/ios_hello/)
and run Infer on it:

```bash
infer run -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator
```

Infer will output the list of found bugs:

```
/* Detailed source-code truncated for AI context efficiency. */
```

Similarly to the case of [gradle](#differential-analysis),
running the command above a second time will yield no analysis results, as
nothing gets recompiled. Either add the `--reactive` (or `-r`) flag to the
`infer` command:

```bash
infer run --reactive -- xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator
```

or ask the build system to reinitialize the directory before running Infer
again, using

```bash
xcodebuild -target HelloWorldApp -configuration Debug -sdk iphonesimulator clean
```

## Hello world Make

Go to the sample C project in
[`infer/examples/c_hello`](https://github.com/facebook/infer/tree/main/examples/c_hello/)
and run Infer on it:

```bash
infer run -- make
```

Infer will output the list of found bugs:

```bash
example.c:22: error: NULL_DEREFERENCE
   pointer max last assigned on line 21 could be null and is dereferenced at line 22, column 10

example.c:36: error: NULL_DEREFERENCE
   pointer joe last assigned on line 35 could be null and is dereferenced by call to get_age() at line 36, column 10

example.c:45: error: RESOURCE_LEAK
   resource acquired to fd by call to open() at line 41, column 12 is not released after line 45, column 5

example.c:51: error: MEMORY_LEAK
   memory dynamically allocated to p by call to malloc() at line 51, column 14 is not reachable after line 51, column 3

example.c:57: error: MEMORY_LEAK
   memory dynamically allocated to p by call to malloc() at line 56, column 14 is not reachable after line 57, column 3
```

Similarly to the case of [gradle](#differential-analysis),
running `infer run -- make` a second time will yield no analysis results, as
nothing gets recompiled. Either add the `--reactive` (or `-r`) flag to the
`infer` command:

```bash
infer run --reactive -- make
```

or run

```bash
make clean
```

before analyzing the project again.

---

### 01 Analyzing Apps Or Projects (`website/docs/01-analyzing-apps-or-projects.md`)

---
id: analyzing-apps-or-projects
title: Analyzing apps or projects
---

To analyze files with Infer you can use the compilers `javac` and `clang`. You
can also use Infer with `gcc`, however, internally Infer will use `clang` to
compile your code. So, it may not work if your code does not compile with
`clang`.

Moreover, you can run Infer with a variety of build systems. Notice that you can
run infer faster by running the compilation command in parallel, e.g.
`infer run -- make -j8`. Please also take into account that if you wish to
analyze a project, you should probably do `clean` beforehand so that the
compiler compiles all the files and so Infer also analyses all the files (see
the [previous section](infer-workflow)).

Here is an overview of the build systems supported by Infer. You can get more
information about how a particular build system is supported by looking at the
SYNOPSIS section of the infer-capture manual: `infer capture --help`.

### ant

```bash
infer run -- ant
```

### Buck

Running:

```bash
infer run -- buck <buck target>
```

will compute the list of Infer warnings in the targets passed as argument.

Running:

```bash
infer run -- buck --deep <buck target>
```

will compute the list of Infer warnings in the targets passed as argument and
all the transitive dependencies.

The distinction between `--deep` and the normal Buck complation mode is only
supported for Java projects. For the other kinds of projects, the `--deep`
option has no effect.

### cmake

The most robust way is to have `cmake` generate a compilation database that can
be then processed by Infer:

```bash
cd build
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ..
cd ..
infer run --compilation-database build/compile_commands.json
```

Alternatively, one can trick `cmake` into using infer instead of the system's
compilers:

```bash
cd build
infer compile -- cmake ..
infer run -- make -j 4
```

### Gradle

```bash
infer run -- gradle <gradle task, e.g. "build">
infer run -- ./gradlew <gradle task, e.g. "build">
```

### Make

Infer can analyze projects that compile with `make` by switching the compilers
(for C/C++/Objective-C or Java) called by `make` with infer wrappers. This
doesn't always work, for instance if the Makefiles hardcode the absolute paths
to the compilers (eg, if `make` calls `/usr/bin/gcc` instead of `gcc`). This is
because this integration works by modifying `PATH` under the hood.

```bash
infer run -- make <make target>
```

### Maven

```bash
infer run -- mvn <maven target>
```

### Xcodebuild

The most robust way is to generate a compilation database, then pass that
database to Infer:

```bash
xcodebuild <your build options> | tee xcodebuild.log
xcpretty -r json-compilation-database -o compile_commands.json < xcodebuild.log > /dev/null
infer run --skip-analysis-in-path Pods --clang-compilation-db-files-escaped compile_commands.json
```

See also
[this comment on GitHub](https://github.com/facebook/infer/issues/9#issuecomment-280121791).

Infer also provides a direct integration to xcodebuild that swaps the compiler
used by xcodebuild under the hood. For instance, for an iOS app:

```bash
infer run -- xcodebuild -target <target name> -configuration <build configuration> -sdk iphonesimulator
```

There is an alternative xcodebuild integration that uses `xcpretty` under the
hood; use it by passing `--xcpretty` to infer.

### xctool

Use `xctool` to generate a compilation database then pass it to infer:

```bash
xctool.sh <your build options> -reporter json-compilation-database:compile_commands.json
infer run --skip-analysis-in-path Pods --clang-compilation-db-files-escaped compile_commands.json
```

See also
[this comment on GitHub](https://github.com/facebook/infer/issues/9#issuecomment-280121791).

### Using a compilation database

Many build systems like cmake, Xcode or Buck generate compilation databases.
infer is able to use this database directly, simplifying its usage.

```bash
infer --compilation-database compile_commands.json
```

### Other build systems

If infer doesn't recognize your build system, you will get an error like this:

```console
$ infer run -- foo
Usage Error: Unsupported build command foo
```

If your build system behaves like one of the above, you can tell infer to use
the same integration with `--force-integration`. For instance this will proceed
as if `foo` was working the same way as `make`:

```bash
infer run --force-integration make -- foo
```

If your build system is more exotic, and it doesn't support outputting
compilation databases, please let us know by
[opening an issue](https://github.com/facebook/infer/issues/new).

---

### 01 Infer Workflow (`website/docs/01-infer-workflow.md`)

---
id: infer-workflow
title: Infer workflow
---

This page documents several ways of running Infer, that you can adapt to your
own project.

**tl; dr**:

1. Make sure your project is clean when you first run Infer on it (with
   `make clean`, or `gradle clean`, or ...).
2. When running Infer several times in a row, either clean your project as in
   step 1 in-between Infer runs, or add `--reactive` to the `infer` command.
3. These steps are not needed if you are not using an incremental build system,
   for instance if you are analyzing single files with
   `infer run -- javac Hello.java`.
4. After a successful Infer run, you can explore Infer's reports in more details
   by running `infer explore` from the same directory.

## The two phases of an Infer run

Regardless of the input language (Java, Objective-C, or C), there are two main
phases in an Infer run:

### 1. The capture phase

Compilation commands are captured by Infer to translate the files to be analyzed
into Infer's own internal intermediate language.

This translation is similar to compilation, so Infer takes information from the
compilation process to perform its own translation. This is why we call infer
with a compilation command: `infer run -- javac File.java` or
`infer run -- clang -c file.c`. What happens is that the files get compiled as
usual, and they also get translated by Infer to be analyzed in the second phase.
In particular, if no file gets compiled, also no file will be analyzed.

Infer stores the intermediate files in the results directory which by default is
created in the folder where the `infer` command is invoked, and is called
`infer-out/`. You can change the name of the results directory with the option
`-o`, e.g.

```bash
infer run -o /tmp/out -- javac Test.java
```

You can run just the capture phase using the `capture` subcommand instead of the
`run` subcommand:

```bash
infer capture -- javac Test.java
```

### 2. The analysis phase

In this phase, the files in `infer-out/` are analyzed by Infer. Infer analyzes
each function and method separately. If Infer encounters an error when analyzing
a method or function, it stops there for that method or function, but will
continue the analysis of other methods and functions. So, a possible workflow
would be to run Infer on your code, fix the errors generated, and run it again
to find possibly more errors or to check that all the errors have been fixed.

The errors will be displayed in the standard output and also in a file
`infer-out/report.txt`. We filter the bugs and show the ones that are most
likely to be real.

## Global (default) and differential workflows

By default, running Infer will delete the previous `infer-out/` directory if it
exists. This leads to a _default_ workflow where the entire project is analyzed
every time. Passing `--reactive` (or `-r`) to Infer prevents it from deleting
`infer-out/`, leading to a _differential_ workflow.

There are exceptions to this. In particular, you can run only one of the phases
above. For instance, `infer run -- javac Hello.java` is equivalent to running
these two commands:

```bash
infer capture -- javac Hello.java
infer analyze
```

Notice that the second command does not erase `infer-out/`, as the files it
needs to analyze live there!

You can learn more about the subcommands supported by Infer by running
`infer --help`, `infer capture --help`, or more generally
`infer <subcommand> --help`.

Let us highlight when you may need global and differential workflows.

### Global workflow

The global workflow is well suited to running Infer on all the files in a
project, e.g., for a Gradle-based project that compiles using the `gradle build`
command:

```bash
infer run -- gradle build
```

In general, running Infer on your project is as simple as running
`infer run -- <your build command here>` where the build command is the one you
would normally use to compile your source code.

To start a fresh analysis and be sure to analyze all the files in your project,
you have to clean the build products, for instance with `make clean` for a
make-based project, `gradle clean` for Gradle, etc.

### Differential workflow

Software projects such as mobile apps use _incremental_ build systems, where
code evolves as a sequence of code changes. For these projects, it can often
make sense to analyze only the current changes in the project, instead of
analyzing the whole project every time. It is possible to analyze only what's
changed using Infer's _reactive mode_.

Infer should first be run on a _clean_ version of the project, to capture all
the compilation commands in its capture phase.

For instance, for a project compiled using Gradle,

```bash
gradle clean
infer capture -- gradle build
```

Note that the above command does not perform an expensive analysis, but captures
all the compilation commands and stores the results in Infer's internal format.

Next, if you change some files in your project, for instance in response to an
Infer report, or as part of normal development, you can either clean and
reanalyze the entire project (as in the [global workflow](#global-workflow)
above), or else tell Infer that you are interested in the effects of the code
change. The second option can be significantly faster, as only a subset of the
project needs to be analyzed: the modified files/procedures and their
dependencies.

```bash
edit some/File.java
# make some changes to some/File.java
infer run --reactive -- gradle build
```

Note that you can run Infer with the `--reactive` flag the first time around as
well.

To control the granularity of the changes to be analyzed, it is possible to tell
Infer to combine several changes into one before the analysis. This is done with
the `--continue` option.

For example:

```bash
edit some/File1.java
# make some changes to some/File1.java
infer run --reactive -- gradle build
edit some/File2.java
# make some changes to some/File2.java
infer run --reactive --continue -- gradle build
```

After the first invocation, Infer will analyze the results of the first change.
After the second invocation, Infer will analyze the results of both changes. If
the `--continue` option were omitted, it would only analyze the results of the
second change.

Finally, it is always possible to perform an analysis of the current changes in
isolation:

```bash
infer run --reactive --continue -- analyze
```

The list of build systems supported by Infer is detailed in the
[next section](analyzing-apps-or-projects).

## Exploring Infer reports

You can get more information about the reports generated by Infer by running
`infer explore` in the same directory. For instance

```bash
infer run -- gradle build
infer explore
```

This tool allows you to see error traces leading to each bug reported by Infer,
which can be helpful in tracking down the precise cause of each bug. See the
output of `infer explore --help` for more information.

---

### 01 Man Pages (`website/docs/01-man-pages.md`)

---
id: man-pages
title: Infer Manuals
---

Here are the man pages for all the infer commands:

- [infer](pathname:///man/next/infer.1.html)
- [infer analyze](pathname:///man/next/infer-analyze.1.html)
- [infer capture](pathname:///man/next/infer-capture.1.html)
- [infer compile](pathname:///man/next/infer-compile.1.html)
- [infer help](pathname:///man/next/infer-help.1.html)
- [infer explore](pathname:///man/next/infer-explore.1.html)
- [infer report](pathname:///man/next/infer-report.1.html)
- [infer reportdiff](pathname:///man/next/infer-reportdiff.1.html)
- [infer run](pathname:///man/next/infer-run.1.html)

---

### 01 Steps For Ci (`website/docs/01-steps-for-ci.md`)

---
id: steps-for-ci
title: Recommended flow for CI
---

The recommended flow for CI integration is to determine the modified files, and
run the analysis in reactive mode starting from those files. If you would like
to run more than one analyzer, it is more efficient to separate the capture
phase, so that the result can be used by all the analyzers.

### Differential Workflow

Here's how to run infer on two versions of a project and compare the results in
general.

Assume the project uses git, `feature` is the feature branch (the code change
you want to analyze), `main` is the main branch, and `make` builds the
project.

```bash
# go to feature branch if not there already
git checkout feature
# get list of changed files
git diff --name-only origin/feature..origin/main > index.txt
## first run: feature branch
# run infer on the feature branch
infer capture -- make -j 4  # assuming a machine with 4 cores
infer analyze --changed-files-index index.txt
# store the infer report
cp infer-out/report.json report-feature.json
## second run: main branch
git checkout main
# run capture in reactive mode so that previously-captured source files are kept if they are up-to-date
infer capture --reactive --mark-if-unchanged -- make -j 4
infer analyze --incremental-analysis --changed-files-index index.txt
# compare reports
infer reportdiff --report-current report-feature.json --report-previous infer-out/report.json
```

At the end of this process, "infer-out/differential/" contains three files,
which follow the same format as normal infer JSON reports:

- introduced.json contains the issues found in the feature branch but not in
  main;
- fixed.json contains the issues found in main but not in the feature branch;
- preexisting.json contains the issues found in both branches.

### Example: Android Gradle

The following CI script runs the `infer` and `eradicate` analyzers. Assume again
that `feature` is the feature branch, and `main` is the main branch.

```bash
git diff --name-only origin/feature..origin/main > index.txt
infer capture -- ./gradlew --offline assembleDebug
infer analyze --fail-on-issue --eradicate --changed-files-index ./index.txt
```

Notice that

- We use git to find the changed files `git diff --name-only`
- We run capture only once, and the output is kept for the subsequent analyses
- We run the eradicate analysis alongside the default analyses: `--eradicate`
- We analyze only the changed files `--changed-files-index ./index.txt`

---

### 01 Suppressions (`website/docs/01-suppressions.md`)

---
id: suppressions
title: Suppression of Infer Issues
---

Infer includes a language-agnostic method to suppress Infer issues in source files.

When an Infer issue is suppressed, it will not appear in the text report (infer-out/report.txt) after an Infer run. Suppressed issues will still appear in the JSON report file (infer-out/report.json) but with the added key `"suppressed": true`.

Two keywords are supported:

* `@infer-ignore ISSUE_TYPE, ISSUE_TYPE2, ...`

  Ignore matching Infer issues on the next or current line. Comma `,` is used to separate multiple issue types on the same line.

* `@infer-ignore-every ISSUE_TYPE, ISSUE_TYPE2, ...`

  Ignore all matching Infer issues in the current file. This keyword can be added anywhere in the source file.

These two keywords are meant to be added as comment lines in the source files you run Infer on.

The full name of the issue type is given as an argument to the @ignore keywords. For example, use `DEAD_STORE` and not 'Dead Store' which is the name used in the text report file.

### Wildcards

Wildcards can be used as arguments to the @ignore keywords to suppress a larger set of Infer issue types without the need to list all of them.

For example, `@infer-ignore PULSE_UNNECESSARY_COPY*` will suppress all unnecessary copy issues, including `PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST` and `PULSE_UNNECESSARY_COPY_INTERMEDIATE`, etc.

### Examples

* Suppress a single issue

```java
// @infer-ignore THREAD_SAFETY_VIOLATION
if (ConfigUtil.getBoolean(context)) {
    ...
}

// or

if (ConfigUtil.getBoolean(context)) { // @infer-ignore THREAD_SAFETY_VIOLATION
    ...
}

```

* Suppress all issues in a file

```php
% @infer-ignore-every TOPL_ERROR, TOPL_ERROR_LATENT
-module(hello).
-export([hello_world/0]).
hello_world() -> io:fwrite("hello\n").
```

* A line without an @ignore keyword cannot be placed between the @ignore line and the line with the issues.

```java
// @infer-ignore THREAD_SAFETY_VIOLATION
// some more context
if (ConfigUtil.getBoolean(context)) {
    ...
}
```

In this case, the issue on the if statement line is not suppressed since a line without a @infer-ignore is added between the suppression and the line with the issue.

#### Accumulation

When using the `@infer-ignore` keyword, all issue types in a contiguous block of comment lines containing the `@infer-ignore` keyword are accumulated and applied to the next line without a @ignore keyword. This way, long lines can be avoided, and extra context can be given.

For example:

```c
free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE
// also this one @infer-ignore DEAD_STORE
return *x;
```

In the example above, on the `return` line, both the issue types `USE_AFTER_FREE` and `DEAD_STORE` are suppressed.

Equivalent to the example above:

```c
free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE
return *x; // @infer-ignore DEAD_STORE
```

An alternative way to achieve the same result would be:

```c
free(x);
// a really good explanation why we are suppressing this warning
// @infer-ignore USE_AFTER_FREE, DEAD_STORE
return *x;
```

---

### 02 About Infer (`website/docs/02-about-infer.md`)

---
id: about-Infer
title: About Infer
---

Infer is a static program analyzer for Java, C, C++, Objective-C, and
Erlang, written in [OCaml](https://ocaml.org/). Infer is deployed
within Meta and it is running as part of its Continuous Integration
pipeline to verify select properties of every code modification for a
large range of projects, including the main family of apps such as
Facebook, Messenger, Instagram, and WhatsApp. Infer is used at a
number of other companies too. Infer can detect deep issues such as
null pointer dereferences, data races, and many more, which can
involve reasoning about multiple functions or methods in different
files in the code.

---

### 02 Separation Logic And Biabduction (`website/docs/02-separation-logic-and-biabduction.md`)

---
id: separation-logic-and-bi-abduction
title: Separation logic and bi-abduction
---

export const Math = ({ code }) => ( <img
src={`https://math.now.sh?from=${encodeURIComponent(code)}&color=mediumslateblue`}
style={{ height: '100%', verticalAlign: "middle" }} /> );

- [Separation logic](separation-logic-and-bi-abduction#separation-logic)
- [Bi-abduction](separation-logic-and-bi-abduction#bi-abduction)
- [Technical papers](separation-logic-and-bi-abduction#technical-papers)

## Separation logic

Separation logic is a novel kind of mathematical logic which facilitates
reasoning about mutations to computer memory. It enables scalability by breaking
reasoning into chunks corresponding to local operations on memory, and then
composing the reasoning chunks together.

Separation logic is based on a logical connective <Math code="\\( * \\)" />
called the _separating conjunction_ and pronounced "and separately". Separation
logic formulae are interpreted over program allocated heaps. The logical formula
<Math code="\\( A*B \\)" /> holds of a piece of program heap (a heaplet) when it
can be divided into two sub-heaplets described by <Math code="\\(A\\)" /> and
<Math code="\\(B\\)" />. For example, the formula

---

<Math code="\\(x \mapsto y * y \mapsto x \\)" />

---

can be read "<Math code="\\(x\\)" /> points to <Math code="\\(y\\)" /> and
separately <Math code="\\(y\\)" /> points to <Math code="\\(x\\)" />". This
formula describes precisely two allocated memory cells. The first cell is
allocated at the address denoted by the pointer <Math code="\\(x\\)" /> and the
content of this cell is the value of <Math code="\\(y\\)" />. The second cell is
allocated at the address denoted by the pointer <Math code="\\(y\\)" /> and the
content of this second cell is the value of <Math code="\\(x\\)" />. Crucially,
we know that there are precisely two cells because <Math code="\\( * \\)" />
stipulates that they are separated and therefore the cells are allocated in two
different parts of memory. In other words, <Math code="\\( * \\)" /> says that
<Math code="\\(x\\)" /> and <Math code="\\(y\\)" /> do not hold the same value
(i.e., these pointers are not aliased). The heaplet partitioning defined by the
formula above can be visualized like so:



The important thing about the separating conjunction is the way that it fits
together with mutation to computer memory; reasoning about program commands
tends to work by updating <Math code="\\(*\\)" />-conjuncts in-place, mimicking
the operational in-place update of RAM.

Separation logic uses Hoare triples of the form
<Math code="\\( \lbrace pre \rbrace prog \lbrace post \rbrace \\)" /> where
<Math code="\\(pre\\)" /> is the precondition, <Math code="\\(prog\\)" /> a
program part, and <Math code="\\(post\\)" /> the postcondition. Triples are
abstract specifications of the behavior of the program. For example, we could
take

---

<Math code="\\( \lbrace r \mapsto open\rbrace \, closeResource(r)\, \lbrace r \mapsto closed\rbrace  \;\;\; (spec)\\)" />

---

as a specification for a method which closes a resource given to it as a
parameter.

Now, suppose we have two resources <Math code="\\( r\_1 \\)" /> and
<Math code="\\( r\_2 \\)" />, described by
<Math code="\\(r\_1 \mapsto open * r\_2 \mapsto open\\)" /> and we close the
first of them. We think operationally in terms of updating the memory in place,
leaving <Math code="\\(r\_2 \mapsto open\\)" /> alone, as described by this triple:

---

<Math code="\\( \lbrace r\_1 \mapsto open * r\_2 \mapsto open\rbrace  closeResource(r\_1) \lbrace r\_1 \mapsto closed * r\_2 \mapsto open \rbrace \;\;\; (use)\\)" />

---

What we have here is the that specification (spec) described how
<Math code="\\(closeResource()\\)" /> works by mentioning only one piece of
state, what is sometimes called a small specification, and in (use) we use that
specification to update a larger precondition in place.

This is an instance of a general pattern. There is a rule that lets you go from
smaller to bigger specifications

---

<Math code="\\( \frac{\lbrace pre \rbrace prog \lbrace post \rbrace}{\lbrace pre * frame \rbrace prog \lbrace post * frame \rbrace}\\)" />

---

Our passage from (spec) to (use) is obtained by taking

- <Math code="\\(pre\\)" /> to be <Math code="\\(r\_1 \mapsto open\\)" />
- <Math code="\\(post\\)" /> to be <Math code="\\(r\_1 \mapsto closed \\)" />,
  and
- <Math code="\\(frame\\)" /> to be <Math code="\\(r\_2 \mapsto open \\)" />

This rule is called the _frame rule_ of separation logic. It is named after the
frame problem, a classic problem in artificial intelligence. Generally, the
<Math code="\\(frame\\)" /> describes state that remains unchanged; the
terminology comes from the analogy of a background scene in an animation as
unchanging while the objects and characters within the scene change.

The frame rule is the key to the principle of local reasoning in separation
logic: reasoning and specifications should concentrate on the resources that a
program accesses (the footprint), without mentioning what doesn't change.

## Bi-abduction

Bi-abduction is a form of logical inference for separation logic which automates
the key ideas about local reasoning.

Usually, logic works with validity or entailment statements like

---

<Math code="\\(A \vdash B\\)" />

---

which says that <Math code="\\(A\\)" /> implies <Math code="\\(B\\)" />. Infer
uses an extension of this inference question in an internal theorem prover while
it runs over program statements. Infer's question

---

<Math code="\\(A * ?antiframe \vdash B * ?frame\\)" />

---

is called _bi-abduction_. The problem here is for the theorem prover to <i>
discover </i> a pair of frame and antiframe formulae that make the entailment
statement valid.

Global analyses of large programs are normally computationally intractable.
However, bi-abduction breaks apart a large analysis of a large program into
small independent analyses of its procedures. This gives Infer the ability to
scale independently of the size of the analyzed code. Moreover, by breaking the
analysis into small independent parts, when the full program is analyzed again
because of a code change the analysis results of the unchanged part of the code
can be reused, and only the code change needs to be re-analyzed. This process
is called incremental analysis and it is very powerful when integrating a
static analysis tool like Infer in a development environment.

In order to be able to decompose a global analysis into small independent
analyses, let's first consider how a function call is analyzed in separation
logic. Assume we have the following spec for a function
<Math code="\\( f() \\)" />:

---

<Math code="\\( \lbrace pre\_f \rbrace \;\; f() \;\; \lbrace post\_f \rbrace \\)" />

---

and by analyzing the caller function, we compute that before the call of <Math
code="\\( f \\)" />, the formula <Math code="\\( CallingState \\)" />
holds. Then to utilize the specification of <Math code="\\( f \\)" /> the
following implication must hold:

---

<Math code="\\( CallingState \vdash pre\_f  \;\;\;\;\;\;\;\;\;\;\;\; (Function Call)\\)" />

---

Given that, bi-abduction is used at procedure call sites for two reasons: to
discover missing state that is needed for the above implication to hold and
allow the analysis to proceed (the antiframe) as well as state that the
procedure leaves unchanged (the frame).

To see how this works suppose we have some bare code

---

<Math code="\\(closeResource(r1); \, closeResource(r2)\\)" />

---

but no overall specification; we are going to describe how to discover a
pre/post spec for it. Considering the first statement and the (spec) above, the
human might say: if only we had <Math code="\\(r1 \mapsto open\\)" /> in the
precondition then we could proceed. Technically, we ask a bi-abduction question:

---

<Math code="\\(emp * ?antiframe \vdash r1 \mapsto open * ?frame\\)" />

---

and we can fill this in easily by picking
<Math code="\\(antiframe = r1 \mapsto open\\)" /> and
<Math code="\\(frame = emp\\)" />, where <Math code="emp"/>
means the empty state. The <Math code="emp" /> is recording that at the start
we presume nothing. So we obtain the trivially true implication:

---

<Math code="\\(emp * r1 \mapsto open \vdash r1 \mapsto open * emp\\)" />

---

which, by applying logical rules, can be re-written equivalently to:

---

<Math code="\\(r1 \mapsto open \vdash r1 \mapsto open\\)" />

---

Notice that this satisfies the (Function Call) requirement to correctly make
the call. So let's add that information in the <Math code="pre" />, and while
we are at it, record the information in the <Math code="post" /> of the first
statement that comes from <Math code="\\(spec\\)" />.

---

<Math code="\\( \lbrace r1 \mapsto open  \rbrace \\)" />
<Math code="\\( closeResource(r1) \\)" />
<Math code="\\( \lbrace r1 \mapsto closed \rbrace \\)" />
<Math code="\\( closeResource(r2) \\)" />

---

Now, let's move to the second statement. Its precondition
<Math code="\\(r1 \mapsto closed\\)" /> in the partial symbolic execution trace
just given does not have the information needed by
<Math code="\\(closeResource(r2)\\)" />, so we can fill that in and continue by
putting <Math code="\\(r2 \mapsto open\\)" /> in the <Math code="pre" />. While
we are at it, we can thread this assertion back to the beginning.

---

<Math code="\\( \lbrace r1 \mapsto open * r2 \mapsto open  \rbrace \\)" />
<Math code="\\( closeResource(r1) \\)" />
<Math code="\\( \lbrace r1 \mapsto closed * r2 \mapsto open\rbrace \\)" />
<Math code="\\( closeResource(r2) \\)" />

---

This information on what to thread backwards can be obtained as the antiframe
part of the bi-abduction question:

---

<Math code="\\(r1 \mapsto closed * ?antiframe \vdash r2 \mapsto open * ?frame\\)" />

---

where the solution picks
<Math code="\\(antiframe = r2 \mapsto open\\) and \\(frame = r1 \mapsto closed\\)" />.
Note that the antiframe is precisely the information missing from the
precondition in order for <Math code="\\(closeResource(r2)\\)" /> to proceed. On
the other hand, the frame <Math code="\\(r1 \mapsto closed\\)" /> is the portion
of state not changed by <Math code="\\(closeResource(r2)\\)" />; we can thread
that through to the overall postconditon (as justified by the frame rule),
giving us:

---

<Math code="\\( \lbrace r1 \mapsto open * r2 \mapsto open  \rbrace \\)" />
<Math code="\\( closeResource(r1) \\)" />
<Math code="\\( \lbrace r1 \mapsto closed * r2 \mapsto open\rbrace \\)" />
<Math code="\\( closeResource(r2) \\)" />
<Math code="\\( \lbrace r1 \mapsto closed * r2 \mapsto closed \rbrace\\)" />

---

Thus, we have obtained a <Math code="pre" /> and <Math code="post" /> for this
code by symbolically executing it, using bi-abduction to discover preconditions
(abduction of antiframes) as well as untouched portions of memory (frames) as
we go along.

In general, bi-abduction provides a way to infer a pre/post specs from bare
code, as long as we know specs for the primitives at the base level of the code.
The human does not need to write preconditions and postconditions for all the
procedures, which is the key to having a high level of automation. This is the
basis for how Infer works, why it can scale, and how it can analyze code changes
incrementally.

Context: The logical terminology we have been using here comes from AI and
philosophy of science. Abductive inference was introduced by the philosopher
Charles Peirce, and described as the mechanism underpinning hypothesis formation
(or, guessing what might be true about the world), the most creative part of the
scientific process. Abduction and the frame problem have both attracted
significant attention in AI. Infer uses an automated form of abduction to
generate preconditions describing the memory that a program touches (the
antiframe part above), and frame inference to discover what isn't touched. Infer
then uses deductive reasoning to calculate a formula describing the effect of a
program, starting from the preconditions. In a sense, Infer approaches automated
reasoning about programs by mimicking what a human might do when trying to
understand a program: it abduces what the program needs, and deduces conclusions
of that. It is when the reasoning goes wrong that Infer reports a potential bug.

This description is by necessity simplified compared to what Infer actually
does. More technical information can be found in the following papers. The
descriptions in the papers are precise, but still simplified; there are many
engineering decisions not recorded there. Finally, beyond the papers, you can
read the source code if you wish!

## Technical papers

The following papers contain some of the technical background on Infer and
information on how it is used inside Facebook.

- <a href="http://link.springer.com/chapter/10.1007%2F3-540-44802-0_1">Local
  Reasoning about Programs that Alter Data Structures.</a> An early separation
  logic paper which advanced ideas about local reasoning and the frame rule.
- <a href="http://link.springer.com/chapter/10.1007/11804192_6">Smallfoot:
  Modular Automatic Assertion Checking with Separation Logic.</a> First
  separation logic verification tool, introduced frame inference
- <a href="http://link.springer.com/chapter/10.1007%2F11691372_19">A Local Shape
  Analysis Based on Separation Logic.</a> Separation logic meets abstract
  interpretation; calculating loop invariants via a fixed-point computation.
- <a href="http://dl.acm.org/citation.cfm?id=2049700">Compositional Shape
  Analysis by Means of Bi-Abduction.</a> The bi-abduction paper.
- <a href="https://research.facebook.com/publications/moving-fast-with-software-verification/">Moving
  Fast with Software Verification.</a> A paper about the way we use Infer at
  Facebook.

---

### 04 Absint Framework (`website/docs/04-absint-framework.md`)

---
id: absint-framework
title: Building checkers with the Infer.AI framework
---

Infer.AI is a framework for quickly developing abstract interpretation-based
checkers (intraprocedural or interprocedural). You define only:

1. An abstract domain (type of abstract state plus `<=`, `join`, and `widen`
operations)
2. Transfer functions (a transformer that takes an abstract state as input and
produces an abstract state as output)

What you get in exchange is an analysis that can run on all of the
languages Infer supports (C, Objective-C, C++, and Java)!

This guide covers how to use the framework. For background on why we built the
framework and how it works, check out these
[slides](/downloads/pldi17-infer-ai-tutorial.pdf) from a PLDI
2017 tutorial and this
[talk](https://atscaleconference.com/videos/getting-the-most-out-of-static-analyzers)
from @Scale2016.

**If you feel like coding instead of reading, a great way to get started with
Infer.AI is to go through the lab exercise
[here](https://github.com/facebook/infer/blob/main/infer/src/labs/README.md).**

## By example: intraprocedural analysis

This section helps you get started ASAP if you already understand
[abstract interpretation](http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html) (or
don't, but are feeling bold).

Take a look at
[liveness.ml](https://github.com/facebook/infer/blob/main/infer/src/checkers/liveness.ml).
This code is performing a compilers-101 style liveness analysis over
SIL, Infer's intermediate
language. Since this code is fairly small and you should already understand what
it's trying to do, it's a fairly good place to look in order to understand both
how to use the abstract interpretation framework and what SIL is.

There are basically three important bits here: defining the domain, defining the
transfer functions, and then passing the pieces to the framework to create an
analysis. Let's break down the third bit:

```OCaml
module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional))
module CheckerAnalyzer =
  AbstractInterpreter.MakeRPO (TransferFunctions (CheckerMode) (CFG))
```

The `ProcCfg.Backward (ProcCfg.Exceptional)` part says: "I want the direction of
iteration to be backward" (since liveness is a backward analysis), and "I want
the analysis to follow exceptional edges". For a forward analysis that ignores
exceptional edges, you would do `ProcCfg.Normal` instead (and many other
combinations are possible; take a look at
[ProcCfg.mli](https://github.com/facebook/infer/blob/main/infer/src/absint/ProcCfg.mli)
for more). And finally, the `TransferFunctions` part says "Use the transfer
functions I defined above".

Now you have a `CheckerAnalyzer` module that exposes useful functions
like
[`compute_post`](https://github.com/facebook/infer/blob/main/infer/src/absint/AbstractInterpreter.mli#L30)
(take a procedure as input and compute a postcondition) and
[`exec_pdesc`](https://github.com/facebook/infer/blob/main/infer/src/absint/AbstractInterpreter.mli#L36)
(take a procedure and compute an invariant map from node id's to the
pre/post at each node). The next step is to hook your checker up to
the Infer command-line interface (CLI). For the liveness analysis, you
would do this by exposing a function for running the checker on a
single procedure:

```OCaml
let checker ({IntraproceduralAnalysis.proc_desc; err_log} as analysis_data) =
  match Analyzer.compute_post analysis_data ~initial:Domain.empty with
  | Some post ->
      Logging.progress "Computed post %a for %a"
        Domain.pp post Procname.pp (Procdesc.get_proc_name proc_desc);
  | None -> ()
```

and then adding `Liveness.checker` to the list of registered checkers
in
[registerCheckers.ml](https://github.com/facebook/infer/blob/main/infer/src/backend/registerCheckers.ml)
(search for "Liveness").

you can then run `infer run --liveness-only -- <your_build_command>` to run your
checker on real code. See [here](/docs/next/analyzing-apps-or-projects) for more
details on the build systems supported by Infer.

Other examples of simple intraprocedural checkers are
[addressTaken.ml](https://github.com/facebook/infer/blob/main/infer/src/checkers/addressTaken.ml)
and
[Siof.ml](https://github.com/facebook/infer/blob/main/infer/src/checkers/Siof.ml).

## Error reporting

Useful analyses have output. Basic printing to stderr or stderr is
good for debugging, but to report a programmer-readable error that is
tied to a source code location, you'll want to use
[`Reporting.log_issue`](pathname:///odoc/next/infer/Absint/Reporting/index.html#val-log_issue).

## By example: interprocedural analysis

Let's assume you have already read and understood the "intraprocedural analysis"
section and have an intraprocedural checker. The abstract interpretation
framework makes it easy to convert your intraprocedural analysis into a
_modular_ interprocedural analysis. Let me emphasize the _modular_ point once
more; global analyses cannot be expressed in this framework.

To make your checker interprocedural, you need to:

1. Define the type of procedure summaries for your analysis and let
registerCheckers.ml know that your checker is interprocedural

2. Add logic for (a) using summaries in your transfer functions and (b)
converting your intraprocedural abstract state to a summary.

A good example to look at here is
[Siof.ml](https://github.com/facebook/infer/blob/main/infer/src/checkers/Siof.ml).
Step (1) is just:

```OCaml
(* in src/checkers/SiofDomain.ml *)
(* note that as a result the type of summaries is the same as the type of domain
   elements *)
module Summary = ...
include Summary


(* in src/backend/Payloads.ml: register the payload of the analyzer *)
type t =
  { ...
  ; siof: SiofDomain.Summary.t option
  ... }


(* in src/backend/registerCheckers.ml *)
let all_checkers = [ ...
  ; {checker= SIOF; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]}
  ... ]
```

Here, the type of the abstract state and the type of the summary are the same,
which makes things easier for us (no logic to convert an abstract state to a
summary).

Part (2a) is
[here](https://github.com/facebook/infer/blob/be4ddc48f6330b7b788d899ce12ca51b4d673530/infer/src/checkers/Siof.ml#L168)
and uses the `analyze_dependency` callback provided by the framework:

```
match analyze_dependency callee_pname with
```

This says: "read the summary for `callee_pname`, possibly computing it
first". You must then add logic for applying the summary to the
current abstract state (often, this is as simple as doing a join).

Because our summary type is the same as the abstract state, part (2b)
here simply consists in return the post computed by the analysis as
the procedure's summary, using `Analyzer.compute_post`.

That's it! We now have an interprocedural analysis.

To go deeper, jump to the [lab
exercise](https://github.com/facebook/infer/blob/main/infer/src/labs/README.md)
and to the [API documentation](internal-API/), e.g. for the
[Absint](pathname:///odoc/next/infer/Absint.html) and
[IR](pathname:///odoc/next/infer/IR.html) modules.

---

### 04 Internal API (`website/docs/04-internal-API.md`)

---
id: internal-API
title: Infer Internal OCaml Modules API
---

Browse the generated documentation for Infer's OCaml code [here](pathname:///odoc/next/infer/infer.html).

You can also generate these pages from within an Infer repository with `make doc`.

---

### All Categories (`website/docs/all-categories.md`)

---
title: List of all categories of issue types
---

Here are all the categories that issue types might belong to in Infer. Some issue types have no associated category at the moment. This usually indicates that the issue type is not yet mature enough to be used.

## Concurrency

Concurrent accesses to the same resource conflict in a way that can give incorrect results, block progress, or result in undefined behaviour.

Issue types in this category:
- [DEADLOCK](/docs/next/all-issue-types#deadlock)
- [GUARDEDBY_VIOLATION](/docs/next/all-issue-types#guardedby_violation)
- [INTERFACE_NOT_THREAD_SAFE](/docs/next/all-issue-types#interface_not_thread_safe)
- [LOCK_CONSISTENCY_VIOLATION](/docs/next/all-issue-types#lock_consistency_violation)
- [STATIC_CONSTRUCTOR_STALL](/docs/next/all-issue-types#static_constructor_stall)
- [THREAD_SAFETY_VIOLATION](/docs/next/all-issue-types#thread_safety_violation)

## Logic error

Something that does not make sense and the sign of a potential programming error.

Issue types in this category:
- [DEAD_STORE](/docs/next/all-issue-types#dead_store)
- [PULSE_TRANSITIVE_ACCESS](/docs/next/all-issue-types#pulse_transitive_access)

## Memory error

Incorrect handling of pointers that isn't a null pointer dereference, but can still result in undefined behaviour and crashes.

Issue types in this category:
- [CXX_REF_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#cxx_ref_captured_in_block)
- [CXX_STRING_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#cxx_string_captured_in_block)
- [NIL_MESSAGING_TO_NON_POD](/docs/next/all-issue-types#nil_messaging_to_non_pod)
- [NIL_MESSAGING_TO_NON_POD_LATENT](/docs/next/all-issue-types#nil_messaging_to_non_pod_latent)
- [NSSTRING_INTERNAL_PTR_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#nsstring_internal_ptr_captured_in_block)
- [PULSE_REFERENCE_STABILITY](/docs/next/all-issue-types#pulse_reference_stability)
- [PULSE_UNINITIALIZED_VALUE](/docs/next/all-issue-types#pulse_uninitialized_value)
- [STACK_VARIABLE_ADDRESS_ESCAPE](/docs/next/all-issue-types#stack_variable_address_escape)
- [STATIC_INITIALIZATION_ORDER_FIASCO](/docs/next/all-issue-types#static_initialization_order_fiasco)
- [STRONG_SELF_NOT_CHECKED](/docs/next/all-issue-types#strong_self_not_checked)
- [USE_AFTER_DELETE](/docs/next/all-issue-types#use_after_delete)
- [USE_AFTER_DELETE_LATENT](/docs/next/all-issue-types#use_after_delete_latent)
- [USE_AFTER_FREE](/docs/next/all-issue-types#use_after_free)
- [USE_AFTER_FREE_LATENT](/docs/next/all-issue-types#use_after_free_latent)
- [USE_AFTER_LIFETIME](/docs/next/all-issue-types#use_after_lifetime)
- [USE_AFTER_LIFETIME_LATENT](/docs/next/all-issue-types#use_after_lifetime_latent)
- [VECTOR_INVALIDATION](/docs/next/all-issue-types#vector_invalidation)
- [VECTOR_INVALIDATION_LATENT](/docs/next/all-issue-types#vector_invalidation_latent)

## Null pointer dereference

The null pointer is used where a valid pointer is required, causing a memory fault and a crash. For example, it is dereferenced.

Issue types in this category:
- [BLOCK_PARAMETER_NOT_NULL_CHECKED](/docs/next/all-issue-types#block_parameter_not_null_checked)
- [COMPARED_TO_NULL_AND_DEREFERENCED](/docs/next/all-issue-types#compared_to_null_and_dereferenced)
- [MISSING_NULLABILITY_ANNOTATION](/docs/next/all-issue-types#missing_nullability_annotation)
- [MISSING_NULLABILITY_ANNOTATION_PULSE](/docs/next/all-issue-types#missing_nullability_annotation_pulse)
- [NIL_BLOCK_CALL](/docs/next/all-issue-types#nil_block_call)
- [NIL_BLOCK_CALL_LATENT](/docs/next/all-issue-types#nil_block_call_latent)
- [NULLPTR_DEREFERENCE](/docs/next/all-issue-types#nullptr_dereference)
- [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS](/docs/next/all-issue-types#nullptr_dereference_in_nullsafe_class)
- [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS_LATENT](/docs/next/all-issue-types#nullptr_dereference_in_nullsafe_class_latent)
- [NULLPTR_DEREFERENCE_LATENT](/docs/next/all-issue-types#nullptr_dereference_latent)
- [SWIFT_NPE](/docs/next/all-issue-types#swift_npe)
- [SWIFT_NPE_LATENT](/docs/next/all-issue-types#swift_npe_latent)

## Perf regression

Unnecessary (or blocking) computation is performed, potentially causing a performance or responsiveness regression.

Issue types in this category:
- [CHECKERS_ALLOCATES_MEMORY](/docs/next/all-issue-types#checkers_allocates_memory)
- [CHECKERS_CALLS_EXPENSIVE_METHOD](/docs/next/all-issue-types#checkers_calls_expensive_method)
- [CONFIG_IMPACT](/docs/next/all-issue-types#config_impact)
- [INEFFICIENT_KEYSET_ITERATOR](/docs/next/all-issue-types#inefficient_keyset_iterator)
- [IPC_ON_UI_THREAD](/docs/next/all-issue-types#ipc_on_ui_thread)
- [LOCK_ON_UI_THREAD](/docs/next/all-issue-types#lock_on_ui_thread)
- [PULSE_CONST_REFABLE](/docs/next/all-issue-types#pulse_const_refable)
- [PULSE_READONLY_SHARED_PTR_PARAM](/docs/next/all-issue-types#pulse_readonly_shared_ptr_param)
- [PULSE_UNNECESSARY_COPY](/docs/next/all-issue-types#pulse_unnecessary_copy)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment_const)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment_movable)
- [PULSE_UNNECESSARY_COPY_INTERMEDIATE](/docs/next/all-issue-types#pulse_unnecessary_copy_intermediate)
- [PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_intermediate_const)
- [PULSE_UNNECESSARY_COPY_MOVABLE](/docs/next/all-issue-types#pulse_unnecessary_copy_movable)
- [PULSE_UNNECESSARY_COPY_OPTIONAL](/docs/next/all-issue-types#pulse_unnecessary_copy_optional)
- [PULSE_UNNECESSARY_COPY_OPTIONAL_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_optional_const)
- [PULSE_UNNECESSARY_COPY_RETURN](/docs/next/all-issue-types#pulse_unnecessary_copy_return)
- [PULSE_UNNECESSARY_COPY_THRIFT_ASSIGNMENT](/docs/next/all-issue-types#pulse_unnecessary_copy_thrift_assignment)
- [REGEX_OP_ON_UI_THREAD](/docs/next/all-issue-types#regex_op_on_ui_thread)
- [STRICT_MODE_VIOLATION](/docs/next/all-issue-types#strict_mode_violation)

## Resource leak

A resource (for example memory, or a file descriptor) has been manually allocated but not released, possibly creating memory pressure over time or even incorrect results.

Issue types in this category:
- [CAPTURED_STRONG_SELF](/docs/next/all-issue-types#captured_strong_self)
- [CHECKERS_FRAGMENT_RETAINS_VIEW](/docs/next/all-issue-types#checkers_fragment_retains_view)
- [MEMORY_LEAK_C](/docs/next/all-issue-types#memory_leak_c)
- [MEMORY_LEAK_CPP](/docs/next/all-issue-types#memory_leak_cpp)
- [MIXED_SELF_WEAKSELF](/docs/next/all-issue-types#mixed_self_weakself)
- [PULSE_RESOURCE_LEAK](/docs/next/all-issue-types#pulse_resource_leak)
- [PULSE_UNAWAITED_AWAITABLE](/docs/next/all-issue-types#pulse_unawaited_awaitable)
- [PULSE_UNFINISHED_BUILDER](/docs/next/all-issue-types#pulse_unfinished_builder)
- [RETAIN_CYCLE](/docs/next/all-issue-types#retain_cycle)
- [RETAIN_CYCLE_NO_WEAK_INFO](/docs/next/all-issue-types#retain_cycle_no_weak_info)
- [SELF_IN_BLOCK_PASSED_TO_INIT](/docs/next/all-issue-types#self_in_block_passed_to_init)

## Runtime exception

A runtime exception can occur and potentially crash the program.

Issue types in this category:
- [BAD_ARG](/docs/next/all-issue-types#bad_arg)
- [BAD_ARG_LATENT](/docs/next/all-issue-types#bad_arg_latent)
- [BAD_GENERATOR](/docs/next/all-issue-types#bad_generator)
- [BAD_GENERATOR_LATENT](/docs/next/all-issue-types#bad_generator_latent)
- [BAD_KEY](/docs/next/all-issue-types#bad_key)
- [BAD_KEY_LATENT](/docs/next/all-issue-types#bad_key_latent)
- [BAD_MAP](/docs/next/all-issue-types#bad_map)
- [BAD_MAP_LATENT](/docs/next/all-issue-types#bad_map_latent)
- [BAD_RECORD](/docs/next/all-issue-types#bad_record)
- [BAD_RECORD_LATENT](/docs/next/all-issue-types#bad_record_latent)
- [INFINITE_LOOP](/docs/next/all-issue-types#infinite_loop)
- [INFINITE_RECURSION](/docs/next/all-issue-types#infinite_recursion)
- [MISSING_REQUIRED_PROP](/docs/next/all-issue-types#missing_required_prop)
- [MUTUAL_RECURSION_CYCLE](/docs/next/all-issue-types#mutual_recursion_cycle)
- [NIL_INSERTION_INTO_COLLECTION](/docs/next/all-issue-types#nil_insertion_into_collection)
- [NIL_INSERTION_INTO_COLLECTION_LATENT](/docs/next/all-issue-types#nil_insertion_into_collection_latent)
- [NO_MATCHING_BRANCH_IN_TRY](/docs/next/all-issue-types#no_matching_branch_in_try)
- [NO_MATCHING_BRANCH_IN_TRY_LATENT](/docs/next/all-issue-types#no_matching_branch_in_try_latent)
- [NO_MATCHING_CASE_CLAUSE](/docs/next/all-issue-types#no_matching_case_clause)
- [NO_MATCHING_CASE_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_case_clause_latent)
- [NO_MATCHING_ELSE_CLAUSE](/docs/next/all-issue-types#no_matching_else_clause)
- [NO_MATCHING_ELSE_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_else_clause_latent)
- [NO_MATCHING_FUNCTION_CLAUSE](/docs/next/all-issue-types#no_matching_function_clause)
- [NO_MATCHING_FUNCTION_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_function_clause_latent)
- [NO_MATCH_OF_RHS](/docs/next/all-issue-types#no_match_of_rhs)
- [NO_MATCH_OF_RHS_LATENT](/docs/next/all-issue-types#no_match_of_rhs_latent)
- [NO_TRUE_BRANCH_IN_IF](/docs/next/all-issue-types#no_true_branch_in_if)
- [NO_TRUE_BRANCH_IN_IF_LATENT](/docs/next/all-issue-types#no_true_branch_in_if_latent)
- [NULL_ARGUMENT](/docs/next/all-issue-types#null_argument)
- [NULL_ARGUMENT_LATENT](/docs/next/all-issue-types#null_argument_latent)
- [OPTIONAL_EMPTY_ACCESS](/docs/next/all-issue-types#optional_empty_access)
- [OPTIONAL_EMPTY_ACCESS_LATENT](/docs/next/all-issue-types#optional_empty_access_latent)
- [PULSE_ASSERTION_ERROR](/docs/next/all-issue-types#pulse_assertion_error)
- [PULSE_CANNOT_INSTANTIATE_ABSTRACT_CLASS](/docs/next/all-issue-types#pulse_cannot_instantiate_abstract_class)
- [PULSE_DICT_MISSING_KEY](/docs/next/all-issue-types#pulse_dict_missing_key)
- [PULSE_DYNAMIC_TYPE_MISMATCH](/docs/next/all-issue-types#pulse_dynamic_type_mismatch)
- [PULSE_UNINITIALIZED_CONST](/docs/next/all-issue-types#pulse_uninitialized_const)
- [PULSE_UNINITIALIZED_METHOD](/docs/next/all-issue-types#pulse_uninitialized_method)

## Sensitive data flow

Sensitive data is flowing where it shouldn't.

Issue types in this category:
- [DATA_FLOW_TO_SINK](/docs/next/all-issue-types#data_flow_to_sink)
- [LINEAGE_FLOW](/docs/next/all-issue-types#lineage_flow)
- [SCOPE_LEAKAGE](/docs/next/all-issue-types#scope_leakage)
- [SENSITIVE_DATA_FLOW](/docs/next/all-issue-types#sensitive_data_flow)
- [TAINT_ERROR](/docs/next/all-issue-types#taint_error)

## Ungated code

Code must be under a gating mechanism but isn't.

Issue types in this category:
- [CONFIG_IMPACT_STRICT](/docs/next/all-issue-types#config_impact_strict)

## User defined property

A user defined (custom) property is violated.

Issue types in this category:
- [CHECKERS_ANNOTATION_REACHABILITY_ERROR](/docs/next/all-issue-types#checkers_annotation_reachability_error)
- [TOPL_ERROR](/docs/next/all-issue-types#topl_error)
- [TOPL_ERROR_LATENT](/docs/next/all-issue-types#topl_error_latent)

---

### All Checkers (`website/docs/all-checkers.md`)

---
title: List of all checkers
hide_table_of_contents: true
---

Here is an overview of the checkers currently available in Infer.

## Annotation Reachability

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`.

[Visit here for more information.](/docs/next/checker-annotation-reachability)

## Buffer Overrun Analysis (InferBO)

InferBO is a detector for out-of-bounds array accesses.

**\*\*\*DEPRECATED\*\*\*** Use Pulse instead.

[Visit here for more information.](/docs/next/checker-bufferoverrun)

## Config Gating

Determines which config flags gate the execution of each line of code.

[Visit here for more information.](/docs/next/checker-config-gating)

## Config Impact Analysis

[EXPERIMENTAL] Collects function that are called without config checks.

[Visit here for more information.](/docs/next/checker-config-impact-analysis)

## Cost: Complexity Analysis

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`.

[Visit here for more information.](/docs/next/checker-cost)

## Static Constructor Stall Checker

Detect if dispatch_once is called from a static constructor.

[Visit here for more information.](/docs/next/checker-static-constructor-stall-checker)

## Fragment Retains View

Detects when Android fragments are not explicitly nullified before becoming unreachable.

[Visit here for more information.](/docs/next/checker-fragment-retains-view)

## Impurity

Detects functions with potential side-effects. Same as "purity", but implemented on top of Pulse.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

[Visit here for more information.](/docs/next/checker-impurity)

## Inefficient keySet Iterator

Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly.

[Visit here for more information.](/docs/next/checker-inefficient-keyset-iterator)

## Lineage

Computes a dataflow graph

[Visit here for more information.](/docs/next/checker-lineage)

## Litho "Required Props"

Checks that all non-optional `@Prop`s have been specified when constructing Litho components.

[Visit here for more information.](/docs/next/checker-litho-required-props)

## Liveness

Detection of dead stores and unused variables.

[Visit here for more information.](/docs/next/checker-liveness)

## Loop Hoisting

Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

[Visit here for more information.](/docs/next/checker-loop-hoisting)

## Parameter Not Null Checked

An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first.

[Visit here for more information.](/docs/next/checker-parameter-not-null-checked)

## Pulse

General-purpose memory and value analysis engine.

[Visit here for more information.](/docs/next/checker-pulse)

## Purity

Detects pure (side-effect-free) functions. A different implementation of "impurity".

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

[Visit here for more information.](/docs/next/checker-purity)

## RacerD

Thread safety analysis.

[Visit here for more information.](/docs/next/checker-racerd)

## Resource Leak Lab Exercise

Toy checker for the "resource leak" write-your-own-checker exercise.

[Visit here for more information.](/docs/next/checker-resource-leak-lab)

## SIL validation

This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL.

[Visit here for more information.](/docs/next/checker-sil-validation)

## Static Initialization Order Fiasco

Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

[Visit here for more information.](/docs/next/checker-siof)

## Scope Leakage

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).

[Visit here for more information.](/docs/next/checker-scope-leakage)

## Self in Block

An Objective-C-specific analysis to detect when a block captures `self`.

[Visit here for more information.](/docs/next/checker-self-in-block)

## Starvation

Detect various kinds of situations when no progress is being made because of concurrency errors.

[Visit here for more information.](/docs/next/checker-starvation)

## Swift/Obj-C Nullability

Detects missing nullability annotations in Objective-C methods called from Swift, which can lead to runtime crashes via Implicitly Unwrapped Optionals.

[Visit here for more information.](/docs/next/checker-swift-objc-nullability)

## Topl

Detect errors based on user-provided state machines describing temporal properties over multiple objects.

[Visit here for more information.](/docs/next/checker-topl)

---

### All Issue Types (`website/docs/all-issue-types.md`)

---
title: List of all issue types
---

Here is an overview of the issue types currently reported by Infer.

## ARBITRARY_CODE_EXECUTION_UNDER_LOCK

*Reported as "Arbitrary Code Execution Under lock" by [starvation](/docs/next/checker-starvation).*

A call that may execute arbitrary code (such as registered, or chained, callbacks) is made while holding a lock.
This code may deadlock whenever the callbacks obtain locks themselves, so it is an unsafe pattern.

Example:
```java
  SettableFuture future = null;

  public void callFutureSet() {
    future.set(null);
  }

  // synchronized means it's taking a lock implicitly
  public synchronized void example_of_bad_pattern() {
    callFutureSet(); // <- issue reported here
  }

  // If the call is made while holding multiple locks, the warning
  // will be issued only at the innermost lock acquisition. Here we
  // report in example_of_bad_pattern but we won't report below.
  public void nested_bad_pattern_no_report(Object o) {
    synchronized (o) {
      example_of_bad_pattern(); // <- no issue reported
    }
  }
```

## BAD_ARG

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Arg" by [pulse](/docs/next/checker-pulse).*

Bad arg in Erlang: Reports an error when the type of an argument is wrong or the argument is badly formed. Corresponds to the `badarg` error in the Erlang runtime.

For example, trying to concatenate the number `3` with  the list `[1,2]` gives `badarg` error because `3` is not a list.
```erlang
f() ->
    3 ++ [1,2]. // badarg error
```

Note that although the first argument needs to be a list, the second argument may not be a list.
For instance, concatenating [1,2] with the number `3` raises no error in Erlang.
```erlang
g() ->
    [1,2] ++ 3. // no error. Result: [1,2|3]
```

## BAD_ARG_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Arg Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_ARG](#bad_arg). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BAD_GENERATOR

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Generator" by [pulse](/docs/next/checker-pulse).*

Bad generator in Erlang: Reports an error when a wrong type is used in a generator. Corresponds to the `bad_generator` error in the Erlang runtime.

For example:
```erlang
list_instead_of_map() ->
    M = [],
    [{K, V} || K := V <- M]
```

## BAD_GENERATOR_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Generator Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_GENERATOR](#bad_generator). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BAD_KEY

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Key" by [pulse](/docs/next/checker-pulse).*

Bad key in Erlang: Reports an error when trying to access or update a non-existing key in a map. Corresponds to the `{badkey,K}` error in the Erlang runtime.

For example, trying to update the key `2` in `M` gives `{badkey,2}` error because `2` is not present as a key in `M`.
```erlang
f() ->
    M = #{},
    M#{2 := 3}.
```

Note that maps currently use a recency abstraction, meaning that only the most recent key/value is tracked.
Therefore, if a map is non-empty and we try to access a key other than the one we track, we just assume that it is there to avoid false positives.

## BAD_KEY_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Key Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_KEY](#bad_key). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BAD_MAP

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Map" by [pulse](/docs/next/checker-pulse).*

Bad map in Erlang: Reports an error when trying to access or update a key for a term that is not a map. Corresponds to the `{badmap,...}` error in the Erlang runtime.

For example, trying to update `L` as if it was a map gives `{badmap,[1,2,3]}` error because `L` is actually a list (`[1,2,3]`).
```erlang
f() ->
    L = [1,2,3],
    L#{1 => 2}.
```

## BAD_MAP_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Map Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_MAP](#bad_map). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BAD_RECORD

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Record" by [pulse](/docs/next/checker-pulse).*

Bad record in Erlang: Reports an error when trying to access or update a record with the wrong name. Corresponds to the `{badrecord,Name}` error in the Erlang runtime.

For example, accessing `R` as a `person` record gives `{badrecord,person}` error because `R` is `rabbit` (even though both share the `name` field).
```erlang
-record(person, {name, phone}).
-record(rabbit, {name, color}).

f() ->
    R = #rabbit{name = "Bunny", color = "Brown"},
    R#person.name.
```

## BAD_RECORD_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Bad Record Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_RECORD](#bad_record). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BAD_RETURN

*Reported as "Bad Return" by [pulse](/docs/next/checker-pulse).*

Bad return in Erlang: The dynamic type of a returned value disagrees with the static type given in the spec.

For example, this function returns an integer, while the spec says it returns an atom.
```erlang
-spec f() -> atom().
f() -> 1.
```

Note that this will *not* lead to a runtime error when running the Erlang program.

## BAD_RETURN_LATENT

*Reported as "Bad Return Latent" by [pulse](/docs/next/checker-pulse).*

A latent [BAD_RETURN](#bad_return). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## BLOCK_PARAMETER_NOT_NULL_CHECKED

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Block Parameter Not Null Checked" by [parameter-not-null-checked](/docs/next/checker-parameter-not-null-checked).*

This error type is reported only in Objective-C/Objective-C++. It happens when a method has a block as a parameter,
and the block is executed in the method's body without checking it for `nil` first. If a `nil` block is passed to
the method, then this will cause a crash. For example:

```objectivec
- (void)uploadTaskWithRequest:(NSURLRequest*)urlRequest
                       fromFile:(NSURL*)fileURL
                       delegate:(id)delegate
                  delegateQueue:(NSOperationQueue*)delegateQueue
                     completion:(void (^)())completion {
     ...
    completion();
}
```

**Action**:
Possible solutions are adding a check for `nil`, or making sure that the method
is not ever called with `nil`. When an argument will never be `nil`, you can add
the annotation `nonnull` to the argument's type, to tell Infer (and the type
system), that the argument won't be `nil`. This will silence the warning.

## BUFFER_OVERRUN_L1

*Reported as "Buffer Overrun L1" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

This is reported when outside of buffer bound is accessed.  It can corrupt memory and may introduce
security issues in C/C++.

For example, `int a[3]; a[5] = 42;` generates a `BUFFER_OVERRUN_L1` on `a[5] = 42;`.

Buffer overrun reports fall into several "buckets" corresponding to the expected precision of the
report.  The higher the number, the more likely it is to be a false positive.

*   `L1`: The most faithful report, when it *must* be unsafe.  For example, array size: `[3,3]`,
    offset: `[5,5]`.

*   `L2`: Less faithful report than `L1`, when it *may* be unsafe.  For example, array size:`[3,3]`,
    offset: `[0,5]`.  Note that the offset may be a safe value in the real execution, i.e. safe when
    0, 1, or 2; unsafe when 3, 4, or 5.

*   `L5`: The least faithful report, when there is an interval top.  For example, array size:
    `[3,3]`, offset: `[-oo,+oo]`.

*   `L4`: More faithful report than `L5`, when there is an infinity value.  For example, array size:
    `[3,3]`, offset: `[0, +oo]`.

*   `L3`: The reports that are not included in the above cases.

*   `S2`: An array access is unsafe by symbolic values.  For example, array size: `[n,n]`, offset
    `[n,+oo]`.

*   `U5`: An array access is unsafe by unknown values, which are usually from unknown function
    calls.

## BUFFER_OVERRUN_L2

*Reported as "Buffer Overrun L2" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## BUFFER_OVERRUN_L3

*Reported as "Buffer Overrun L3" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## BUFFER_OVERRUN_L4

*Reported as "Buffer Overrun L4" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## BUFFER_OVERRUN_L5

*Reported as "Buffer Overrun L5" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## BUFFER_OVERRUN_S2

*Reported as "Buffer Overrun S2" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## BUFFER_OVERRUN_U5

*Reported as "Buffer Overrun U5" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [BUFFER_OVERRUN_L1](#buffer_overrun_l1)
## CAPTURED_STRONG_SELF

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Captured strongSelf" by [self-in-block](/docs/next/checker-self-in-block).*

This check is about when a strong pointer to `self` is captured in a block.
This could lead to retain cycles or unexpected behavior since to avoid retain
cycles one usually uses a local strong pointer or a captured weak pointer instead.

This will happen in one of two cases generally:

1. One uses `weakSelf` but forgot to declare it weak first.

Example:

```objectivec
  __typeof(self) weakSelf = self;
  int (^my_block)(BOOL) = ^(BOOL isTapped) {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    return strongSelf->x;
  };
```

**Action:** Replace the first line with `__weak __typeof(self) weakSelf = self;`.


2. One is using `strongSelf`, declared in a block, in another inner block.
   The retain cycle is avoided in the outer block because `strongSelf` is a
   local variable of the block. If `strongSelf` is used in the inner block,
   then it's not a local variable anymore, but a captured variable.

   Example:

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int (^my_block)() = ^() {
        int x = strongSelf->x;
        ...
      };
      ...
    }
    ...
  };
```

In this example, `strongSelf` is a captured variable of the inner block, and this could cause retain cycles.

**Action:** Use a new pointer to self local to the inner block. In the example:

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int (^my_block)() = ^() {
         __typeof(self) innerStrongSelf = weakSelf;
        int x = innerStrongSelf->x;
        ...
      };
      ...
    }
    ...
  };
```

Or, to improve readability, move the inner block logic into a separate method.

Another solution could be to copy the instance variable that one needs to access inside the inner block to a local variable, and use the local variable instead:

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong typeof(self) strongSelf = weakSelf;
    if (strongSelf) {
      int my_x = strongSelf->x;
      int (^my_block)() = ^() {
        int x = my_x;
        ...
      };
      ...
    }
    ...
  };
```

## CHECKERS_ALLOCATES_MEMORY

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Allocates Memory" by [annotation-reachability](/docs/next/checker-annotation-reachability).*

A method annotated with `@NoAllocation` transitively calls `new`.

Example:

```java
class C implements I {
  @NoAllocation
  void directlyAllocatingMethod() {
    new Object();
  }
}
```

## CHECKERS_ANNOTATION_REACHABILITY_ERROR

*Category: [User defined property](/docs/next/all-categories#user-defined-property). Reported as "Annotation Reachability Error" by [annotation-reachability](/docs/next/checker-annotation-reachability).*

A method annotated with an annotation `@A` transitively calls a method annotated `@B` where the combination of annotations is forbidden (for example, `@UiThread` calling `@WorkerThread`).

## CHECKERS_CALLS_EXPENSIVE_METHOD

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Expensive Method Called" by [annotation-reachability](/docs/next/checker-annotation-reachability).*

A method annotated with `@PerformanceCritical` transitively calls a method annotated `@Expensive`.

Example:

```java
class C {
  @PerformanceCritical
  void perfCritical() {
    expensive();
  }

  @Expensive
  void expensive() {}
}
```

## CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED

*Reported as "Expensive Overrides Unannotated" by [annotation-reachability](/docs/next/checker-annotation-reachability).*

A method annotated with `@Expensive` overrides an un-annotated method.

Example:

```java
interface I {
  void foo();
}

class A implements I {
  @Expensive
  public void foo() {}
}
```

## CHECKERS_FRAGMENT_RETAINS_VIEW

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Fragment Retains View" by [fragment-retains-view](/docs/next/checker-fragment-retains-view).*

This error type is Android-specific. It fires when a `Fragment` type fails to
nullify one or more of its declared `View` fields in `onDestroyView`. In
performance-sensitive applications, a `Fragment` should initialize all `View`'s
in `onCreateView` and nullify them in `onDestroyView`. If a `Fragment` is placed
on the back stack and fails to nullify a `View` in `onDestroyView`, it will
retain a useless reference to that `View` that will not be cleaned up until the
`Fragment` is resumed or destroyed.

Action: Nullify the `View` in question in `onDestroyView`.

## COMPARED_TO_NULL_AND_DEREFERENCED

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Compared To Null And Dereferenced" by [pulse](/docs/next/checker-pulse).*

A pointer that has both been compared to null, which suggests that it could be null, but has also been dereferenced without a null check.
## CONFIG_GATED

*Reported as "Config Gated" by [config-gating](/docs/next/checker-config-gating).*

A call site is gated by one or more config flags. Being gated by config X means
that changing the value of config X can be used to turn off the execution of the
reported code.

## CONFIG_IMPACT

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Config Impact" by [config-impact-analysis](/docs/next/checker-config-impact-analysis).*

Infer reports this issue when an *expensive* function is called without a *config check*.  The
*config* is usually a boolean value that enables experimental new features and it is defined per
application/codebase, e.g. gatekeepers.  To determine whether a function is expensive or not, the
checker relies on modeled functions that are assumed to be expensive, e.g. string operations,
regular expression match, or DB accesses.

Similar to [Cost analysis](/docs/next/checker-cost), this issue type is reported only in
differential mode, i.e. when there are original code and modified one and we can compare Infer's
results on both of them.

For instance, if we have the following code

```java
// version1
foo();
if (config_check){
   bar();
}
```

which is then modified to next

```java
// version2
foo();
if (config_check){
   bar();
}
goo(); // added
```

the analysis would warn the developer that "`goo()` is a newly added function call and it might
cause an unexpected new behavior". However, if we were to add `goo()` right after `bar()`, then
Infer wouldn't warn about it because it is already gated under the `config_check`.

The analysis is inter-procedural: it can reason about impacts by code changes not only inside a
single procedure, but also the impacts that are propagated by function calls. Thus, if we were to
modify `version1` to `version3` below by calling `goo()` in `foo()`,

```java
// version3
void foo(){
   // ....
   goo(); // added
}
```

then the analysis will report a `CONFIG_IMPACT` issue on the ungated call site of `foo()`.

Currently, the analysis supports both Objective-C and Java but not C++.

Action: Make sure the ungated code change is semantically correct and harmless in terms of execution
cost.  If you are not sure, gate it with a new or pre-existing config.

## CONFIG_IMPACT_STRICT

*Category: [Ungated code](/docs/next/all-categories#ungated-code). Reported as "Config Impact Strict" by [config-impact-analysis](/docs/next/checker-config-impact-analysis).*

This is similar to [`CONFIG_IMPACT` issue](#config_impact) but the analysis reports **all** ungated
codes irrespective of whether they are expensive or not.

## CONFIG_UNGATED

*Reported as "Config Ungated" by [config-gating](/docs/next/checker-config-gating).*

A call site is not gated by any config flag. There is no config value that,
if changed, would prevent this code from executing.

## CONFIG_USAGE

*Reported as "Config Usage" by [pulse](/docs/next/checker-pulse).*

Infer reports this issue when a *config* value is used as branch condition in a function.  The
*config* is usually a boolean value that enables experimental new features and it is defined per
application/codebase, e.g. gatekeepers.

For instance, if we have the following code

```cpp
void foo() {
  if(config_check("my_new_feature")){ ... }
}
```

then analysis would provide information that "the function `foo` uses the config `my_new_feature` as
branch condition".

Note: This type of issue is only for providing semantic information, rather than warning or
reporting actual problem.

## CONSTANT_ADDRESS_DEREFERENCE

*Reported as "Constant Address Dereference" by [pulse](/docs/next/checker-pulse).*

This is reported when an address at an absolute location, e.g. 1234,
is dereferenced. It is a more general version of the
[`NULLPTR_DEREFERENCE`](#nullptr_dereference) error type that is
reported when the address is a constant other than zero.

For example, `int *p = (int *) 123; *p = 42;` generates a `CONSTANT_ADDRESS_DEREFERENCE` on `*p = 42;`.

For more information see the [`NULLPTR_DEREFERENCE`](#nullptr_dereference) issue type.

## CONSTANT_ADDRESS_DEREFERENCE_LATENT

*Reported as "Constant Address Dereference Latent" by [pulse](/docs/next/checker-pulse).*

A latent [CONSTANT_ADDRESS_DEREFERENCE](#constant_address_dereference). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## CXX_REF_CAPTURED_IN_BLOCK

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "C++ Reference Captured in Block" by [self-in-block](/docs/next/checker-self-in-block).*

This check flags when a C++ reference is captured in an escaping block.
This means that the block will be leaving the current scope, i.e. it is
not annotated with `__attribute__((noescape))`.

Example:

```
- (void)ref_captured_in_escaping_block_bad:(int&)y {
  dispatch_async(dispatch_get_main_queue(), ^{
    int a = y;
    ...
  });
  ...;
}
```

This could cause crashes because C++ references are not managed pointers
(like ARC pointers) and so the referent is likely to be gone if the block
dereferences it later.

## CXX_STRING_CAPTURED_IN_BLOCK

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "C++ String Captured in Block" by [self-in-block](/docs/next/checker-self-in-block).*

This check flags when an internal pointer of a local variable of type `std::string` is captured in an escaping block.
This means that the block will be leaving the current scope, i.e. it is
not annotated with `__attribute__((noescape))`.

Example:

```
  std::string fullName;
  const char* c = fullName.c_str();
  dispatch_async(dispatch_get_main_queue(), ^{
    const char* c1 = c;
  });
```

This could cause crashes because the variable is likely to be freed when the code is executed, leaving the pointer dangling.

## DATA_FLOW_TO_SINK

*Category: [Sensitive data flow](/docs/next/all-categories#sensitive-data-flow). Reported as "Data Flow to Sink" by [pulse](/docs/next/checker-pulse).*

A flow of data was detected to a sink.
## DEADLOCK

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "Deadlock" by [starvation](/docs/next/checker-starvation).*

This error is currently reported in Java. A deadlock occurs when two distinct
threads try to acquire two locks in reverse orders. The following code
illustrates a textbook example. Of course, in real deadlocks, the lock
acquisitions may be separated by deeply nested call chains.

```java
  public void lockAThenB() {
    synchronized(lockA) {
      synchronized(lockB) {
       // do something with both resources
      }
    }
  }

  public void lockBThenA() {
    synchronized(lockB) {
      synchronized(lockA) {
       // do something with both resources
      }
    }
  }
```

The standard solution to a deadlock is to fix an order of lock acquisition and
adhere to that order in all cases. Another solution may be to shrink the
critical sections (i.e., the code executing under lock) to the minimum required.

Old-style containers such as `Vector` are synchronized on the object monitor,
which means that deadlocks can occur even without explicit synchronisation on
both threads. For instance:

```java
  public void lockAThenAddToVector() {
    synchronized(lockA) {
      vector.add(object);
    }
  }

  public void lockVectorThenA() {
    synchronized(vector) {
      synchronized(lockA) {
       // do something with both resources
      }
    }
  }
```

Infer has support for detecting these deadlocks too.

To suppress reports of deadlocks in a method `m()` use the
`@SuppressLint("DEADLOCK")` annotation, as follows:

```java
  import android.annotation.SuppressLint;

  @SuppressLint("DEADLOCK")
  public void m() {
  ...
  }
```

## DEAD_STORE

*Category: [Logic error](/docs/next/all-categories#logic-error). Reported as "Dead Store" by [liveness](/docs/next/checker-liveness).*

This error is reported in C++. It fires when the value assigned to a variables
is never used (e.g., `int i = 1; i = 2; return i;`).

## EXECUTION_TIME_COMPLEXITY_INCREASE

*Reported as "Execution Time Complexity Increase" by [cost](/docs/next/checker-cost).*

Infer reports this issue when the execution time complexity of a
program increases in degree: e.g. from constant to linear or from
logarithmic to quadratic. This issue type is only reported in
differential mode: i.e when we are comparing the cost analysis results of
two runs of infer on a file. Check out examples in [here](/docs/next/checker-cost#examples-execution-cost).



## EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD

*Reported as "Execution Time Complexity Increase Ui Thread" by [cost](/docs/next/checker-cost).*

Infer reports this issue when the execution time complexity of the procedure increases in degree **and** the procedure runs on the UI (main) thread.

Infer considers a method as running on the UI thread whenever:

- The method, one of its overrides, its class, or an ancestral class, is
  annotated with `@UiThread`.
- The method, or one of its overrides is annotated with `@OnEvent`, `@OnClick`,
  etc.
- The method or its callees call a `Litho.ThreadUtils` method such as
  `assertMainThread`.


## EXECUTION_TIME_UNREACHABLE_AT_EXIT

*Reported as "Execution Time Unreachable At Exit" by [cost](/docs/next/checker-cost).*

This issue type indicates that the program's execution doesn't reach
the exit node (where our analysis computes the final cost of the
procedure). Hence, we cannot compute a static bound for the procedure.


Examples:
```java
void exit_unreachable() {
  exit(0); // modeled as unreachable
}

void infeasible_path_unreachable() {
    Preconditions.checkState(false); // like assert false, state pruned to bottom
}
```

## EXPENSIVE_EXECUTION_TIME

*Reported as "Expensive Execution Time" by [cost](/docs/next/checker-cost).*

\[EXPERIMENTAL\] This warning indicates that the procedure has non-constant and non-top execution cost. By default, this issue type is disabled. To enable it, set `enabled=true` in [costKind.ml](https://github.com/facebook/infer/blob/main/infer/src/base/costKind.ml#L55).

For instance, a simple example where we report this issue is a function with linear cost:
```java
int sum_linear(ArrayList<Integer> list){
 int sum = 0;
 for (Integer el: list){
   sum += el;
 }
 return sum;
}
```

## EXPENSIVE_LOOP_INVARIANT_CALL

*Reported as "Expensive Loop Invariant Call" by [loop-hoisting](/docs/next/checker-loop-hoisting).*

We report this issue type when a function is [loop-invariant](/docs/next/all-issue-types#invariant_call) and also expensive (i.e. at least has linear complexity as determined by the [cost](/docs/next/checker-cost) analysis).

```java
int incr(int x) {
  return x + 1;
}

// incr will not be hoisted since it is cheap(constant time)
void foo_linear(int size) {
  int x = 10;
  for (int i = 0; i < size; i++) {
    incr(x); // constant call, don't hoist
  }
}

// call to foo_linear will be hoisted since it is expensive(linear in size).
void symbolic_expensive_hoist(int size) {
  for (int i = 0; i < size; i++) {
    foo_linear(size); // hoist
  }
}
```

## GUARDEDBY_VIOLATION

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "GuardedBy Violation" by [racerd](/docs/next/checker-racerd).*

A field annotated with `@GuardedBy` is being accessed by a call-chain that starts at a non-private method without synchronization.

Example:

```java
class C {
  @GuardedBy("this")
  String f;

  void foo(String s) {
    f = s; // unprotected access here
  }
}
```

Action: Protect the offending access by acquiring the lock indicated by the `@GuardedBy(...)`.

## IMPURE_FUNCTION

*Reported as "Impure Function" by [impurity](/docs/next/checker-impurity).*

This issue type indicates impure functions. For instance, below functions would be marked as impure:
```java
void makeAllZero_impure(ArrayList<Foo> list) {
  Iterator<Foo> listIterator = list.iterator();
  while (listIterator.hasNext()) {
    Foo foo = listIterator.next();
    foo.x = 0;
  }
}
```

## INEFFICIENT_KEYSET_ITERATOR

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Inefficient Keyset Iterator" by [inefficient-keyset-iterator](/docs/next/checker-inefficient-keyset-iterator).*

This issue is raised when
- iterating over a HashMap with `keySet()` iterator
- looking up the key each time

Example:

```java
void inefficient_loop_bad(HashMap<String, Integer> testMap) {
 for (String key : testMap.keySet()) {
   Integer value = testMap.get(key); // extra look-up cost
   foo(key, value);
 }
}
```

**Action**:

Instead, it is more efficient to iterate over the loop with `entrySet` which returns key-vaue pairs and gets rid of the hashMap lookup.
 
```java
void efficient_loop_ok(HashMap<String, Integer> testMap) {
  for (Map.Entry<String, Integer> entry : testMap.entrySet()) {
    String key = entry.getKey();
    Integer value = entry.getValue();
    foo(key, value);
  }
}
```

## INFERBO_ALLOC_IS_BIG

*Reported as "Alloc Is Big" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

`malloc` is passed a large constant value (>=10^6). For example, `int n = 1000000; malloc(n);` generates `INFERBO_ALLOC_IS_BIG` on `malloc(n)`.

Action: Fix the size argument or make sure it is really needed.
## INFERBO_ALLOC_IS_NEGATIVE

*Reported as "Alloc Is Negative" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

`malloc` is called with a negative size. For example, `int n = 3 - 5; malloc(n);` generates `INFERBO_ALLOC_IS_NEGATIVE` on `malloc(n)`.

Action: Fix the size argument.
## INFERBO_ALLOC_IS_ZERO

*Reported as "Alloc Is Zero" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

`malloc` is called with a zero size. For example, `int n = 3 - 3; malloc(n);` generates `INFERBO_ALLOC_IS_ZERO` on `malloc(n)`.

Action: Fix the size argument.
## INFERBO_ALLOC_MAY_BE_BIG

*Reported as "Alloc May Be Big" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

`malloc` *may* be called with a large value. For example, `int n = b ? 3 : 1000000; malloc(n);` generates `INFERBO_ALLOC_MAY_BE_BIG` on `malloc(n)`.

Action: Fix the size argument or add a bound checking, e.g. `if (n < A_SMALL_NUMBER) { malloc(n); }`.
## INFERBO_ALLOC_MAY_BE_NEGATIVE

*Reported as "Alloc May Be Negative" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

`malloc` *may* be called with a negative value. For example, `int n = b ? 3 : -5; malloc(n);` generates `INFERBO_ALLOC_MAY_BE_NEGATIVE` on `malloc(n)`.

Action: Fix the size argument or add a bound checking, e.g. `if (n > 0) { malloc(n); }`.
## INFINITE_EXECUTION_TIME

*Reported as "Infinite Execution Time" by [cost](/docs/next/checker-cost).*

This warning indicates that Infer was not able to determine a static
upper bound on the execution cost of the procedure. By default, this
issue type is disabled.

### Example 1: T due to expressivity

For instance, Inferbo's interval analysis is limited to affine
expressions. Hence, we can't statically estimate an upper bound on the
below example and obtain T(unknown) cost:
```java
// Expected: square root(x), got T
void square_root_FP(int x) {
 int i = 0;
 while (i * i < x) {
   i++;
 }
}
```
### Example 2: T due to unmodeled calls 
Another common case where we get T cost is when Infer cannot statically determine the range of values for loop bounds. For instance, 

```java
void loop_over_charArray_FP(StringBuilder builder, String input) {
  for (Character c : input.toCharArray()) {}
}
```
Here, Infer does not have any InferBo models for the range of values returned by `String.toCharArray`, hence it cannot determine that we will be iterating over a char array in the size of `input` string.  

To teach InferBo about such library calls, they should be semantically modeled in [InferBo](https://github.com/facebook/infer/blob/main/infer/src/bufferoverrun/bufferOverrunModels.ml).


### Example 3: T due to calling another T-costed function
Since the analysis is inter-procedural, another example we can have T cost is if at least one of the callees has T cost.

```java
// Expected: constant, got T
void call_top_cost_FP() {
 square_root_FP(1); // square_root_FP has Top cost
}
```


## INFINITE_LOOP

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Infinite Loop" by [pulse](/docs/next/checker-pulse).*

An infinite loop has been detected. The program won't terminate.

Example of recursive function:


```C
void loop(int x) {
  int y = 1;
  while (x != 3)
    y++;
}
```

## INFINITE_RECURSION

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Infinite Recursion" by [pulse](/docs/next/checker-pulse).*

A special case of [MUTUAL_RECURSION_CYCLE](#mutual_recursion_cycle) where we detected that the recursive call is made with the exact same values, which guarantees an infinite recursion.
## INTEGER_OVERFLOW_L1

*Reported as "Integer Overflow L1" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

This is reported when integer overflow occurred by integer operations such as addition, subtraction,
and multiplication. For example, `int n = INT_MAX; int m = n + 3;` generates a INTEGER_OVERFLOW_L1
on `n + 3`.

Integer overflows reports fall into several "buckets" corresponding to the expected precision of the
report. The higher the number, the more likely it is to be a false positive.

*   `L1`: The most faithful report, when it *must* be unsafe.  For example,
    `[2147483647,2147483647] + [1,1]` in 32-bit signed integer type.

*   `L2`: Less faithful report than `L1`, when it *may* be unsafe.  For example,
    `[2147483647,2147483647] + [0,1]` in 32-bit signed integer type.  Note that the integer of RHS
    can be 0, which is safe.

*   `L5`: The reports that are not included in the above cases.

*   `U5`: A binary integer operation is unsafe by unknown values, which are usually from unknown
    function calls.

## INTEGER_OVERFLOW_L2

*Reported as "Integer Overflow L2" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)
## INTEGER_OVERFLOW_L5

*Reported as "Integer Overflow L5" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)
## INTEGER_OVERFLOW_U5

*Reported as "Integer Overflow U5" by [bufferoverrun](/docs/next/checker-bufferoverrun).*

See [INTEGER_OVERFLOW_L1](#integer_overflow_l1)
## INTERFACE_NOT_THREAD_SAFE

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "Interface Not Thread Safe" by [racerd](/docs/next/checker-racerd).*

This error indicates that you have invoked an interface method not annotated
with `@ThreadSafe` from a thread-safe context (e.g., code that uses locks or is
marked `@ThreadSafe`). The fix is to add the `@ThreadSafe` annotation to the
interface or to the interface method. For background on why these annotations
are needed, see the detailed explanation
[here](/docs/next/checker-racerd#interface-not-thread-safe).

## INVALID_SIL

*Reported as "Invalid Sil" by [sil-validation](/docs/next/checker-sil-validation).*

The SIL instruction does not conform to the expected subset of instructions
expected for the front-end of the language for the analyzed code.

## INVARIANT_CALL

*Reported as "Invariant Call" by [loop-hoisting](/docs/next/checker-loop-hoisting).*

We report this issue type when a function call is loop-invariant and hoistable, i.e.
- the function has no side side effects (pure)
- has invariant arguments and result (i.e. have the same value in all loop iterations)
- it is guaranteed to execute, i.e. it dominates all loop sources

```java
int foo(int x, int y) {
 return x + y;
}


void invariant_hoist(int size) {
    int x = 10;
    int y = 5;
    for (int i = 0; i < size; i++) {
      foo(x, y); // hoistable
    }
  }
```

## IPC_ON_UI_THREAD

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Ipc On Ui Thread" by [starvation](/docs/next/checker-starvation).*

A blocking `Binder` IPC call occurs on the UI thread.
## LAB_RESOURCE_LEAK

*Reported as "Lab Resource Leak" by [resource-leak-lab](/docs/next/checker-resource-leak-lab).*

Toy issue.
## LINEAGE_FLOW

*Category: [Sensitive data flow](/docs/next/all-categories#sensitive-data-flow). Reported as "Lineage Flow" by [lineage](/docs/next/checker-lineage).*

A Lineage taint flow has been detected from a source to a sink.

## LOCKLESS_VIOLATION

*Reported as "Lockless Violation" by [starvation](/docs/next/checker-starvation).*

A method implements an interface signature annotated with `@Lockless` but which transitively acquires a lock.

Example:

```java
Interface I {
    @Lockless
    public void no_lock();
}

class C implements I {
  private synchronized do_lock() {}

  public void no_lock() { // this method should not acquire any locks
    do_lock();
  }
}
```

## LOCK_CONSISTENCY_VIOLATION

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "Lock Consistency Violation" by [racerd](/docs/next/checker-racerd).*

This is an error reported on C++ and Objective C classes whenever:

- Some class method directly uses locking primitives (not transitively).
- It has a public method which writes to some member `x` while holding a lock.
- It has a public method which reads `x` without holding a lock.

The above may happen through a chain of calls. Above, `x` may also be a
container (an array, a vector, etc).

### Fixing Lock Consistency Violation reports

- Avoid the offending access (most often the read). Of course, this may not be
  possible.
- Use synchronization to protect the read, by using the same lock protecting the
  corresponding write.
- Make the method doing the read access private. This should silence the
  warning, since Infer looks for a pair of non-private methods. Objective-C:
  Infer considers a method as private if it's not exported in the header-file
  interface.

## LOCK_ON_UI_THREAD

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Lock on UI Thread" by [starvation](/docs/next/checker-starvation).*

A method annoted as being on UIThread acquires a lock. This could be a potential performance issue

Example:

```java
class Example {
    @UiThread
    void foo() {
        synchronized(this) {
        }
    }
}
```

## MEMORY_LEAK_C

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Memory Leak" by [pulse](/docs/next/checker-pulse).*

### Memory leak in C

This error type is only reported in C and Objective-C code. In Java we do not
report memory leaks because it is a garbage collected language.

In C, Infer reports memory leaks when objects are created with `malloc` and not
freed. For example:

```c
void memory_leak_bug () {
    struct Person *p = malloc(sizeof(struct Person));
}
```

### Memory leak in Objective-C

Additionally, in Objective-C, Infer reports memory leaks that happen when
objects from Core Foundation or Core Graphics don't get released.

```objectivec
-(void) memory_leak_bug_cf {
    CGPathRef shadowPath = CGPathCreateWithRect(self.inputView.bounds, NULL); //object created and not released.
}
```

## MEMORY_LEAK_CPP

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Memory Leak" by [pulse](/docs/next/checker-pulse).*

See [MEMORY_LEAK_C](#memory_leak_c)
## MISSING_NULLABILITY_ANNOTATION

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Missing Nullability Annotation" by [swift-objc-nullability](/docs/next/checker-swift-objc-nullability).*

An Objective-C method that returns a pointer is being called from Swift,
but its declaration carries no nullability annotation (`_Nullable` or
`_Nonnull`). Without an annotation Swift's clang importer treats the result
as an Implicitly Unwrapped Optional (`T!`), so any subsequent use that
assumes non-nil values traps at runtime if the method ever returns `nil`.

### Why this matters

Objective-C uses raw pointers and signals "may be nil" only by convention.
Swift, by contrast, requires nullability to be explicit in the type system:

| Objective-C declaration             | Swift import      | Behaviour on `nil`             |
| ----------------------------------- | ----------------- | ------------------------------ |
| `- (NSString *)foo;`                | `func foo() -> String!` | implicit unwrap, **trap**      |
| `- (NSString * _Nonnull)foo;`       | `func foo() -> String`  | impossible by contract         |
| `- (NSString * _Nullable)foo;`      | `func foo() -> String?` | safe; caller must unwrap       |

The unannotated form is the dangerous one: Swift will silently let you
write `api.foo().count` even though the underlying call may return `nil`,
and the trap fires far away from the missing annotation.

### Example

```objc
// LegacyAPI.h - third-party header, no annotation
@interface LegacyAPI : NSObject
- (NSString *)getOptionalThing;
@end
```

```swift
func bad(api: LegacyAPI) {
  let s = api.getOptionalThing()  // imported as String!
  print(s.count)                  // crashes if getOptionalThing returns nil
}
```

Infer reports `MISSING_NULLABILITY_ANNOTATION` on the call to
`getOptionalThing`.

### Preferred fix: annotate the Objective-C header

Edit the declaration to state the contract explicitly. If the method may
return `nil`, mark it `_Nullable`; otherwise mark it `_Nonnull`:

```objc
// LegacyAPI.h
@interface LegacyAPI : NSObject
- (NSString * _Nullable)getOptionalThing;
@end
```

Now Swift imports the result as `String?` and the compiler forces the
caller to handle the nil case:

```swift
func good(api: LegacyAPI) {
  if let s = api.getOptionalThing() {
    print(s.count)
  }
}
```

For headers that already wrap whole regions in
`NS_ASSUME_NONNULL_BEGIN` / `NS_ASSUME_NONNULL_END`, only the exception
needs the explicit `_Nullable`.

### Workaround when you cannot edit the header

If the declaration lives in a third-party framework or a header you do not
own, defend at the Swift call site by casting the result to an Optional
with `as?`:

```swift
func goodWorkaround(api: LegacyAPI) {
  if let s = api.getOptionalThing() as? NSString {
    print(s.length)
  }
}
```

The `as?` cast lifts the IUO into a real `Optional`, and `if let` /
`guard let` then forces the nil case to be handled. Infer recognises this
defensive shape (an `objc_msgSend` whose result feeds a
`_bridgeToObjectiveC` call in the lowered IR) and stops reporting on the
call.

A bare force-unwrap (`api.getOptionalThing()!`) is **not** a fix: it makes
the trap explicit but does not eliminate it, and infer will continue to
report on the call.

## MISSING_NULLABILITY_ANNOTATION_PULSE

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Missing Nullability Annotation" by [pulse](/docs/next/checker-pulse).*

An Objective-C method that returns a pointer is being called from Swift,
but its declaration carries no nullability annotation (`_Nullable` or
`_Nonnull`). Without an annotation Swift's clang importer treats the result
as an Implicitly Unwrapped Optional (`T!`), so any subsequent use that
assumes non-nil values traps at runtime if the method ever returns `nil`.

### Why this matters

Objective-C uses raw pointers and signals "may be nil" only by convention.
Swift, by contrast, requires nullability to be explicit in the type system:

| Objective-C declaration             | Swift import      | Behaviour on `nil`             |
| ----------------------------------- | ----------------- | ------------------------------ |
| `- (NSString *)foo;`                | `func foo() -> String!` | implicit unwrap, **trap**      |
| `- (NSString * _Nonnull)foo;`       | `func foo() -> String`  | impossible by contract         |
| `- (NSString * _Nullable)foo;`      | `func foo() -> String?` | safe; caller must unwrap       |

The unannotated form is the dangerous one: Swift will silently let you
write `api.foo().count` even though the underlying call may return `nil`,
and the trap fires far away from the missing annotation.

### Example

```objc
// LegacyAPI.h - third-party header, no annotation
@interface LegacyAPI : NSObject
- (NSString *)getOptionalThing;
@end
```

```swift
func bad(api: LegacyAPI) {
  let s = api.getOptionalThing()  // imported as String!
  print(s.count)                  // crashes if getOptionalThing returns nil
}
```

Infer reports `MISSING_NULLABILITY_ANNOTATION` on the call to
`getOptionalThing`.

### Preferred fix: annotate the Objective-C header

Edit the declaration to state the contract explicitly. If the method may
return `nil`, mark it `_Nullable`; otherwise mark it `_Nonnull`:

```objc
// LegacyAPI.h
@interface LegacyAPI : NSObject
- (NSString * _Nullable)getOptionalThing;
@end
```

Now Swift imports the result as `String?` and the compiler forces the
caller to handle the nil case:

```swift
func good(api: LegacyAPI) {
  if let s = api.getOptionalThing() {
    print(s.count)
  }
}
```

For headers that already wrap whole regions in
`NS_ASSUME_NONNULL_BEGIN` / `NS_ASSUME_NONNULL_END`, only the exception
needs the explicit `_Nullable`.

### Workaround when you cannot edit the header

If the declaration lives in a third-party framework or a header you do not
own, defend at the Swift call site by casting the result to an Optional
with `as?`:

```swift
func goodWorkaround(api: LegacyAPI) {
  if let s = api.getOptionalThing() as? NSString {
    print(s.length)
  }
}
```

The `as?` cast lifts the IUO into a real `Optional`, and `if let` /
`guard let` then forces the nil case to be handled. Infer recognises this
defensive shape (an `objc_msgSend` whose result feeds a
`_bridgeToObjectiveC` call in the lowered IR) and stops reporting on the
call.

A bare force-unwrap (`api.getOptionalThing()!`) is **not** a fix: it makes
the trap explicit but does not eliminate it, and infer will continue to
report on the call.

## MISSING_REQUIRED_PROP

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Missing Required Prop" by [litho-required-props](/docs/next/checker-litho-required-props).*

This issues is reported when a required `@Prop` is missing.


## Examples

Assume that the following Litho Component specification is defined as follows where `prop1` is optional and `prop2` is required.

```java
class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop int prop2) {
    ...
  }
  ...
}
```

When we build the corresponding component, we should have all the required props. If we are missing optional props (e..g `prop1` below), it is ok.

```java
MyComponent.create(c)
    .prop2(8)
    .build();
```

However, if we are missing a required prop, Infer gives an error below for the missing `prop2`.

```java
MyComponent.create(c)
    .prop1("My prop 1")
    .build();
```

** Action **

There are two ways to fix this issue.

First, we could add the missing `prop2`:

```java
MyComponent.create(c)
    .prop1("My prop 1")
    .prop2(x) // where x is some integer
    .build();
```

or alternatively, if the `prop2` is not really required, we could change the component spec to reflect that:


```java
class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop(optional = true) int prop2) {
    ...
  }
  ...
}
```
## MIXED_SELF_WEAKSELF

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Mixed Self WeakSelf" by [self-in-block](/docs/next/checker-self-in-block).*

This check reports an issue when an Objective-C block captures both `self` and `weakSelf`, a weak pointer to `self`.
Possibly the developer meant to capture only `weakSelf` to avoid a retain cycle, but made a typo and used `self`
instead of `strongSelf`. In this case, this could cause a retain cycle.

Example:

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      [strongSelf foo];
      int x = self->x; // typo here
    }
    return 0;
  };
```

**Action**: Fixing the typo is generally the right course of action.

*Limitations:* To keep this check simple and intra-procedural, we rely on names to find `weakSelf`:
we assume that any captured weak pointer whose name contains "self" is a weak reference to `self`.

## MODIFIES_IMMUTABLE

*Reported as "Modifies Immutable" by [impurity](/docs/next/checker-impurity).*

This issue type indicates modifications to fields marked as @Immutable. For instance, below function `mutateArray` would be marked as modifying immutable field `testArray`:
```java
  @Immutable int[] testArray = new int[]{0, 1, 2, 4};
  
  int[] getTestArray() {
    return testArray;
  }                
          
  void mutateArray() {
    int[] array = getTestArray();
    array[2] = 7;
  }
```

## MULTIPLE_WEAKSELF

*Reported as "Multiple WeakSelf Use" by [self-in-block](/docs/next/checker-self-in-block).*

This check reports when an Objective-C block uses `weakSelf` (a weak pointer to `self`) more than once.
This could lead to unexpected behaviour. Even if `weakSelf` is not nil in the first use, it could be nil
in the following uses since the object that `weakSelf` points to could be freed anytime.

Example:

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
      [weakSelf foo];
      int x = weakSelf->x;
  };
```

**Action:**
One should assign `weakSelf` to a strong pointer first, and then
use it in the block.

```objectivec
  __weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      [strongSelf foo];
      int x = strongSelf->x;
    }
    ...
  };
```

*Limitations:* To keep this check simple and intra-procedural, we rely on names to find `weakSelf`:
we assume that any captured weak pointer whose name contains "self" is a weak reference to `self`.
In contrast, `strongSelf` is a local variable to the block, so the check supports any name given to
a local strong pointer that has been assigned `weakSelf`.

## MUTUAL_RECURSION_CYCLE

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Mutual Recursion Cycle" by [pulse](/docs/next/checker-pulse).*

A recursive call or mutually recursive call has been detected. This does *not* mean that the program won't terminate, just that the code is recursive. You should double-check if the recursion is intended and if it can lead to non-termination or a stack overflow.

Example of recursive function:


```C
int factorial(int x) {
  if (x > 0) {
    return x * factorial(x-1);
  } else {
    return 1;
  }
}
```

## NIL_BLOCK_CALL

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Nil Block Call" by [pulse](/docs/next/checker-pulse).*

This check reports when one tries to call an Objective-C block that is `nil`.
This causes a crash.

Example:

```objectivec
-(void) foo:(void (^)())callback {
    callback();
}

-(void) bar {
    [self foo:nil]; //crash
}
```

**Action**:

Adding a check for `nil` before calling the block, or making sure never to call the method `foo:` with `nil`.

## NIL_BLOCK_CALL_LATENT

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Nil Block Call Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NIL_BLOCK_CALL](#nil_block_call). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NIL_INSERTION_INTO_COLLECTION

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Nil Insertion Into Collection" by [pulse](/docs/next/checker-pulse).*

This checks reports when `nil` is passed to collections in Objective-C such as arrays and dictionaries. This causes a crash.

### Arrays

Adding objects to an array, inserting objects at a given index, or replacing objects at a given index, can all
lead to a crash when the object is `nil`.

```objectivec
  [mArray addObject:nil];  //crash

  [mArray insertObject:nil atIndex:0];   //crash

  [mArray replaceObjectAtIndex:0 withObject:nil]; //crash
```

### Dictionaries

Adding a `nil` value in a dictionary causes a crash. If the concept of `nil` is required, one can add
`[NSNull null]` instead.

```objectivec
  id value = nil;
  [mDict setObject:value forKey:@"somestring"]; //crash

  [mDict setObject:[NSNull null] forKey:@"somestring"]; //ok
```

Retrieving or removing an object from a dictionary with a `nil` key also causes a crash:

```objectivec
    id key = nil;
    mDict[key] = @"somestring"; //crash

   [mDict removeObjectForKey:nil]; //crash
```

**Action**:

In all the cases above, when passing `nil` causes a crash, the solutions are either making sure
that the object passed will never be `nil`, or adding a check for `nil` before calling those methods.

## NIL_INSERTION_INTO_COLLECTION_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Nil Insertion Into Collection" by [pulse](/docs/next/checker-pulse).*

A latent [NIL_INSERTION_INTO_COLLECTION](#nil_insertion_into_collection). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NIL_MESSAGING_TO_NON_POD

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Nil Messaging To Non Pod" by [pulse](/docs/next/checker-pulse).*

In Objective-C, calling a method on `nil` (or in Objective-C terms, sending a message to `nil`) does not crash,
it simply returns a falsy value (nil/0/false). However, sending a message that returns
a non-POD C++ type (POD being ["Plain Old Data"](https://en.cppreference.com/w/cpp/named_req/PODType), essentially
anything that cannot be compiled as a C-style struct) to `nil` causes undefined behaviour.

```objectivec
std::shared_ptr<int> callMethodReturnsnonPOD() {
  SomeObject* obj = getObjectOrNil();
  std::shared_ptr<int> d = [obj returnsnonPOD]; // UB
  return d;
}
```

To fix the above issue, we need to check if `obj` is
not `nil` before calling the `returnsnonPOD` method:

```objectivec
std::shared_ptr<int> callMethodReturnsnonPOD(bool b) {
  SomeObject* obj = getObjectOrNil(b);
  if (obj == nil) { return std::make_shared<int>(0); }
  std::shared_ptr<int> d = [obj returnsnonPOD];
  return d;
}
```

## NIL_MESSAGING_TO_NON_POD_LATENT

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Nil Messaging To Non Pod Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NIL_MESSAGING_TO_NON_POD](#nil_messaging_to_non_pod). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_MATCHING_BRANCH_IN_TRY

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Branch In Try" by [pulse](/docs/next/checker-pulse).*

No matching branch is found when evaluating the `of` section of a `try` expression. Corresponds to the `{try_clause,V}` error in the Erlang runtime.

For example, if we call `tail([])` and the full definition of `tail` is
```erlang
tail(X) ->
    try X of
        [_|T] -> {ok,T}
    catch
        _ -> error
    end.
```

## NO_MATCHING_BRANCH_IN_TRY_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Branch In Try Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_MATCHING_BRANCH_IN_TRY](#no_matching_branch_in_try). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_MATCHING_CASE_CLAUSE

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Case Clause" by [pulse](/docs/next/checker-pulse).*

No matching case clause in Erlang: Reports an error when none of the clauses of a `case` match the expression. Corresponds to the `{case_clause,V}` error in the Erlang runtime.

For example, if we call `tail([])` and the full definition of `tail` is
```erlang
tail(X) ->
    case X of
        [_|T] -> T
    end.
```

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

## NO_MATCHING_CASE_CLAUSE_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Case Clause Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_MATCHING_CASE_CLAUSE](#no_matching_case_clause). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_MATCHING_ELSE_CLAUSE

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Else Clause" by [pulse](/docs/next/checker-pulse).*

No matching else clause in Erlang: Reports an error when none of the clauses of an `else` match the short-circuit result from `maybe` body. Corresponds to the `{else_clause,V}` error in the Erlang runtime.

For example, here the `1 ?= 2` expression does not match and short-circuits to `2`, which does not match the single clause under `else`:
```erlang
else_clause_error() ->
    maybe
        1 ?= 2
    else
        1 -> ok
    end.
```

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

## NO_MATCHING_ELSE_CLAUSE_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Else Clause Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_MATCHING_ELSE_CLAUSE](#no_matching_else_clause). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_MATCHING_FUNCTION_CLAUSE

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Function Clause" by [pulse](/docs/next/checker-pulse).*

No matching function clause in Erlang: Reports an error when none of the clauses of a function match the arguments of a call. Corresponds to the `function_clause` error in the Erlang runtime.

For example, if we call `tail([])` and the full definition of `tail` is
```erlang
tail([_|Xs]) -> Xs.
```

This error is reported if either the pattern(s) or the guard(s) prevent matching any of the clauses.

## NO_MATCHING_FUNCTION_CLAUSE_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Matching Function Clause Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_MATCHING_FUNCTION_CLAUSE](#no_matching_function_clause). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_MATCH_OF_RHS

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Match Of Rhs" by [pulse](/docs/next/checker-pulse).*

No match of right hand side value in Erlang: Reports an error when the right hand side value of a `match` expression does not match the pattern on the left hand side. Corresponds to the `{badmatch,V}` error in the Erlang runtime.

For example, `[H|T] = []` gives the error because the left hand side pattern requires at least one element in the list on the right hand side.

## NO_MATCH_OF_RHS_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No Match Of Rhs Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_MATCH_OF_RHS](#no_match_of_rhs). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NO_TRUE_BRANCH_IN_IF

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No True Branch In If" by [pulse](/docs/next/checker-pulse).*

No true branch when evaluating an if expression in Erlang: Reports an error when none of the branches of an `if` expression evaluate to true. Corresponds to the `if_clause` error in the Erlang runtime.

For example, if we call `sign(0)` and the full definition of `sign` is
```erlang
sign(X) ->
    if
        X > 0 -> positive;
        X < 0 -> negative
    end.
```

## NO_TRUE_BRANCH_IN_IF_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "No True Branch In If Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NO_TRUE_BRANCH_IN_IF](#no_true_branch_in_if). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NSSTRING_INTERNAL_PTR_CAPTURED_IN_BLOCK

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "NSString Captured in Block" by [self-in-block](/docs/next/checker-self-in-block).*

This check flags when an internal pointer of a local variable of type `std::string` is captured in an escaping block.
This means that the block will be leaving the current scope, i.e. it is
not annotated with `__attribute__((noescape))`.

Example:

```
  std::string fullName;
  const char* c = fullName.c_str();
  dispatch_async(dispatch_get_main_queue(), ^{
    const char* c1 = c;
  });
```

This could cause crashes because the variable is likely to be freed when the code is executed, leaving the pointer dangling.

## NULLPTR_DEREFERENCE

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse).*

Infer reports null dereference bugs in Java, C, C++, and Objective-C
when it is possible that the null pointer is dereferenced, leading to
a crash.

### Null dereference in Java

Many of Infer's reports of potential Null Pointer Exceptions (NPE) come from code of the form

```java
  p = foo(); // foo() might return null
  stuff();
  p.goo();   // dereferencing p, potential NPE
```

If you see code of this form, then you have several options.

**If you are unsure whether or not `foo()` will return null**, you should
ideally either

1. Change the code to ensure that `foo()` can not return null, or

2. Add a check that `p` is not `null` before dereferencing `p`.

Sometimes, in case (2) it is not obvious what you should do when `p`
is `null`. One possibility is to throw an exception, failing early but
explicitly. This can be done using `checkNotNull` as in the following
code:

```java
// code idiom for failing early
import static com.google.common.base.Preconditions.checkNotNull;

  //... intervening code

  p = checkNotNull(foo()); // foo() might return null
  stuff();
  p.goo(); // p cannot be null here
```

The call `checkNotNull(foo())` will never return `null`: if `foo()`
returns `null` then it fails early by throwing a Null Pointer
Exception.

Facebook NOTE: **If you are absolutely sure that foo() will not be
null**, then if you land your diff this case will no longer be
reported after your diff makes it to trunk.

### Null dereference in C

Here is an example of an inter-procedural null dereference bug in C:

```c
struct Person {
  int age;
  int height;
  int weight;
};
int get_age(struct Person *who) {
  return who->age;
}
int null_pointer_interproc() {
  struct Person *joe = 0;
  return get_age(joe);
}
```

### Null dereference in Objective-C

In Objective-C, null dereferences are less common than in Java, but they still
happen and their cause can be hidden. In general, passing a message to nil does
not cause a crash and returns `nil`, but dereferencing a pointer directly does
cause a crash.

Example:

```objectivec
(int) foo:(C*) param {  // passing nil
  D* d = [param bar];   // nil message passing
  return d->fld;        // crash
}
(void) callFoo {
  C* c = [self bar];    // returns nil
  [foo:c];              // crash reported here
}
```

**Action**:
Adding a `nil` check either for `param` above or for `d`, or making sure that `foo:` will never
be called with `nil`.

Calling a `nil` block will also cause a crash.
We have a dedicated issue type for this case: [Nil Block Call](/docs/next/all-issue-types#nil_block_call).

Moreover, inserting `nil` into a collection will cause a crash as well. We
also have a dedicated issue type for this case:
[Nil Insertion Into Collection](/docs/next/all-issue-types#nil_insertion_into_collection).

## NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse).*

Infer reports null dereference bugs in Java, C, C++, and Objective-C
when it is possible that the null pointer is dereferenced, leading to
a crash.

### Null dereference in Java

Many of Infer's reports of potential Null Pointer Exceptions (NPE) come from code of the form

```java
  p = foo(); // foo() might return null
  stuff();
  p.goo();   // dereferencing p, potential NPE
```

If you see code of this form, then you have several options.

**If you are unsure whether or not `foo()` will return null**, you should
ideally either

1. Change the code to ensure that `foo()` can not return null, or

2. Add a check that `p` is not `null` before dereferencing `p`.

Sometimes, in case (2) it is not obvious what you should do when `p`
is `null`. One possibility is to throw an exception, failing early but
explicitly. This can be done using `checkNotNull` as in the following
code:

```java
// code idiom for failing early
import static com.google.common.base.Preconditions.checkNotNull;

  //... intervening code

  p = checkNotNull(foo()); // foo() might return null
  stuff();
  p.goo(); // p cannot be null here
```

The call `checkNotNull(foo())` will never return `null`: if `foo()`
returns `null` then it fails early by throwing a Null Pointer
Exception.

Facebook NOTE: **If you are absolutely sure that foo() will not be
null**, then if you land your diff this case will no longer be
reported after your diff makes it to trunk.

### Null dereference in C

Here is an example of an inter-procedural null dereference bug in C:

```c
struct Person {
  int age;
  int height;
  int weight;
};
int get_age(struct Person *who) {
  return who->age;
}
int null_pointer_interproc() {
  struct Person *joe = 0;
  return get_age(joe);
}
```

### Null dereference in Objective-C

In Objective-C, null dereferences are less common than in Java, but they still
happen and their cause can be hidden. In general, passing a message to nil does
not cause a crash and returns `nil`, but dereferencing a pointer directly does
cause a crash.

Example:

```objectivec
(int) foo:(C*) param {  // passing nil
  D* d = [param bar];   // nil message passing
  return d->fld;        // crash
}
(void) callFoo {
  C* c = [self bar];    // returns nil
  [foo:c];              // crash reported here
}
```

**Action**:
Adding a `nil` check either for `param` above or for `d`, or making sure that `foo:` will never
be called with `nil`.

Calling a `nil` block will also cause a crash.
We have a dedicated issue type for this case: [Nil Block Call](/docs/next/all-issue-types#nil_block_call).

Moreover, inserting `nil` into a collection will cause a crash as well. We
also have a dedicated issue type for this case:
[Nil Insertion Into Collection](/docs/next/all-issue-types#nil_insertion_into_collection).

## NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS_LATENT

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse).*

A latent [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS](#nullptr_dereference_in_nullsafe_class). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NULLPTR_DEREFERENCE_LATENT

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Null Dereference" by [pulse](/docs/next/checker-pulse).*

A latent [NULLPTR_DEREFERENCE](#nullptr_dereference). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## NULL_ARGUMENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Null Argument" by [pulse](/docs/next/checker-pulse).*

```objc
This issue type indicates `nil` being passed as argument where a non-nil value expected.

#import <Foundation/Foundation.h>

// Test (non-nil) returned values of NSString methods against `nil`
NSString* stringNotNil(NSString* str) {
  if (!str) {
        // ERROR: NSString:stringWithString: expects a non-nil value
	return [NSString stringWithString:nil];
  }
  return str;
}
```

## NULL_ARGUMENT_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Null Argument Latent" by [pulse](/docs/next/checker-pulse).*

A latent [NULL_ARGUMENT](#null_argument). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## OPTIONAL_EMPTY_ACCESS

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Optional Empty Access" by [pulse](/docs/next/checker-pulse).*

Optional Empty Access warnings are reported when we try to retrieve the value of a [`folly::Optional`](https://github.com/facebook/folly/blob/master/folly/Optional.h) when it is empty (i.e. `folly::none`).

In the following example we get a warning as `int_opt` might be `folly::none` and its value is being accessed:

```cpp
bool somef(int v);

folly::Optional<int> mightReturnNone(int v) {
   if (somef(v)) {
      return folly::Optional(v);
   }

   return folly::none;
}

int value_no_check() {
  folly::Optional<int> int_opt = mightReturnNone (4);
  return int_opt.value(); // Optional Empty Access warning
}
```

We do not get the warning anymore if we add a check whether `int_opt` is not empty:

```cpp
int value_check() {
  folly::Optional<int> int_opt = mightReturnNone (4);
  if (int_opt.has_value()) {
     return int_opt.value(); // OK
  }
  return -1;
}
```

In some cases we know that we have a non-empty value and there is no need to have a check. Consider the following example where Infer does not warn:

```cpp
bool somef(int v) {return v > 3;};

folly::Optional<int> mightReturnNone(int v) {
   if (somef(v)) {
      return folly::Optional(v);
   }

   return folly::none;
}

int value_no_check() {
  folly::Optional<int> int_opt = mightReturnNone (4); // cannot be folly::none
  return int_opt.value(); // OK
}
```

## OPTIONAL_EMPTY_ACCESS_LATENT

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Optional Empty Access Latent" by [pulse](/docs/next/checker-pulse).*

A latent [OPTIONAL_EMPTY_ACCESS](#optional_empty_access). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## PULSE_ASSERTION_ERROR

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Assertion Error" by [pulse](/docs/next/checker-pulse).*

This error is reported in Java and in Python. It fires when we detect a path that leads to an assertion failure.



## PULSE_CANNOT_INSTANTIATE_ABSTRACT_CLASS

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Cannot Instantiate Abstract Class" by [pulse](/docs/next/checker-pulse).*

Instantiating an abstract class will lead to `Cannot instantiate abstract class` error.

```hack
abstract class AbstractClass1 {}

class ConcreteClass1 extends AbstractClass1 {}

public static function makeGeneric<T>(classname<T> $cls): void {
    new $cls();
}

<<__ConsistentConstruct>>
abstract class AbstractClass2 {

  public static function makeStatic(): void {
    new static();
  }
}

class ConcreteClass2 extends AbstractClass2 {}

public function badViaGeneric(): void {
    Main::makeGeneric(AbstractClass1::class); // ERROR!
}

public function goodViaGeneric(): void {
  Main::makeGeneric(ConcreteClass1::class);
}

public function badViaStatic(): void {
  AbstractClass2::makeStatic(); // ERROR!
}

public function goodViaStatic(): void {
  ConcreteClass2::makeStatic();
}
```

## PULSE_CONST_REFABLE

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Const Refable Parameter" by [pulse](/docs/next/checker-pulse).*

This issue is reported when a function parameter is a) passed by value and b) is not modified inside the function. Instead, parameter can be passed by const reference, i.e. converted to a `const&` so that no unnecessary copy is created at the callsite of the function.

For example,

```cpp
#include <vector>

int read_first(const std::vector<int>& vec) { return vec[0]; }

void const_refable(std::vector<int> vec) {
  int first = read_first(vec); // vec is never modified, so the parameter should have type const&
}
```

## PULSE_DICT_MISSING_KEY

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Dict Missing Key" by [pulse](/docs/next/checker-pulse).*

This issue is similar to [`PULSE_UNINITIALIZED_VALUE`](#pulse_uninitialized_value), but it is to warn
reading a missing key of dictionary in Hack.

For example, in the following code, the dictionary `$d` has no entry for `bye`, so reading
`$d['bye']` will throw the `OutOfBoundsException` exception, which is usually unexpected from
developers.  We can use a safer function `idx` instead when keys of a dictionary is unclear.

```hack
function simple_bad() : int {
  $d = dict['hi' => 42, 'hello' => 52];
  return $d['bye'];
}
```

## PULSE_DYNAMIC_TYPE_MISMATCH

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Dynamic Type Mismatch" by [pulse](/docs/next/checker-pulse).*

This error is reported in Hack. It fires when we detect an operation that is incompatible
with the dynamic type of its arguments.

For example, reading `$x['key']` when `$x` is a vector.


## PULSE_READONLY_SHARED_PTR_PARAM

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Read-only Shared Parameter" by [pulse](/docs/next/checker-pulse).*

This issue is reported when a shared pointer parameter is a) passed by value and b) is used only for reading, rather than lifetime extension. At the callsite, this might cause a potentially expensive unnecessary copy of the shared pointer, especially when many number of threads are sharing it. To avoid this, consider 1) passing the raw pointer instead and 2) use `std::shared_ptr::get` at callsites.

For example,

```cpp
void callee(std::shared_ptr<T> x) {
  // read_T(*x);
}

void caller() {
  callee(shared_ptr);
}
```

can be changed to

```cpp
void callee(T* p) {
  // read_T(*p);
}

void caller() {
  callee(shared_ptr.get());
}
```

## PULSE_REFERENCE_STABILITY

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Reference Stability" by [pulse](/docs/next/checker-pulse).*

The family of maps `folly::F14ValueMap`, `folly::F14VectorMap`, and by extension
`folly::F14FastMap` differs slightly from `std::unordered_map` as it does not
provide reference stability. When the map resizes such as when `reserve` is
called or new elements are added, all existing references become invalid and
should not be used.

`operator[]` is an interesting case as it can easily introduce unsafe code when
used twice in the same expression. Depending on what keys are present and which
order the compiler sequences sub-expressions, an insert via `operator[]` can
invalidate a reference obtained in the same expression before it's read from.
Typically, those cases can be improved by using other map functions such as
`at`, `find`, `emplace`, or `insert_or_assign` to increase code quality and
safety.

Examples:

```cpp
#include <folly/container/F14Map.h>

void use_reference_after_growth_bad(folly::F14FastMap<int, int>& map) {
  const auto& valueRef = map.at(1);
  map.emplace(13, 71);
  const auto valueCopy = valueRef;
}

void unsafe_expressions_bad(folly::F14FastMap<int, int>& map) {
  // Unsafe expressions in situations where one or both keys are not present.
  map[13] = map[71];
  const auto p = map[13] * map[71];
  const auto q = f(map[13], map[71]);
}
```

## PULSE_RESOURCE_LEAK

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Resource Leak" by [pulse](/docs/next/checker-pulse).*

See [RESOURCE_LEAK](#resource_leak)
## PULSE_TRANSITIVE_ACCESS

*Category: [Logic error](/docs/next/all-categories#logic-error). Reported as "Transitive Access" by [pulse](/docs/next/checker-pulse).*

This issue tracks spurious accesses that are reachable from specific entry functions.

Spurious accesses are specified as specific load/calls.

Entry functions are specified through their enclosing class that must extend a specific 
class and should not extend a list of specific classes.


## PULSE_UNAWAITED_AWAITABLE

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Unawaited Awaitable" by [pulse](/docs/next/checker-pulse).*

`Awaitable` values created by calls to asynchronous methods should eventually be `await`ed along all codepaths (even if their value is unused). Hence the following is *not* OK

```hack
class A {
  public static async genInt() : Awaitable<int>{
    // typically do something involving IO
  }

  public static async genBad() : Awaitable<void> {
    $_unused = self::genInt(); // ERROR: should have done $_unused = await self::genInt();
    return;
  }
}
```

Failure to `await` an `Awaitable` can lead to non-deterministic amount of the asynchronous call actually being executed, and can also indicate a logical confusion between `T` and `Awaitable<T>` that may not be caught by the type-checker.

## PULSE_UNFINISHED_BUILDER

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Unfinished Builder" by [pulse](/docs/next/checker-pulse).*

Classes adhering to builder pattern are usually expected to call a finalizer function at some point to produce final result based on values that were passed to a builder itself. If finalizer function hasn't been called then builder's data won't be consumed in any meaningful way and will just be discarded.

```hack
class MyBuilder {
  private int $a = 0;
  private int $b = 0;

  public function setA(int $a): MyBuilder {
    $this->a = $a;
    return $this;
  }

  public function setB(int $b): MyBuilder {
    $this->b = $b;
    return $this;
  }

  public function saveX(): Awaitable<void> {
    // typically do something involving IO
  }
}

class BuilderTester {
  public static function builderUserOK(): void {
    $b = new MyBuilder(0);
    $b->setA(42)->setB(97)->saveX();
  }

  public static function builderUserBad(): void {
    $b = new MyBuilder(0);
    $b->setA(42)->setB(97); // ERROR: saveX hasn't been called so the builder's data is discarded
  }
}
```

## PULSE_UNINITIALIZED_CONST

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Uninitialized Const" by [pulse](/docs/next/checker-pulse).*

This issue is similar to [`PULSE_UNINITIALIZED_VALUE`](#pulse_uninitialized_value), but it is to detect the uninitialized abstract const value in Hack.

For example, in the following code, the `FIELD` can be read by the static method `get_field`.

* It is problematic invoking `static::FIELD`, since it may be resolved to a `A::FIELD` access, if called from `A::get_field()`. Because `FIELD` is abstract in `A`, it is never assigned a value and the vm will crash. Unfortunately, Hack's type system cannot catch this.
* In the `B` class, `FIELD` is initialized, thus invoking `B::get_field` is safe.

```hack
abstract class A {
  abstract const string FIELD;
  
  public static function get_field(): string {
    return static::FIELD;
  }
}

function call_get_field_bad(): string {
  return A::get_field();
}

class B extends A {
  const string FIELD = "defined";
}

function call_get_field_ok(): string {
  return B::get_field();
}
```

## PULSE_UNINITIALIZED_METHOD

*Category: [Runtime exception](/docs/next/all-categories#runtime-exception). Reported as "Uninitialized Method" by [pulse](/docs/next/checker-pulse).*

This issue is similar to [`PULSE_UNINITIALIZED_CONST`](#pulse_uninitialized_const), but it is to detect the uninitialized method call in Hack.

For example, in the following code, the static method `foo` is declared only in the interface and the abstract class.  Thus, calling the static method can introduce an unexpected exception or a fatal error, while the type checker does miss the issue.

```hack
interface MyInterface {
  public static function foo(): string;
}

abstract class MyAbstractClass {
  public abstract static function foo(): string;
}

function interface_method_static_method_bad(): string {
  // Uncaught exception 'TypehintViolationException'
  $c = MyInterface::class;
  return $c::foo();
}

function abstract_class_static_method_bad(): string {
  // Fatal error: Cannot call abstract method
  $c = MyAbstractClass::class;
  return $c::foo();
}
```

## PULSE_UNINITIALIZED_VALUE

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Uninitialized Value" by [pulse](/docs/next/checker-pulse).*

The code uses a variable that has not been initialized, leading to unpredictable or unintended results.

Using uninitialized values can lead to undefined behaviors possibly resulting in crashes, security failures and invalid results.

This can easily be fixed by assigning all variables to an initial value when declaring them.

This, for example, in C:

```c
struct coordinates {
  int x;
  int y;
};

void foo() {
  struct coordinates c;
  c.x = 42;
  c.y++; // uninitialized value c.y!

  int z;
  if (z == 0) { // uninitialized value z!
    // something
  }
}
```

## PULSE_UNNECESSARY_COPY

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy" by [pulse](/docs/next/checker-pulse).*

This is reported when Infer detects an unnecessary copy of an object via copy constructor where neither the source nor the copied variable are modified before the variable goes out of scope. Rather than the copy, a reference to the source object could be used to save memory.

For example,

```cpp
struct A {
  int a;
};

int unnecessary_copy(A& x){
  auto y = x; // calls copy constructor
  return y.a; // y is not modified after copy, hence we could avoid the copy by adding & after auto as below
}

int use_reference_instead(A& x){
  auto& y = x; // copy the ref only
  return y.a;
}
```
## PULSE_UNNECESSARY_COPY_ASSIGNMENT

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Assignment" by [pulse](/docs/next/checker-pulse).*

See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy).
## PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Assignment from Const" by [pulse](/docs/next/checker-pulse).*

See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy).
## PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Assignment Movable" by [pulse](/docs/next/checker-pulse).*

See [PULSE_UNNECESSARY_COPY_MOVABLE](#pulse_unnecessary_copy_movable).
## PULSE_UNNECESSARY_COPY_INTERMEDIATE

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Intermediate" by [pulse](/docs/next/checker-pulse).*

This is reported when Infer detects an unnecessary temporary copy of an intermediate object where copy is created to be passed down to a function unnecessarily. Instead, the intermediate object should either be moved into the callee or the type of the callee's parameter should be made `const &`.

A prime example of this occurs when we call a function with a call-by-value parameter as follows:

```cpp
void callee(ExpensiveObject obj) {
  // ....
}

void caller() {
  callee(myExpensiveObj); // a copy of myExpensiveObj is created
  // the copy is destroyed right after the call  
}
```

In this case, when we call `callee`, under the hood, a copy of the argument `myExpensiveObj` is created to be passed to the function call. However, the copy might be unnecessary if

 -   `callee` doesn’t modify its parameter → then we can change its type to `const ExpensiveObject&`, getting rid of the copy at caller
 -   even if `callee` might modify the object, if the argument `myExpensiveObj` is never used later on, we can get rid of the copy by moving it instead: `callee(std::move(myExpensiveObj))`.


The analysis is careful about suggesting moves blindly though: if the argument `myExpensiveObj` is of type `const & ExpensiveObject` then we also recommend that for move to work, const-reference needs to be removed.


PS: We check for other conditions on the argument here: e.g. it should be local to the procedure, as moving a non-local member might cause other memory correctness issues like use-after-move later on.
## PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Intermediate from Const" by [pulse](/docs/next/checker-pulse).*

See [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy).
## PULSE_UNNECESSARY_COPY_MOVABLE

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Movable" by [pulse](/docs/next/checker-pulse).*

This is reported when Infer detects an unnecessary copy into a field where
- the source is an rvalue-reference
- the source is not modified before it goes out of scope or is destroyed.

Note that the copy can be modified since it has the ownership of the object.

Fix: Rather than the copying into the field, the source should be moved into it.

For example,

```cpp
struct A {
  std::vector<int> vec;
};

class Test {
  A mem_a;

  void unnecessary_copy(A&& src) {
   mem_a = src;
   // fix is to move as follows
   // mem_a = std::move(src);
  }

};

```
## PULSE_UNNECESSARY_COPY_OPTIONAL

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy to Optional" by [pulse](/docs/next/checker-pulse).*

This is reported when Infer detects an unnecessary copy of an object via `optional` value
construction where the source is not modified before it goes out of scope.  To avoid the copy, we
can move the source object or change the callee's type.

For example,

```cpp
void get_optional_value(std::optional<A> x) {}

void pass_non_optional_value(A x) {
  get_optional_value(x);
  // fix is to move as follows
  // get_optional_value(std::move(x));
}
```

## PULSE_UNNECESSARY_COPY_OPTIONAL_CONST

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy to Optional from Const" by [pulse](/docs/next/checker-pulse).*

See [PULSE_UNNECESSARY_COPY_OPTIONAL](#pulse_unnecessary_copy_optional).
## PULSE_UNNECESSARY_COPY_RETURN

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Return" by [pulse](/docs/next/checker-pulse).*

This is similar to [PULSE_UNNECESSARY_COPY](#pulse_unnecessary_copy), but reported when a callee returns a copied value and it is not modified in its caller.  We may be able to return const-ref typed value or try `std::move` to avoid the copy.

For example,

```cpp
class MyClass {
  T v;
 public:
  T get() {
    return v; // v is copied here, which is avoidable.
  }
};

void caller(MyClass obj) {
  T x = obj.get();
  std::cout << x; // x is not modified.
}
```

## PULSE_UNNECESSARY_COPY_THRIFT_ASSIGNMENT

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Unnecessary Copy Assignment into Thrift" by [pulse](/docs/next/checker-pulse).*

This is similar to [PULSE_UNNECESSARY_COPY_ASSIGNMENT](#pulse_unnecessary_copy_assignment), but is
reported when copied into thrift fields.

## PURE_FUNCTION

*Reported as "Pure Function" by [purity](/docs/next/checker-purity).*

This issue type indicates pure functions. For instance, below functions would be marked as pure:

```java
int local_write_pure(int x, int y) {
  int k = x + y;
  k++;
  return k;
}

// no change to outside state, the local allocation is ok.
int local_alloc_pure(ArrayList<Integer> list) {
  ArrayList<Integer> list_new = new ArrayList<Integer>();
  for (Integer el : list) {
    list_new.add(el);
  }
  return list_new.size();
}
```

However, the following ones would not be pure:

```java
void swap_impure(int[] array, int i, int j) {
  int tmp = array[i];
  array[i] = array[j]; // modifying the input array
  array[j] = tmp;
}

int a = 0;
void set_impure(int x, int y) {
  a = x + y; //modifying a global variable
}
```

## REGEX_OP_ON_UI_THREAD

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Regex Op On Ui Thread" by [starvation](/docs/next/checker-starvation).*

A potentially costly operation on a regular expression occurs on the UI thread.
## RETAIN_CYCLE

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Retain Cycle" by [pulse](/docs/next/checker-pulse).*

A retain cycle is a situation when object A retains object B, and object B
retains object A at the same time. Here is an example:

```objectivec
@class Child;
@interface Parent : NSObject {
    Child *child; // Instance variables are implicitly __strong
}
@end
@interface Child : NSObject {
    Parent *parent;
}
@end
```

You can fix a retain cycle in ARC by using \_\_weak variables or weak properties
for your "back links", i.e. links to direct or indirect parents in an object
hierarchy:

```objectivec
@class Child;
@interface Parent : NSObject {
    Child *child;
}
@end
@interface Child : NSObject {
    __weak Parent *parent;
}
@end
```

## RETAIN_CYCLE_NO_WEAK_INFO

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Retain Cycle No Weak Info" by [pulse](/docs/next/checker-pulse).*

A retain cycle is a situation when object A retains object B, and object B
retains object A at the same time. Here is an example:

```objectivec
@class Child;
@interface Parent : NSObject {
    Child *child; // Instance variables are implicitly __strong
}
@end
@interface Child : NSObject {
    Parent *parent;
}
@end
```

You can fix a retain cycle in ARC by using \_\_weak variables or weak properties
for your "back links", i.e. links to direct or indirect parents in an object
hierarchy:

```objectivec
@class Child;
@interface Parent : NSObject {
    Child *child;
}
@end
@interface Child : NSObject {
    __weak Parent *parent;
}
@end
```

## SCOPE_LEAKAGE

*Category: [Sensitive data flow](/docs/next/all-categories#sensitive-data-flow). Reported as "Scope Leakage" by [scope-leakage](/docs/next/checker-scope-leakage).*

This issue type indicates that a class with scope annotation A stores a field
with whose (dynamic) type (or one of its super types) is annotated with scope
B such that a scope nesting restriction is violated. By "stores", we mean
either directly or transitively.

A configuration is used to list the set of scopes and the must-not-hold relation.

In the following Java example, the set of scopes is Outer and Inner, and the must-not-hold
relation is simply \{(Outer, Inner)\}:
```java
@ScopeType(value = Outer.class)
class ClassOfOuterScope {
  final ClassOfInner c = new ClassOfInner(); // <-- warn here that ClassOfInner would leak.
}

@ScopeType(value = Inner.class)
class ClassOfInner {}
```

Here is a more detailed description of the analysis.

This analysis operates over Java bytecode. It assumes that types (classes, interfaces, enums,
etc.) may be annotated with so-called scope annotations. The analysis is parameterized by a set
of scopes and a "must-not-hold" relation over pairs of scopes, which it reads from a
configuration file.

The analysis aims to detect violations of the following property: if there exist a path of
fields from object OA to object OB and the type of OA (or one of its super-types) is annotated
with scope SA and the type of OB (or one of its super-types) is annotated with scope SB then
must-not-hold(SA, SB) must be false. Intuitively, the given objects have different scopes that
should not be nested, for example, different intended lifetimes, and a forbidden path from OA to
OB results in OB "leaking" out of the scope SA.

The implementation reads a configuration to determine a list of (scope) "generators" for each
type of scope and a scope class for each type of scope. A generator for a scope type SA is given
by the name of a class and a list of methods where it is understood that any of the methods
listed for the given class returns an object that is known to have scope SA. (This can be seen
as a form of lightweight modeling.) A scope class is the name of the class that represents a
given scope.

## SELF_IN_BLOCK_PASSED_TO_INIT

*Category: [Resource leak](/docs/next/all-categories#resource-leak). Reported as "Self In Block Passed To Init" by [self-in-block](/docs/next/checker-self-in-block).*

This check flags when `self` is captured in a block that is passed to an initialiser method. That
could cause retain cycles if the initialiser code retains the block.

Example:

```objectivec
  [obj initWithHandler:^() {
    [self foo];
    ...
  }];
```

Instead it's better to use the `weakSelf`/`strongSelf` pattern.

```objectivec
  __weak __typeof(self) weakSelf = self;
  [obj initWithHandler:^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
        [strongSelf foo];
    }
    ...
  }];
```

## SENSITIVE_DATA_FLOW

*Category: [Sensitive data flow](/docs/next/all-categories#sensitive-data-flow). Reported as "Sensitive Data Flow" by [pulse](/docs/next/checker-pulse).*

A flow of sensitive data was detected from a source.
## STACK_VARIABLE_ADDRESS_ESCAPE

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Stack Variable Address Escape" by [pulse](/docs/next/checker-pulse).*

Reported when an address pointing into the stack of the current
function will escape to its calling context. Such addresses will
become invalid by the time the function actually returns so are
potentially dangerous.

For example, directly returning a pointer to a local variable:

```C
int* foo() {
   int x = 42;
   return &x; // <-- warn here that "&x" will escape
}
```

## STARVATION

*Reported as "UI Thread Starvation" by [starvation](/docs/next/checker-starvation).*

This error is reported in Java, and specifically on Android. These reports are
triggered when a method that runs on the UI thread may block, thus potentially
leading to an Application Not Responding error.

Infer considers a method as running on the UI thread whenever:

- The method, one of its overrides, its class, or an ancestral class, is
  annotated with `@UiThread`.
- The method, or one of its overrides is annotated with `@OnEvent`, `@OnClick`,
  etc.
- The method or its callees call a `Litho.ThreadUtils` method such as
  `assertMainThread`.

The issue is reported when a method deemed to run on the UI thread

- Makes a method call which may block.
- Takes a lock, and another thread takes the same lock, and before releasing it,
  makes a call that may block.

Calls that may block are considered:

- Certain I/O calls.
- Two way `Binder.transact` calls.
- Certain OS calls.
- `Future` or `AsyncTask` calls to `get` without timeouts, or with too large
  timeouts.

To suppress starvation reports in a method `m()` use the
`@SuppressLint("STARVATION")` annotation, as follows:

```java
  import android.annotation.SuppressLint;

  @SuppressLint("STARVATION")
  public void m() {
  ...
  }
```

To signal to Infer that a method does not perform any blocking calls, despite
appearences, you can use the `@NonBlocking` annotation:

```java
  import com.facebook.infer.annotation.NonBlocking;

  @NonBlocking
  public void m() {
  ...
  }
```

This instructs Infer to filter out any potentially blocking calls in `m()`
(also, transitively), and thus any other method can expect no starvation reports
due to a call to `m()`. You will need to set up your class path appropriately to
include the JAR files in `infer/annotations` for this annotation to work.

## STATIC_CONSTRUCTOR_STALL

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "Static Constructor Stall" by [static-constructor-stall-checker](/docs/next/checker-static-constructor-stall-checker).*

Calling certain methods, for instance dispatch_once, during the static initialization of objects is risky. It could cause deadlocks, because other objects might not have been initialized yet.
## STATIC_INITIALIZATION_ORDER_FIASCO

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Static Initialization Order Fiasco" by [siof](/docs/next/checker-siof).*

This error is reported in C++. It fires when the initialization of a static
variable `A`, accesses a static variable `B` from another translation unit
(usually another `.cpp` file). There are no guarantees whether `B` has been
already initialized or not at that point.

For more technical definition and techniques to avoid/remediate, see the
[FAQ](https://isocpp.org/wiki/faq/ctors#static-init-order).

## STRICT_MODE_VIOLATION

*Category: [Perf regression](/docs/next/all-categories#perf-regression). Reported as "Strict Mode Violation" by [starvation](/docs/next/checker-starvation).*

Android has a feature called
[strict mode](https://developer.android.com/reference/android/os/StrictMode),
which if enabled, will flag the occasions where the main thread makes a call
that results in disk I/O, waiting on a network socket, etc. The analysis
catching starvation errors and deadlocks (the `--starvation` analysis) has the
ability to statically detect such violations.

To suppress this warning, it's enough to annotate the offending method with
`@SuppressLint("STRICT_MODE_VIOLATION")`.

## STRONG_SELF_NOT_CHECKED

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "StrongSelf Not Checked" by [self-in-block](/docs/next/checker-self-in-block).*

This checks reports a potential issue when a block captures `weakSelf` (a weak pointer to `self`),
then one assigns this pointer to a local variable `strongSelf` inside the block and uses this variable
without checking first whether it is `nil`. The problem here is that the weak pointer could be `nil` at
the time when the block is executed. So, the correct usage is to first check whether `strongSelf` is a valid
pointer, and then use it.

Example:

```objectivec
__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    int y = strongSelf->x;
    ...
```

**Action:**
Add a check for `nil`:

```objectivec
__weak __typeof(self) weakSelf = self;
  int (^my_block)() = ^() {
    __strong __typeof(weakSelf) strongSelf = weakSelf;
    if (strongSelf) {
      int y = strongSelf->x;
      ...
    }
```

*Limitations:* To keep this check simple and intra-procedural, we rely on names to find `weakSelf`:
we assume that any captured weak pointer whose name contains "self" is a weak reference to `self`.
In contrast, `strongSelf` is a local variable to the block, so the check supports any name given to
a local strong pointer that has been assigned `weakSelf`.

## SWIFT_NPE

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Swift Null Dereference" by [pulse](/docs/next/checker-pulse).*

Pulse detected a Swift code path that reads from an Optional value known
to be `nil`. The dereference itself is unsafe -- not the surrounding
type annotation.

The check is Swift-specific and considers an unwrap unsafe only when the
`.none` case is reachable along some path. Unwraps on values that are
known `.some` (literal payload, prior `if let` / `guard let` binding,
`??` default) are silent. Unknown receivers (e.g. the result of an
unmodelled extern call) are also silent.

## Force-unwrap of an Optional whose `nil` case is reachable

```swift
func unwrapsKnownNil_bad() {
  let x: Int? = nil
  _ = x!                 // SWIFT_NPE: x is known .none here
}
```

Fix by binding the value before use:

```swift
func unwrapsKnownNil_good() {
  let x: Int? = nil
  if let v = x {
    _ = v                 // OK: only reached on the .some branch
  }
}
```

Or provide a default:

```swift
func defaultsToZero_good() {
  let x: Int? = nil
  let _ = x ?? 0          // OK: no force-unwrap
}
```

## Implicitly Unwrapped Optional (`T!`) whose underlying value is `nil`

`T!` types are written as non-optional but compile to `Optional<T>` and
trap on access if the value is `nil`.

```swift
func iuoFromBridge_bad(api: LegacyAPI) {
  let s: String! = api.getUnannotatedString()   // ObjC returns nullable
  _ = s.count                                   // SWIFT_NPE on .none
}
```

Treat the value as a regular Optional and bind it explicitly:

```swift
func iuoBound_good(api: LegacyAPI) {
  guard let s = api.getUnannotatedString() else { return }
  _ = s.count                                   // OK
}
```

If the underlying source can be annotated, mark the ObjC return
`_Nonnull` (or change the Swift type from `T?` / `T!` to `T`) so the
guarantee shows up in the signature.

## `Optional.unsafelyUnwrapped` on a known-`nil` receiver

```swift
func unsafelyUnwrappedNil_bad() {
  let x: Int? = nil
  _ = x.unsafelyUnwrapped       // SWIFT_NPE
}
```

`unsafelyUnwrapped` has the same trap semantics as `!` but skips the
runtime check in optimised builds. Prefer the same fixes as above
(`if let`, `guard let`, `??`).

## SWIFT_NPE_LATENT

*Category: [Null pointer dereference](/docs/next/all-categories#null-pointer-dereference). Reported as "Swift Null Dereference" by [pulse](/docs/next/checker-pulse).*

A latent [SWIFT_NPE](#swift_npe). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## TAINT_ERROR

*Category: [Sensitive data flow](/docs/next/all-categories#sensitive-data-flow). Reported as "Taint Error" by [pulse](/docs/next/checker-pulse).*

A taint flow was detected from a source to a sink
## THREAD_SAFETY_VIOLATION

*Category: [Concurrency](/docs/next/all-categories#concurrency). Reported as "Thread Safety Violation" by [racerd](/docs/next/checker-racerd).*

This warning indicates a potential data race in Java. The analyser is called
RacerD and this section gives brief but a mostly complete description of its
features. See the [RacerD page](/docs/next/checker-racerd) for more in-depth information and
examples.

### Thread-safety: What is a data race

Here a data race is a pair of accesses to the same member field such that:

- at least one is a write, and,
- at least one occurs without any lock synchronization, and,
- the two accesses occur on threads (if known) which can run in parallel.

### Thread-safety: Potential fixes

- Synchronizing the accesses (using the `synchronized` keyword, thread-exclusion
  such as atomic objects, `volatile` etc).
- Making an offending method private -- this will exclude it from being checked
  at the top level, though it will be checked if called by a public method which
  may itself, e.g., hold a lock when calling it.
- Putting the two accesses on the same thread, e.g., by using `@MainThread` or
  `@ThreadConfined`.

### Thread-safety: Conditions checked before reporting

The class and method are not marked `@ThreadSafe(enableChecks = false)`, and,

- The method is declared `synchronized`, or employs (non-transitively) locking,
  or,
- The class is not marked `@NotThreadSafe`, and,
  - The class/method is marked `@ThreadSafe,` or one of the configured synonyms
    in `.inferconfig`, or,
  - A parent class, or an override method are marked with the above annotations.

NB currently RacerD **does not take into account `@GuardedBy`**.

### Thread-safety: Thread annotations recognized by RacerD

These class and method annotations imply the method is on the main thread:
`@MainThread`, `@UiThread`

These method annotations imply the method is on the main thread: `@OnBind`,
`@OnEvent`, `@OnMount`, `@OnUnbind`, `@OnUnmount`

Both classes of annotations work through the inheritance tree (i.e. if a parent
class or method is marked with one of these annotations, so is the child class /
method override).

In addition to these, RacerD recognizes many lifecycle methods as necessarily
running on the main thread, eg `Fragment.onCreate` etc.

Finally, the thread status of being on the main thread propagates backwards
through the call graph (ie if `foo` calls `bar` and `bar` is marked `@UiThtread`
then `foo` is automatically considered on the main thread too). Calling
`assertMainThread`, `assertOnUiThread`, `checkOnMainThread` has the same effect.

NB RacerD currently **does not recognize `@WorkerThread`, `@BinderThread` or
`@AnyThread`**.

### Thread-safety: Other annotations and what they do

These annotations can be found at `com.facebook.infer.annotation.*`.

- `@Functional` This is a method annotation indicating the method always returns
  the same value. When a method `foo` is annotated `@Functional`, RacerD will
  ignore any writes of the return value of `foo`. For example, in
  `this.x = foo()`, the write to `this.x` is ignored. The reasoning is that if
  the method returns the same value whenever it's called, any data race on
  `this.x` is benign, if that is the only write.

- `@ThreadConfined` This is a class/method/field annotation which takes a single
  parameter which can be `UI`, `ANY` or a user chosen string. It indicates to
  RacerD a thread identifier for the class/method/field. Thus,
  `@ThreadConfined(UI)` is equivalent to `@UiThread`, and `@ThreadConfined(ANY)`
  is equivalent to not having the annotation at all, for classes and methods.
  When this annotation is applied to a field it instructs Infer to assume
  (without checking) that all accesses to that field are made on the same thread
  (and can, therefore, not race by definition). The intention is that RacerD
  uses that to detect exclusion between accesses occurring on the same thread.
  However, only the UI thread is supported at this time, and any user provided
  value is considered equal to `UI`.

- `@VisibleForTesting` A method annotation making Infer consider the method as
  effectively `private`. This means it will not be checked for races against
  other non-private methods of the class, but only if called by one.

- `@ReturnsOwnership` A method annotation indicating that the method returns a
  freshly owned object. Accesses to the returned value will not be considered
  for data races, as the object is in-effect unique and not accessible yet from
  other threads. The main utility of this annotation is in interfaces, where
  Infer cannot look up the implementation and decide for itself.

## TOPL_ERROR

*Category: [User defined property](/docs/next/all-categories#user-defined-property). Reported as "Topl Error" by [topl](/docs/next/checker-topl).*

A violation of a Topl property (user-specified).
There is an execution path in the code that drives a Topl property from a start state to an error state.

This indicates that the code has a user-defined undesired behavior.

See [Topl](/docs/next/checker-topl#what-is-it) for an example

## TOPL_ERROR_LATENT

*Category: [User defined property](/docs/next/all-categories#user-defined-property). Reported as "Topl Error Latent" by [topl](/docs/next/checker-topl).*

A latent [TOPL_ERROR](#topl_error). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## USE_AFTER_DELETE

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Delete" by [pulse](/docs/next/checker-pulse).*

An address that was invalidated by a call to `delete` in C++ is dereferenced.

## USE_AFTER_DELETE_LATENT

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Delete Latent" by [pulse](/docs/next/checker-pulse).*

A latent [USE_AFTER_DELETE](#use_after_delete). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## USE_AFTER_FREE

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Free" by [pulse](/docs/next/checker-pulse).*

An address that was invalidated by a call to `free` in C is dereferenced.

## USE_AFTER_FREE_LATENT

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Free Latent" by [pulse](/docs/next/checker-pulse).*

A latent [USE_AFTER_FREE](#use_after_free). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## USE_AFTER_LIFETIME

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Lifetime" by [pulse](/docs/next/checker-pulse).*

The lifetime of an object has ended but that object is being
accessed. For example, the address of a variable holding a C++ object
is accessed after the variable has gone out of scope:

```cpp
void foo() {
     X* p;
     { // new scope
       X x = X();
       p = &x;
     } // x has gone out of scope
     p->method(); // ERROR: you should not access *p after x has gone out of scope
}
```

## USE_AFTER_LIFETIME_LATENT

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Use After Lifetime Latent" by [pulse](/docs/next/checker-pulse).*

A latent [USE_AFTER_LIFETIME](#use_after_lifetime). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## VECTOR_INVALIDATION

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Vector Invalidation" by [pulse](/docs/next/checker-pulse).*

An address pointing into a C++ `std::vector` might have become
invalid. This can happen when an address is taken into a vector, then
the vector is mutated in a way that might invalidate the address, for
example by adding elements to the vector, which might trigger a
re-allocation of the entire vector contents (thereby invalidating the
pointers into the previous location of the contents).

For example:

```cpp
void deref_vector_element_after_push_back_bad(std::vector<int>& vec) {
  int* elt = &vec[1];
  int* y = elt;
  vec.push_back(42); // if the array backing the vector was full already, this
                     // will re-allocate it and copy the previous contents
                     // into the new array, then delete the previous array
  std::cout << *y << "\n"; // bad: y might be invalid
}
```

## VECTOR_INVALIDATION_LATENT

*Category: [Memory error](/docs/next/all-categories#memory-error). Reported as "Vector Invalidation Latent" by [pulse](/docs/next/checker-pulse).*

A latent [VECTOR_INVALIDATION](#vector_invalidation). See the [documentation on Pulse latent issues](/docs/next/checker-pulse#latent-issues).
## WEAK_SELF_IN_NO_ESCAPE_BLOCK

*Reported as "Weak Self In No Escape Block" by [self-in-block](/docs/next/checker-self-in-block).*

This check reports when `weakSelf` (a weak pointer to `self`) is used in
a block, and this block is passed to a "no escaping" method. This means that
the block passed to that method won't be leaving the current scope, this is
marked with the annotation `NS_NOESCAPE`.

The issue here is that, because the block is "no escaping", there is no need to use
`weakSelf` and `strongSelf` but we can just use `self`. This has the advantage of
not needing to deal with the added complexity of weak pointers, and it simplifies the
code.

Example:

```objectivec
  __weak __typeof(self) weakSelf = self;
  [self foo:^() { //foo's first parameter is annotates with `NS_NOESCAPE`
      [weakSelf bar];
  }];
```

**Action**:

Replace `weakSelf` with `self`:

```objectivec
  [self foo:^() {
      [self bar];
  }];
```

*Limitations:* To keep this check simple and intra-procedural, we rely on names to find `weakSelf`:
we assume that any captured weak pointer whose name contains "self" is a weak reference to `self`.

---

### Checker Annotation Reachability (`website/docs/checker-annotation-reachability.md`)

---
title: "Annotation Reachability"
description: "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`."
---

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`.

Activate with `--annotation-reachability`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: Yes
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: Experimental



## List of Issue Types

The following issue types are reported by this checker:
- [CHECKERS_ALLOCATES_MEMORY](/docs/next/all-issue-types#checkers_allocates_memory)
- [CHECKERS_ANNOTATION_REACHABILITY_ERROR](/docs/next/all-issue-types#checkers_annotation_reachability_error)
- [CHECKERS_CALLS_EXPENSIVE_METHOD](/docs/next/all-issue-types#checkers_calls_expensive_method)
- [CHECKERS_EXPENSIVE_OVERRIDES_UNANNOTATED](/docs/next/all-issue-types#checkers_expensive_overrides_unannotated)

---

### Checker Bufferoverrun (`website/docs/checker-bufferoverrun.md`)

---
title: "Buffer Overrun Analysis (InferBO)"
description: "InferBO is a detector for out-of-bounds array accesses."
---

InferBO is a detector for out-of-bounds array accesses.

**\*\*\*DEPRECATED\*\*\*** Use Pulse instead.

Activate with `--bufferoverrun`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

You can read about its origins in this [blog post](https://research.fb.com/inferbo-infer-based-buffer-overrun-analyzer/).

## List of Issue Types

The following issue types are reported by this checker:
- [BUFFER_OVERRUN_L1](/docs/next/all-issue-types#buffer_overrun_l1)
- [BUFFER_OVERRUN_L2](/docs/next/all-issue-types#buffer_overrun_l2)
- [BUFFER_OVERRUN_L3](/docs/next/all-issue-types#buffer_overrun_l3)
- [BUFFER_OVERRUN_L4](/docs/next/all-issue-types#buffer_overrun_l4)
- [BUFFER_OVERRUN_L5](/docs/next/all-issue-types#buffer_overrun_l5)
- [BUFFER_OVERRUN_S2](/docs/next/all-issue-types#buffer_overrun_s2)
- [BUFFER_OVERRUN_U5](/docs/next/all-issue-types#buffer_overrun_u5)
- [INFERBO_ALLOC_IS_BIG](/docs/next/all-issue-types#inferbo_alloc_is_big)
- [INFERBO_ALLOC_IS_NEGATIVE](/docs/next/all-issue-types#inferbo_alloc_is_negative)
- [INFERBO_ALLOC_IS_ZERO](/docs/next/all-issue-types#inferbo_alloc_is_zero)
- [INFERBO_ALLOC_MAY_BE_BIG](/docs/next/all-issue-types#inferbo_alloc_may_be_big)
- [INFERBO_ALLOC_MAY_BE_NEGATIVE](/docs/next/all-issue-types#inferbo_alloc_may_be_negative)
- [INTEGER_OVERFLOW_L1](/docs/next/all-issue-types#integer_overflow_l1)
- [INTEGER_OVERFLOW_L2](/docs/next/all-issue-types#integer_overflow_l2)
- [INTEGER_OVERFLOW_L5](/docs/next/all-issue-types#integer_overflow_l5)
- [INTEGER_OVERFLOW_U5](/docs/next/all-issue-types#integer_overflow_u5)

---

### Checker Config Gating (`website/docs/checker-config-gating.md`)

---
title: "Config Gating"
description: "Determines which config flags gate the execution of each line of code."
---

Determines which config flags gate the execution of each line of code.

Activate with `--config-gating`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Experimental
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [CONFIG_GATED](/docs/next/all-issue-types#config_gated)
- [CONFIG_UNGATED](/docs/next/all-issue-types#config_ungated)

---

### Checker Config Impact Analysis (`website/docs/checker-config-impact-analysis.md`)

---
title: "Config Impact Analysis"
description: "[EXPERIMENTAL] Collects function that are called without config checks."
---

[EXPERIMENTAL] Collects function that are called without config checks.

Activate with `--config-impact-analysis`.

Supported languages:
- C/C++/ObjC: Experimental
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Experimental
- Python: No
- Rust: No
- Swift: No

This checker collects functions whose execution isn't gated by certain pre-defined gating functions. The set of gating functions is hardcoded and empty by default for now, so to use this checker, please modify the code directly in [FbGKInteraction.ml](https://github.com/facebook/infer/tree/main/infer/src/opensource).

## List of Issue Types

The following issue types are reported by this checker:
- [CONFIG_IMPACT](/docs/next/all-issue-types#config_impact)
- [CONFIG_IMPACT_STRICT](/docs/next/all-issue-types#config_impact_strict)

---

### Checker Cost (`website/docs/checker-cost.md`)

---
title: "Cost: Complexity Analysis"
description: "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`."
---

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`.

Activate with `--cost`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: Experimental
- Java: Yes
- Python: No
- Rust: No
- Swift: No

Cost analysis statically estimates an upper bound on the worst-case execution cost of a program (WCET). This page gives an overview of how the analysis works for *Java* code. The analyser also has limited support for C/C++ and Objective-C.

To run the analysis, you can use run `infer --cost` (which will run cost analysis along with other
analyses that are run by default) or `infer --cost-only` (which will only run cost analysis).

For example, the command `infer --cost-only -- javac File.java` will run
cost analysis on `File.java`.


## How the analysis works

The analysis computes symbolic upper bounds on the resource usage of programs—-execution cost being the main resource we consider. These costs are expressed in terms of polynomials describing the asymptotic complexity of procedures with respect to their input sizes. The main input of the analysis is the source file which is then translated to an intermediate language along with the control-flow graph of the program. The analysis then operates on this intermediate language in several phases:
- 1) a numerical value analysis based on [InferBo](/docs/checker-bufferoverrun) computes value ranges for instructions accessing memory
- 2) a loop bound analysis determines upper bounds for the number of iterations of loops and generates constraints for nodes in the control-flow graph
- 3) a constraint solving step resolves the constraints generated in the second step and computes an upper bound on the execution cost.

Most ideas behind this analysis are based on Stefan Bydge's PhD thesis [Static WCET Analysis based on Abstract Interpretation and Counting of Elements](https://www.semanticscholar.org/paper/Static-WCET-Analysis-Based-on-Abstract-and-Counting-Bygde/ee5157164d497725c1f42dc6c475a59a87c99957).

The analysis computes two things for each node in the CFG:
- the cost of its instructions, i.e. how much one execution of this node costs,
- how many times it can be executed (part 2 above)

The total cost of the node is the scalar product of these two vectors. Then, these are passed to a constraint solver (part 3 above) that computes the execution cost of the procedure based on the incoming/outgoing edges.


The results of the analysis are written into `costs-report.json` where for each procedure, we record the actual polynomial (for the execution cost) along with the degree of the polynomial, the procedure name, line number etc.



## Types of resources/costs

Although the analysis was initially designed to reason about the execution cost, it is not limited to inferring bounds for just execution cost. In order to statically detect regressions in other types of resource usage, we have generalized the analysis to account costs for different types of resources such as Objective-C's autorelease pool size or memory allocations.


Currently, there are three types of resources/costs the analysis operates on:
- 1) execution cost
- 2) allocation cost
- 3) autoreleasepool size

For 1), the analysis assumes a simple sequential model with an abstract cost semantics: each primitive instruction in the intermediate language (SIL) is assumed to incur a unit execution cost. 

For 2), the analysis only incurs costs for primitive operations that allocate memory (e.g. `new`). This is in experimental mode and hence the results are not written into `costs-report.json`. 

For 3), the analysis incurs a cost when objects are added to Objective-C's `@autoreleasepool`. This usually happens in two cases: 1) when `autorelease` is called explicitly in non-ARC compiled code and 2) when an (autoreleased) object pointer is returned from non-ARC compiled callee to ARC compiled caller, and vice-versa. 


## Examples (execution cost)

For instance, assume that we had the following program:

```java
void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
  }
}
```

Infer statically infers a polynomial (e.g. `8 · |list|+16`) for the execution cost of this program by giving each instruction in Infer's intermediate language a symbolic cost (where `|...|` refers to the length of a list). Here---overlooking the actual constants---the analysis infers that this program’s asymptotic complexity is `O(|list|)`, that is loop is linear in the size of its input list. Then, at diff time, if a developer modifies this code to,

```java
void loop(ArrayList<Integer> list){
  for (int i = 0; i <= list.size(); i++){
    foo(i); // newly added function call
  }
}
```

where `foo` has a linear cost in its parameter, then Infer automatically detects that the complexity of loop has increased from `O(|list|)` to `O(|list|^2)` and then reports an [`EXECUTION_TIME_COMPLEXITY_INCREASE`](/docs/next/all-issue-types#execution_time_complexity_increase) issue.

## Differential mode
Unlike other Infer analyses (which on reports found issues/bugs in `report.json` when running infer once), cost analysis also has a special mode that reports an issue for differential analysis (i.e. when comparing the analysis results on the original and the modified files). For each procedure, `costs-report.json` includes the actual polynomial (for the execution cost) along with the degree of the polynomial, the procedure name, line number etc. Then, in the differential mode, these `costs-report.json` files are compared. 

Differential cost analysis in action:
- first run infer's cost analysis on `File.java` and copy `inter-out/costs-report.json` to `previous-costs-report.json` (Note that the file should be copied outside the result directory because the directory will be removed in the second infer run.)
- modify `File.java` as shown above
- re-run infer on `File.java` and copy `infer-out/costs-report.json` to `current-costs-report.json`
- run `infer reportdiff --costs-current current-costs-report.json --costs-previous previous-costs-report.json`.
- Inspect `infer-out/differential/introduced.json` to see the newly found complexity increase issue(s).


## Limitations

There are a number of known limitations to the design of the static cost analysis:

- [InferBo](/docs/checker-bufferoverrun) 's intervals are limited to affine expressions, not full-blown polynomials. Hence, we can not automatically infer bounds involving square roots.

- We do not handle recursion.

- If the execution cost of a program depends on an unknown call (e.g. due to iterating over an unmodeled library call), we can't compute a static upper bound and return T (unknown cost). See [INFINITE_EXECUTION_COST](/docs/next/all-issue-types#infinite_execution_time) for details.


## List of Issue Types

The following issue types are reported by this checker:
- [EXECUTION_TIME_COMPLEXITY_INCREASE](/docs/next/all-issue-types#execution_time_complexity_increase)
- [EXECUTION_TIME_COMPLEXITY_INCREASE_UI_THREAD](/docs/next/all-issue-types#execution_time_complexity_increase_ui_thread)
- [EXECUTION_TIME_UNREACHABLE_AT_EXIT](/docs/next/all-issue-types#execution_time_unreachable_at_exit)
- [EXPENSIVE_EXECUTION_TIME](/docs/next/all-issue-types#expensive_execution_time)
- [INFINITE_EXECUTION_TIME](/docs/next/all-issue-types#infinite_execution_time)

---

### Checker Fragment Retains View (`website/docs/checker-fragment-retains-view.md`)

---
title: "Fragment Retains View"
description: "Detects when Android fragments are not explicitly nullified before becoming unreachable."
---

Detects when Android fragments are not explicitly nullified before becoming unreachable.

Activate with `--fragment-retains-view`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [CHECKERS_FRAGMENT_RETAINS_VIEW](/docs/next/all-issue-types#checkers_fragment_retains_view)

---

### Checker Impurity (`website/docs/checker-impurity.md`)

---
title: "Impurity"
description: "Detects functions with potential side-effects. Same as \"purity\", but implemented on top of Pulse."
---

Detects functions with potential side-effects. Same as "purity", but implemented on top of Pulse.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

Activate with `--impurity`.

Supported languages:
- C/C++/ObjC: Experimental
- C#/.Net: No
- Erlang: No
- Hack: Experimental
- Java: Experimental
- Python: No
- Rust: No
- Swift: No

This is an experimental inter-procedural analysis that detects impure functions. It is meant to be an improvement over the [purity](/docs/next/checker-purity) analysis with a negation on the issue types. For each function, impurity analysis keeps track of not only the impurity of the function but also some additional information such as which parameters/globals the function modifies. It models functions with no summary/model as impure. The analysis relies on [Pulse](/docs/next/checker-pulse) summaries to determine impurity.


## List of Issue Types

The following issue types are reported by this checker:
- [IMPURE_FUNCTION](/docs/next/all-issue-types#impure_function)
- [MODIFIES_IMMUTABLE](/docs/next/all-issue-types#modifies_immutable)

---

### Checker Inefficient Keyset Iterator (`website/docs/checker-inefficient-keyset-iterator.md`)

---
title: "Inefficient keySet Iterator"
description: "Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly."
---

Check for inefficient uses of iterators that iterate on keys then lookup their values, instead of iterating on key-value pairs directly.

Activate with `--inefficient-keyset-iterator`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [INEFFICIENT_KEYSET_ITERATOR](/docs/next/all-issue-types#inefficient_keyset_iterator)

---

### Checker Lineage (`website/docs/checker-lineage.md`)

---
title: "Lineage"
description: "Computes a dataflow graph"
---

Computes a dataflow graph

Activate with `--lineage`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: Yes
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [LINEAGE_FLOW](/docs/next/all-issue-types#lineage_flow)

---

### Checker Litho Required Props (`website/docs/checker-litho-required-props.md`)

---
title: "Litho \"Required Props\""
description: "Checks that all non-optional `@Prop`s have been specified when constructing Litho components."
---

Checks that all non-optional `@Prop`s have been specified when constructing Litho components.

Activate with `--litho-required-props`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

This analysis checks that all non-optional [`@Prop`](https://fblitho.com/docs/props)`s have been specified when constructing Litho components. This is a [Litho](https://fblitho.com/) specific checker.


## What are required Props?
In a nutshell, a Litho Component is essentially a class that defines immutable inputs, called prop (annotated with `@Prop`) in component hierarchy methods. For each Component there is a corresponding spec class which defines the required props:. E.g:

```java
class MyComponentSpec {

  static void onCreate(
      ComponentContext c,
      @Prop(optional = true) String prop1, @Prop int prop2) {
    ...
  }
  ...
}
```

`MyComponentSpec` defines two props: a String prop called `prop1` and an int prop named `prop2`. For each prop defined on the spec, the annotation processor creates a builder pattern method that has the same name as the prop.

Developers pass down values for these props by calling the appropriate methods:

```java
MyComponent.create(c)
    .prop1("My prop 1")
    .prop2(256)
    .build();
```

If the required props are not called, then annotation processor throws an exception in run time. This is really bad and that's where this checker comes into play to detect such cases statically.

Note that, the functions `create()` and `build()` could be defined in different methods and there could be various function calls, aliasing, and control flow patterns in between. Hence, this checker is inter-procedural.

Check out the examples defined in the issue type [MISSING_REQUIRED_PROP](/docs/next/all-issue-types#missing_required_prop).

## List of Issue Types

The following issue types are reported by this checker:
- [MISSING_REQUIRED_PROP](/docs/next/all-issue-types#missing_required_prop)

---

### Checker Liveness (`website/docs/checker-liveness.md`)

---
title: "Liveness"
description: "Detection of dead stores and unused variables."
---

Detection of dead stores and unused variables.

Activate with `--liveness`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [DEAD_STORE](/docs/next/all-issue-types#dead_store)

---

### Checker Loop Hoisting (`website/docs/checker-loop-hoisting.md`)

---
title: "Loop Hoisting"
description: "Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency."
---

Detect opportunities to hoist function calls that are invariant outside of loop bodies for efficiency.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

Activate with `--loop-hoisting`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

This checker detects opportunities to hoist function calls that are invariant to outside of loop bodies. The hoisting analysis relies on [purity](/docs/next/checker-purity) analysis to determine whether a function is pure or not.

It has an additional mode that reports [loop-invariant functions that are expensive](/docs/next/all-issue-types#expensive_loop_invariant_call) (i.e. at least linear). This is enabled by the flag `--hoisting-report-only-expensive`.


## List of Issue Types

The following issue types are reported by this checker:
- [EXPENSIVE_LOOP_INVARIANT_CALL](/docs/next/all-issue-types#expensive_loop_invariant_call)
- [INVARIANT_CALL](/docs/next/all-issue-types#invariant_call)

---

### Checker Parameter Not Null Checked (`website/docs/checker-parameter-not-null-checked.md`)

---
title: "Parameter Not Null Checked"
description: "An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first."
---

An Objective-C-specific analysis to detect when a block parameter is used before being checked for null first.

Activate with `--parameter-not-null-checked`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No

This checker checks that an Objective-C block that is passed as a parameter
to a function or method is checked for `nil` before it's being executed.


## List of Issue Types

The following issue types are reported by this checker:
- [BLOCK_PARAMETER_NOT_NULL_CHECKED](/docs/next/all-issue-types#block_parameter_not_null_checked)

---

### Checker Pulse (`website/docs/checker-pulse.md`)

---
title: "Pulse"
description: "General-purpose memory and value analysis engine."
---

General-purpose memory and value analysis engine.

Activate with `--pulse`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: Experimental
- Hack: Yes
- Java: Yes
- Python: No
- Rust: Experimental
- Swift: No

## What is Infer:Pulse?

Pulse is an interprocedural memory safety analysis. Pulse can detect, for instance, [Null dereferences](/docs/next/all-issue-types#nullptr_dereference) in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. An example of a Null dereference found by Pulse is given below.

```java
class Person {
    Person emergencyContact;
    String address;

    Person getEmergencyContact() {
        return this.emergencyContact;
    }
}

class Registry {
    void create() {
        Person p = new Person();
        Person c = p.getEmergencyContact();
        // Null dereference here
        System.out.println(c.address);
    }

    void printContact(Person p) {
        // No null dereference, as we don't know anything about `p`
        System.out.println(p.getEmergencyContact().address);
    }
}
```

How to run pulse for Java:
```bash
infer run --pulse -- javac Test.java
```

Pulse reports a Null dereference on this file on `create()`, as it tries to access the field `address` of object `c`, and `c` has value `null`. In contrast, Pulse gives no report for `printContact(Person p)`, as we cannot be sure that `p.getEmergencyContact()` will return `null`. But, thanks to the fact that the analysis is *inter-procedural*, Pulse will report a Null dereference on calls to `printContact(p)` when it detects that `p` is null.

## Latent Issues

When an error can occur only on some values of the parameters of the current function, Pulse does not report an issue. Such issues are called *latent*. But, if Pulse then sees a call site at which all the conditions for the error are satisfied then the error becomes *manifest* and is reported. This example (in C) illustrates how latent issues are created and then reported when they become manifest:

```c
// for more realism, imagine that this function does other things as well
void set_to_null_if_positive(int n, int** p) {
  if (n > 0) {
    *p = NULL;
  }
}

void latent_null_dereference(int n, int* p) {
  set_to_null_if_positive(n, &p);
  *p = 42; // NULL dereference! but only if n > 0 so no report yet
}

void manifest_error(int *p) {
  // no way to avoid the bug here => Pulse reports an error
  latent_null_dereference(1, p);
}
```

## Unknown Functions

In order to avoid false positives, Pulse makes optimistic assumptions about calls to unknown functions. Unknown functions (or unknown methods) are functions for which Infer didn't find any code. For example, it could be because the function belongs to a third-party library and we know only its signature, or because a function is made through a function pointer that Pulse wasn't able to resolve to a concrete function. In either case, Pulse will scramble the parts of the state reachable from the parameters of the call. In general, this helps avoid false positives but note that this may cause false negatives as well as false positives:

```c
void unknown(int* p); // third-party code that does [*p = 5]
                      // Infer doesn't have access to that code

void false_negative() {
  int* x = (int*) malloc(sizeof(int));
  if (x) {
    // unknown call to x makes Pulse forget that x was allocated, in case it frees x
    unknown(x);
  }
} // no memory leak reported: false negative!

void false_positive(int *x) {
  unknown(x); // this sets *x to 5
  if (x != 5) {
    // unreachable
    int* p = NULL;
    *p = 42; // false positive reported here
  }
}
```

You can check if a given function called any unknown functions by inspecting its Pulse summary. For example, for the code above:
```console
$ infer --pulse-only -- clang -c unknown_code.c
  No issues found
$ infer debug --procedures --procedures-filter 'false_negative' --procedures-summary
...
    skipped_calls={ unknown -> call to skipped function occurs here }
```

## Pulse x Nullsafe

Nullsafe is a type checker for `@Nullable` annotations for Java. Classes following the Nullsafe discipline are annotated with `@Nullsafe`.

Consider the classes `Person` and `Registry` from the previous example. Assuming that class `Person` is annotated with `@Nullsafe`. In this case, we also annotate `getEmergencyContact()` with `@Nullable`, to make explicit that this method can return the `null` value. There is still the risk that classes depending on `Person` have Null dereferences. In this case, Pulse would report a Null dereference on `Registry`. It could also be the case that class `Registry` is annotated with `@Nullsafe`. By default Pulse reports on `@Nullsafe` files too, see the `--pulse-nullsafe-report-npe` option (Facebook-specific: Pulse does not report on `@Nullsafe` files).

```java
@Nullsafe(Nullsafe.Mode.LOCAL)
class Person {
    Person emergencyContact;
    String address;

    @Nullable Person getEmergencyContact() {
        return this.emergencyContact;
    }
}

class Registry {
    ... // Pulse reports here
}
```


## List of Issue Types

The following issue types are reported by this checker:
- [BAD_ARG](/docs/next/all-issue-types#bad_arg)
- [BAD_ARG_LATENT](/docs/next/all-issue-types#bad_arg_latent)
- [BAD_GENERATOR](/docs/next/all-issue-types#bad_generator)
- [BAD_GENERATOR_LATENT](/docs/next/all-issue-types#bad_generator_latent)
- [BAD_KEY](/docs/next/all-issue-types#bad_key)
- [BAD_KEY_LATENT](/docs/next/all-issue-types#bad_key_latent)
- [BAD_MAP](/docs/next/all-issue-types#bad_map)
- [BAD_MAP_LATENT](/docs/next/all-issue-types#bad_map_latent)
- [BAD_RECORD](/docs/next/all-issue-types#bad_record)
- [BAD_RECORD_LATENT](/docs/next/all-issue-types#bad_record_latent)
- [BAD_RETURN](/docs/next/all-issue-types#bad_return)
- [BAD_RETURN_LATENT](/docs/next/all-issue-types#bad_return_latent)
- [COMPARED_TO_NULL_AND_DEREFERENCED](/docs/next/all-issue-types#compared_to_null_and_dereferenced)
- [CONFIG_USAGE](/docs/next/all-issue-types#config_usage)
- [CONSTANT_ADDRESS_DEREFERENCE](/docs/next/all-issue-types#constant_address_dereference)
- [CONSTANT_ADDRESS_DEREFERENCE_LATENT](/docs/next/all-issue-types#constant_address_dereference_latent)
- [DATA_FLOW_TO_SINK](/docs/next/all-issue-types#data_flow_to_sink)
- [INFINITE_LOOP](/docs/next/all-issue-types#infinite_loop)
- [INFINITE_RECURSION](/docs/next/all-issue-types#infinite_recursion)
- [MEMORY_LEAK_C](/docs/next/all-issue-types#memory_leak_c)
- [MEMORY_LEAK_CPP](/docs/next/all-issue-types#memory_leak_cpp)
- [MISSING_NULLABILITY_ANNOTATION_PULSE](/docs/next/all-issue-types#missing_nullability_annotation_pulse)
- [MUTUAL_RECURSION_CYCLE](/docs/next/all-issue-types#mutual_recursion_cycle)
- [NIL_BLOCK_CALL](/docs/next/all-issue-types#nil_block_call)
- [NIL_BLOCK_CALL_LATENT](/docs/next/all-issue-types#nil_block_call_latent)
- [NIL_INSERTION_INTO_COLLECTION](/docs/next/all-issue-types#nil_insertion_into_collection)
- [NIL_INSERTION_INTO_COLLECTION_LATENT](/docs/next/all-issue-types#nil_insertion_into_collection_latent)
- [NIL_MESSAGING_TO_NON_POD](/docs/next/all-issue-types#nil_messaging_to_non_pod)
- [NIL_MESSAGING_TO_NON_POD_LATENT](/docs/next/all-issue-types#nil_messaging_to_non_pod_latent)
- [NO_MATCHING_BRANCH_IN_TRY](/docs/next/all-issue-types#no_matching_branch_in_try)
- [NO_MATCHING_BRANCH_IN_TRY_LATENT](/docs/next/all-issue-types#no_matching_branch_in_try_latent)
- [NO_MATCHING_CASE_CLAUSE](/docs/next/all-issue-types#no_matching_case_clause)
- [NO_MATCHING_CASE_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_case_clause_latent)
- [NO_MATCHING_ELSE_CLAUSE](/docs/next/all-issue-types#no_matching_else_clause)
- [NO_MATCHING_ELSE_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_else_clause_latent)
- [NO_MATCHING_FUNCTION_CLAUSE](/docs/next/all-issue-types#no_matching_function_clause)
- [NO_MATCHING_FUNCTION_CLAUSE_LATENT](/docs/next/all-issue-types#no_matching_function_clause_latent)
- [NO_MATCH_OF_RHS](/docs/next/all-issue-types#no_match_of_rhs)
- [NO_MATCH_OF_RHS_LATENT](/docs/next/all-issue-types#no_match_of_rhs_latent)
- [NO_TRUE_BRANCH_IN_IF](/docs/next/all-issue-types#no_true_branch_in_if)
- [NO_TRUE_BRANCH_IN_IF_LATENT](/docs/next/all-issue-types#no_true_branch_in_if_latent)
- [NULLPTR_DEREFERENCE](/docs/next/all-issue-types#nullptr_dereference)
- [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS](/docs/next/all-issue-types#nullptr_dereference_in_nullsafe_class)
- [NULLPTR_DEREFERENCE_IN_NULLSAFE_CLASS_LATENT](/docs/next/all-issue-types#nullptr_dereference_in_nullsafe_class_latent)
- [NULLPTR_DEREFERENCE_LATENT](/docs/next/all-issue-types#nullptr_dereference_latent)
- [NULL_ARGUMENT](/docs/next/all-issue-types#null_argument)
- [NULL_ARGUMENT_LATENT](/docs/next/all-issue-types#null_argument_latent)
- [OPTIONAL_EMPTY_ACCESS](/docs/next/all-issue-types#optional_empty_access)
- [OPTIONAL_EMPTY_ACCESS_LATENT](/docs/next/all-issue-types#optional_empty_access_latent)
- [PULSE_ASSERTION_ERROR](/docs/next/all-issue-types#pulse_assertion_error)
- [PULSE_CANNOT_INSTANTIATE_ABSTRACT_CLASS](/docs/next/all-issue-types#pulse_cannot_instantiate_abstract_class)
- [PULSE_CONST_REFABLE](/docs/next/all-issue-types#pulse_const_refable)
- [PULSE_DICT_MISSING_KEY](/docs/next/all-issue-types#pulse_dict_missing_key)
- [PULSE_DYNAMIC_TYPE_MISMATCH](/docs/next/all-issue-types#pulse_dynamic_type_mismatch)
- [PULSE_READONLY_SHARED_PTR_PARAM](/docs/next/all-issue-types#pulse_readonly_shared_ptr_param)
- [PULSE_REFERENCE_STABILITY](/docs/next/all-issue-types#pulse_reference_stability)
- [PULSE_RESOURCE_LEAK](/docs/next/all-issue-types#pulse_resource_leak)
- [PULSE_TRANSITIVE_ACCESS](/docs/next/all-issue-types#pulse_transitive_access)
- [PULSE_UNAWAITED_AWAITABLE](/docs/next/all-issue-types#pulse_unawaited_awaitable)
- [PULSE_UNFINISHED_BUILDER](/docs/next/all-issue-types#pulse_unfinished_builder)
- [PULSE_UNINITIALIZED_CONST](/docs/next/all-issue-types#pulse_uninitialized_const)
- [PULSE_UNINITIALIZED_METHOD](/docs/next/all-issue-types#pulse_uninitialized_method)
- [PULSE_UNINITIALIZED_VALUE](/docs/next/all-issue-types#pulse_uninitialized_value)
- [PULSE_UNNECESSARY_COPY](/docs/next/all-issue-types#pulse_unnecessary_copy)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment_const)
- [PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE](/docs/next/all-issue-types#pulse_unnecessary_copy_assignment_movable)
- [PULSE_UNNECESSARY_COPY_INTERMEDIATE](/docs/next/all-issue-types#pulse_unnecessary_copy_intermediate)
- [PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_intermediate_const)
- [PULSE_UNNECESSARY_COPY_MOVABLE](/docs/next/all-issue-types#pulse_unnecessary_copy_movable)
- [PULSE_UNNECESSARY_COPY_OPTIONAL](/docs/next/all-issue-types#pulse_unnecessary_copy_optional)
- [PULSE_UNNECESSARY_COPY_OPTIONAL_CONST](/docs/next/all-issue-types#pulse_unnecessary_copy_optional_const)
- [PULSE_UNNECESSARY_COPY_RETURN](/docs/next/all-issue-types#pulse_unnecessary_copy_return)
- [PULSE_UNNECESSARY_COPY_THRIFT_ASSIGNMENT](/docs/next/all-issue-types#pulse_unnecessary_copy_thrift_assignment)
- [RETAIN_CYCLE](/docs/next/all-issue-types#retain_cycle)
- [RETAIN_CYCLE_NO_WEAK_INFO](/docs/next/all-issue-types#retain_cycle_no_weak_info)
- [SENSITIVE_DATA_FLOW](/docs/next/all-issue-types#sensitive_data_flow)
- [STACK_VARIABLE_ADDRESS_ESCAPE](/docs/next/all-issue-types#stack_variable_address_escape)
- [SWIFT_NPE](/docs/next/all-issue-types#swift_npe)
- [SWIFT_NPE_LATENT](/docs/next/all-issue-types#swift_npe_latent)
- [TAINT_ERROR](/docs/next/all-issue-types#taint_error)
- [USE_AFTER_DELETE](/docs/next/all-issue-types#use_after_delete)
- [USE_AFTER_DELETE_LATENT](/docs/next/all-issue-types#use_after_delete_latent)
- [USE_AFTER_FREE](/docs/next/all-issue-types#use_after_free)
- [USE_AFTER_FREE_LATENT](/docs/next/all-issue-types#use_after_free_latent)
- [USE_AFTER_LIFETIME](/docs/next/all-issue-types#use_after_lifetime)
- [USE_AFTER_LIFETIME_LATENT](/docs/next/all-issue-types#use_after_lifetime_latent)
- [VECTOR_INVALIDATION](/docs/next/all-issue-types#vector_invalidation)
- [VECTOR_INVALIDATION_LATENT](/docs/next/all-issue-types#vector_invalidation_latent)

---

### Checker Purity (`website/docs/checker-purity.md`)

---
title: "Purity"
description: "Detects pure (side-effect-free) functions. A different implementation of \"impurity\"."
---

Detects pure (side-effect-free) functions. A different implementation of "impurity".

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

Activate with `--purity`.

Supported languages:
- C/C++/ObjC: Experimental
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Experimental
- Python: No
- Rust: No
- Swift: No

This is an experimental inter-procedural analysis that detects pure (side-effect free) functions. For each function, purity analysis keeps track of not only the purity of the function but also some additional information such as whether the function modifies a global variable or which of the parameters are modified. It models functions with no summary/model as modifying the global state (hence impure).

If the function is pure (i.e. doesn't modify any global state or its parameters and doesn't call any unknown functions), then it reports an [`PURE_FUNCTION`](/docs/next/all-issue-types#pure_function) issue.


## Weaknesses

There are two issues with the existing purity analysis:
- In order to detect which parameters are modified, we need an alias analysis which is difficult to get right.
- Just keeping track of modified arguments doesn't suffice.

Too see the issue with the first point, consider the following simple program:

```java
void foo(Foo a){
  Foo b = a;
  b.x = 10; 
}
```

in order to determine that `foo` is impure, we need to know that the write to `b`'s field is actually changing the function parameter `a`, i.e. we need to check if `b` is aliasing `a`. This is known as alias analysis and is hard to get right in a scalable manner. When this analysis was being developed, Infer didn't have a unified alias analysis and using biabduction seemed like a too daunting task at the time. Hence, we relied on [InferBo](/docs/next/checker-bufferoverrun)'s aliasing mechanism which was easy to invoke and integrate with. However, InferBo's aliasing analysis is far from perfect and causes issues for purity.
To see the issue with the second point, consider the following program:

```java
boolean contains(Integer i, ArrayList<Integer> list){
  Iterator<Integer> listIterator = list.iterator();
  while(listIterator.hasNext()) {
    Integer el = listIterator.next();
    if (i.equals(el)){
      return true;
    }
  }
  return false;
 }
```

The existing purity analysis concludes that the above function `contains` is impure because it calls an impure function `next()` which modifies the iterator (hence it thinks it also modifies the `list`). However, notice that `contains` doesn't have an observable side-effect: `list.iterator()` returns a new object, `hasNext()` and `equals()` are pure, and `next()` only modifies the fields of the fresh object `listIterator`.  Therefore, `contains` should be considered as pure.


To alleviate this problem, we have developed an [Impurity](/docs/next/checker-impurity) analysis which uses [pulse](/docs/next/checker-pulse) which can successfully analyze this program as pure \o/


The analysis is used by:

- [Loop-hoisting](/docs/next/checker-loop-hoisting) analysis which identifies loop-invariant function calls, i.e. functions that are pure and have loop-invariant arguments. 
- [Cost](/docs/next/checker-cost) analysis which identifies control variables in the loop that affect how many times a loop is executed. In this computation, we need to prune control variables that do not affect how many times a loop is executed. In this pruning step, we need to compute loop-invariant variables (which requires the above analysis).


## List of Issue Types

The following issue types are reported by this checker:
- [PURE_FUNCTION](/docs/next/all-issue-types#pure_function)

---

### Checker Racerd (`website/docs/checker-racerd.md`)

---
title: "RacerD"
description: "Thread safety analysis."
---

Thread safety analysis.

Activate with `--racerd`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: Yes
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

RacerD finds data races in your C++/Objective C and Java code. This page gives a more in-depth
explanation of how the analysis works *for Java code*, but may be less complete than the
[Thread Safety Violation bug description page](/docs/next/all-issue-types#thread_safety_violation).
For information on C++ and Objective C, see the
[Lock Consistency violation page](/docs/next/all-issue-types#lock_consistency_violation).

To run the analysis, you can use plain `infer` (to run RacerD along with other
analyses that are run by default) or `infer --racerd-only` (to run only RacerD).

For example, the command `infer --racerd-only -- javac File.java` will run
RacerD on File.java.

## Background

RacerD statically analyzes Java code to detect potential concurrency bugs. This
analysis does not attempt to prove the absence of concurrency issues, rather, it
searches for a high-confidence class of data races. At the moment RacerD
concentrates on race conditions between methods in a class that is itself
intended to be thread safe. A race condition occurs when there are two
concurrent accesses to a class member variable that are not separated by mutual
exclusion, and at least one of the accesses is a write. Mutual exclusion can be
ensured by synchronization primitives such as locks, or by knowledge that both
accesses occur on the same thread.

## Triggering the analysis

RacerD doesn't try to check _all_ code for concurrency issues; it only looks at
code that it believes can run in a concurrent context. There are two signals
that RacerD looks for: (1) Explicitly annotating a class/method with
`@ThreadSafe` and (2) using a lock via the `synchronized` keyword. In both
cases, RacerD will look for concurrency issues in the code containing the signal
and all of its dependencies. In particular, it will report races between any
non-`private` methods of the same class that can perform conflicting accesses.
Annotating a class/interface with `@ThreadSafe` also triggers checking for all
of the subclasses of the class/implementations of the interface.

## Warnings

Let's take a look at the different types of concurrency issues that RacerD
flags. Two of the warning types are data races (`Unprotected write` and
`Read/write race`), and the third warning type encourages adding `@ThreadSafe`
annotations to interfaces to trigger additional checking.

### Unprotected write

RacerD will report an unprotected write when one or more writes can run in
parallel without synchronization. These come in two flavors: (1) a self-race (a
write-write race that occurs due to a method running in parallel with itself)
and (2) two conflicting writes to the same location. Here's an example of the
self-race flavor:

```
@ThreadSafe
public class Dinner {
  private int mTemperature;

  public void makeDinner() {
    boilWater();
  }

  private void boilWater() {
    mTemperature = 100; // unprotected write.
  }
}
```

The class `Dinner` will generate the following report on the public method
`makeDinner()`:

`There may be a Thread Safety Violation: makeDinner() indirectly writes to mTemperature outside of synchronization.`

This warning can be fixed by synchronizing the access to `mTemperature`, making
`mTemperature` `volatile`, marking `makeDinner` as `@VisibleForTesting`, or
suppressing the warning by annotating the `Dinner` class or `makeDinner` method
with `@ThreadSafe(enableChecks = false)`.

### Read/Write Race

We sometimes need to protect read accesses as well as writes. Consider the
following class with unsynchronized methods.

```
@ThreadSafe
public class Account {

  int mBalance = 0;

  public void deposit(int amount) {
    if (amount > 0) {
      mBalance += amount;
    }
  }

  public int withdraw(int amount){
    if (amount >= 0 && mBalance - amount >= 0) {
      mBalance -= amount;
      return mBalance;
    } else {
      return 0;
    }
  }
}
```

If you run the `withdraw()` method in parallel with itself or with `deposit()`
you can get unexpected results here. For instance, if the stored balance is 11
and you run `withdraw(10)` in parallel with itself you can get a negative
balance. Furthermore, if you synchronize only the write statement
`mBalance -= amount`, then you can still get this bad result. The reason is that
there is a read/write race between the boolean condition
`mBalance - amount >= 0` and the writes. RacerD will duly warn

`Read/Write race. Public method int Account.withdraw(int) reads from field Account.mBalance. Potentially races with writes in methods void Account.deposit(int), int Account.withdraw(int)`

on the line with this boolean condition.

A solution to the threading problem here is to make both methods `synchronized`
to wrap both read and write accesses, or to use an `AtomicInteger` for
`mBalance` rather than an ordinary `int`.

### Interface not thread-safe

In the following code, RacerD will report an `Interface not thread-safe` warning
on the call to `i.bar()`:

```
interface I {
  void bar();
}

@ThreadSafe
class C {
  void foo(I i) {
    i.bar(); // RacerD warns here
  }
}
```

The way to fix this warning is to add a `@ThreadSafe` annotation to the
interface `I`, which will enforce the thread-safety of each of the
implementations of `I`.

You might wonder why it's necessary to annotate `I` -- can't RacerD just look at
all the implementations of `i` at the call site for `bar`? Although this is a
fine idea in principle, it's a bad idea in practice due to a (a) separate
compilation and (b) our diff-based deployment model. In the example above, the
compiler doesn't have to know about all implementations (or indeed, any
implementations) of `I` at the time it compiles this code, so there's no
guarantee that RacerD will know about or be able to check all implementations of
`I`. That's (a). For (b), say that we check that all implementations of `I` are
thread-safe at the time this code is written, but we don't add the annotation.
If someone else comes along and adds a new implementation of `I` that is not
thread-safe, RacerD will have no way of knowing that this will cause a potential
bug in `foo`. But if `I` is annotated, RacerD will enforce that all new
implementations of `I` are thread-safe, and `foo` will remain bug-free.

## Annotations to help RacerD understand your code

Getting started with RacerD doesn't require any annotations at all -- RacerD
will look at your usage of locks and figure out what data is not guarded
consistently. But increasing the coverage and signal-to-noise ratio may require
adding `@ThreadSafe` annotations along with some of the other annotations
described below. Most of annotations described below can be used via the Maven
Central package available
[here](https://maven-repository.com/artifact/com.facebook.infer.annotation/infer-annotation).

### `@ThreadConfined`

The intuitive idea of thread-safety is that a class is impervious to concurrency
issues for all concurrent contexts, even those that have not been written yet
(it is future-proof). RacerD implements this by naively assuming that any method
can potentially be called on any thread. You may determine, however, that an
object, method, or field is only ever accessed on a single thread during program
execution. Annotating such elements with `@ThreadConfined` informs RacerD of
this restriction. Note that a thread-confined method cannot race with itself but
it can still race with other methods.

```
List mCache;

@ThreadConfined(UI)
void prepareCache() {
  // populate the cache
  mCache.add(...);
  // post cache cleanup task to run later
  mUIExecutor.execute(new Runnable() {
    @ThreadConfined(UI)
    public void run() {
      mCache.clear();
    }
  });
}
```

In this example, both `prepareCache` and `run` touch `mCache`. But there's no
possibility of a race between the two methods because both of them will run
sequentially on the UI thread. Adding a `@ThreadConfined(UI)` or `@UiThread`
annotation to these methods will stop it from warning that there is a race on
`mCache`. We could also choose to add a `@ThreadConfined` annotation to `mCache`
itself.

### `@Functional`

Not all races are bugs; a race can be benign. Consider the following:

```
@Functional Boolean askNetworkIfShouldShowFeature();

private Boolean mShouldShowFeature;

@ThreadSafe boolean shouldShowFeature() {
  if (mShouldShowFeature == null) {
    mShouldShowFeature = askNetworkIfShouldShowFeature();
  }
  return mShouldShowFeature;
}
```

This code caches the result of an expensive network call that checks whether the
current user should be shown an experimental feature. This code looks racy, and
indeed it is: if two threads execute `shouldShowFeature()` at the same time, one
may read `mShouldShowFeature` at the same time the other is writing it.

However, this is actually a _benign_ race that the programmer intentionally
allows for performance reasons. The reason this code is safe is that the
programmer knows that `askNetworkIfShouldShowFeature()` will always return the
same value in the same run of the app. Adding synchronization would remove the
race, but acquiring/releasing locks and lock contention would potentially slow
down every call to `shouldShowFeature()`. The benign race approach makes every
call after the first fast without changing the safety of the code.

RacerD will report a race on this code by default, but adding the
`@Functional annotation to askNetworkIfShouldShowFeature()` informs RacerD that
the function is always expected to return the same value. This assumption allows
RacerD to understand that this particular code is safe, though it will still
(correctly) warn if `mShouldShowFeature` is read/written elsewhere.

Be sure not to use the `@Functional` pattern for _singleton instantiation_, as
it's possible the "singleton" can be constructed more than once.

```
public class MySingleton {
  private static sInstance;

  // Not @Functional
  public MySingleton getInstance() {
    if (sInstance == null) {
      // Different threads may construct their own instances.
      sInstance == new MySingleton();
    }
    return sInstance;
  }
}
```

### `@ReturnsOwnership`

RacerD does not warn on unprotected writes to _owned_ objects. An object is
owned if it has been freshly allocated in the current thread and has not escaped
to another thread. RacerDf automatically tracks ownership in most cases, but it
needs help with `abstract` and `interface` methods that return ownership:

```
@ThreadSafe
public interface Car {
  @ReturnsOwnership abstract Car buyCar();

  void carsStuff() {
    Car myCar = new Car();
    myCar.wheels = 4; // RacerD won't warn here because it knows myCar is owned
    Car otherCar = buyCar();
    otherCar.wheels = 3; // RacerD would normally warn here, but won't because of the `@ReturnsOwnership` annotation
  }
}
```

### `@VisibleForTesting`

RacerD reports races between any two non`-private` methods of a class that may
run in a concurrent context. Sometimes, a RacerD report may be false because one
of the methods cannot actually be called from outside the current class. One fix
is making the method `private` to enforce this, but this might break unit tests
that need to call the method in order to test it. In this case, the
`@VisibleForTesting` annotation will allow RacerD to consider the method as
effectively `private` and will still allow it to be called from the unit test:

```
@VisibleForTesting void setF() {
  this.f = ...; // RacerD would normally warn here, but @VisibleForTesting will silence the warning
}

synchronized void setFWithLock() {
  setF();
}
```

Unlike the other annotations shown here, this one lives in
[Android](https://developer.android.com/reference/android/support/annotation/VisibleForTesting.html).

## Interprocedural Reasoning

An important feature of RacerD is that it finds races by analyzing not just one
file or class, but by looking at memory accesses that occur after going through
several procedure calls. It handles this even between classes and between files.

Here is a very basic example

```
@ThreadSafe
class A{

  void m1(B bb) {
    bb.meth_write();
  }
}

class B{
 Integer x;

 void meth_write() {
   x = 88;
 }

}
```

Class `B` is not annotated `@ThreadSafe` and does not have any locks, so RacerD
does not directly look for threading issues there. However, method `m1()` in
class `A` has a potential self-race, if it is run in parallel with itself and
the same argument for each call. RacerD discovers this.

```
InterProc.java:17: error: THREAD_SAFETY_VIOLATION
  Unprotected write. Non-private method `A.m1` indirectly writes to field `&this.B.x` outside of synchronization.
 Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in
 parallel with other non-private methods in the class (incuding itself).
  15.
  16.     void m1(B bb) {
  17. >     bb.meth_write();
  18.     }
  19.   }
```

RacerD does this sort of reasoning using what is known as a _compositional
inteprocedural analysis_. There, each method is analyzed independently of its
context to produce a summary of the behaviour of the procedure. In this case the
summaries for `m1()' and`meth()' include information as follows.

```
Procedure: void A.m1(B)
Accesses: { Unprotected({ 1 }) -> { Write to &bb.B.x at void B.meth_write() at line 17 } }

Procedure: void B.meth_write()
Accesses { Unprotected({ 0 }) -> { Write to &this.B.x at  at line 25 } }
```

The descriptions here are cryptic and do not include all the information in the
summaries, but the main point is that you can use RacerD to look for races in
codebases where the mutations done by threads might occur only after a chain of
procedure calls.

## <a name="context"></a> Context and Selected Related Work

Reasoning about concurrency divides into bug detection and proving absence of
bugs. RacerD is on the detection side of reasoning.

The rapid growth in the number of interleavings is problematic for tools that
attempt exhaustive exploration. With just 150 instructions for two threads, the
number 10^88 of interleavings is more that the estimated number of atoms in the
known universe.
[There has been important work which uses various techniques to attempt to reduce the number of interleavings](https://en.wikipedia.org/wiki/Partial_order_reduction)
while still in principle covering all possibilities, but scale is still a
challenge. Note that RacerD is not exhaustive: it has false negatives (missed
bugs). But in compensation it is fast, and effective (it finds bugs in
practice).

Static analysis for concurrency has attracted a lot of attention from
researchers, but difficulties with scalability and precision have meant that
previous techniques have had little industrial impact. Automatic static race
detection itself has seen significant work. The most advanced approaches,
exemplified by the [Chord](http://www.cis.upenn.edu/~mhnaik/pubs/pldi06.pdf)
tool, often use a whole-program analysis paired with a sophisticated alias
analysis, two features we have consciously avoided. Generally speaking, the
leading research tools can be more precise, but RacerD is faster and can operate
without the whole program: we have opted to go for speed in a way that enables
industrial deployment on a large, rapidly changing codebase, while trying to use
as simple techniques as possible to cover many (not all) of the patterns covered
by slower but precise research tools.

An industrial static analysis tool from
[Contemplate](http://homepages.inf.ed.ac.uk/dts/pub/avocs2015.pdf) also targets
@ThreadSafe annotations, but limits the amount of inter-procedural reasoning:
“This analysis is interprocedural, but to keep the overall analysis scalable,
only calls to private and protected methods on the same class are followed”.
RacerD does deep, cross-file and cross-class inter-procedural reasoning, and yet
still scales; the inter-class capability was one of the first requests from
Facebook engineers.
[A separate blog post looked at 100 recent data race fixes](https://code.facebook.com/posts/1537144479682247/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/)
in Infer's deployment in various bug categories, and for data races observed
that 53 of them were inter-file (and thus involving multiple classes).
[See above](#interprocedural-reasoning) for an example of RacerD's interprocedural
capabilities.

One reaction to the challenge of developing effective static race detectors has
been to ask the programmer to do more work to help the analyzer. Examples of
this approach include the
[Clang Thread Safety Analyzer](https://clang.llvm.org/docs/ThreadSafetyAnalysis.html),
the typing of [locks](https://doc.rust-lang.org/std/sync/struct.Mutex.html) in
Rust, and the use/checking of @GuardedBy annotations in
[Java](https://homes.cs.washington.edu/~mernst/pubs/locking-semantics-nfm2016.pdf)
including in
[Google's Error Prone analyzer](https://github.com/google/error-prone/blob/master/docs/bugpattern/GuardedBy.md).
When lock annotations are present they make the analyzer's life easier. It is possible to have a very effective race analysis without decreeing
that such annotations must be present. This was essential for our deployment,
since _requiring_ lock annotations would have been a show stopper for converting
many thousands of lines of code to a concurrent context. We believe that this
finding should be transportable to new type systems and language designs, as
well as to other analyses for existing languages.

Another reaction to difficulties in static race detection has been to instead
develop dynamic analyses, automatic testing tools which work by running a
program to attempt to find flaws. Google's Thread Sanitizer is a widely used and
mature tool in this area, which has been used in production to find many bugs in
C-family languages.
[The Thread Sanitizer authors explicitly call out limitations with static race analyzers](http://www.cs.columbia.edu/~junfeng/11fa-e6121/papers/thread-sanitizer.pdf)
as part of their motivation: “It seems unlikely that static detectors will work
effectively in our environment: Google’s code is large and complex enough that
it would be expensive to add the annotations required by a typical static
detector”.

We have worked to limit the annotations that RacerD needs, for reasons similar
those expressed by the Thread Sanitizer authors. And we have sought to bring the
complementary benefits of static analysis — possibility of cheaper analysis and
fast reporting, and ability to analyze code before it is placed in a context to
run — to race detection. But we are interested as well in the future in
leveraging ideas in the dynamic techniques to improve or add to our analysis for
race detection.

## Limitations

There are a number of known limitations to the design of the race detector.

- It looks for races involving syntactically identical access paths, and misses
  races due to aliasing
- It misses races that arise from a locally declared object escaping its scope
- It uses a boolean locks abstraction, and so misses races where two accesses
  are mistakenly protected by different locks
- It assumes a deep ownership model, which misses races where local objects
  refer to or contain non-owned objects.
- It avoids reasoning about weak memory and Java's volatile keyword

Most of these limitations are consistent with the design goal of reducing false
positives, even if they lead to false negatives. They also allow technical
tradeoffs which are different than if we were to favour reduction of false
negatives over false positives.

A different kind of limitation concerns the bugs searched for: Data races are
the most basic form of concurrency error, but there are many types of
concurrency issues out there that RacerD does not check for (but might in the
future). Examples include deadlock, atomicity, and check-then-act bugs (shown
below). You must look for these bugs yourself!

```
@ThreadSafe
public class SynchronizedList<T> {
  synchronized boolean isEmpty() { ... }
  synchronized T add(T item) { ... }

// Not thread safe!!!
public class ListUtil<T> {
  public void addIfEmpty(SynchronizedList<T> list, T item) {
    if (list.isEmpty()) {
      // In a race, another thread can add to the list here.
      list.add(item);
    }
  }
}
```

Finally, using `synchronized` blindly as a means to fix every unprotected write
or read is not always safe. Even with RacerD, finding, understanding, and fixing
concurrency issues is difficult. If you would like to learn more about best
practices, [Java Concurrency in Practice](http://jcip.net/) is an excellent
resource.


## List of Issue Types

The following issue types are reported by this checker:
- [GUARDEDBY_VIOLATION](/docs/next/all-issue-types#guardedby_violation)
- [INTERFACE_NOT_THREAD_SAFE](/docs/next/all-issue-types#interface_not_thread_safe)
- [LOCK_CONSISTENCY_VIOLATION](/docs/next/all-issue-types#lock_consistency_violation)
- [THREAD_SAFETY_VIOLATION](/docs/next/all-issue-types#thread_safety_violation)

---

### Checker Resource Leak Lab (`website/docs/checker-resource-leak-lab.md`)

---
title: "Resource Leak Lab Exercise"
description: "Toy checker for the \"resource leak\" write-your-own-checker exercise."
---

Toy checker for the "resource leak" write-your-own-checker exercise.

Activate with `--resource-leak-lab`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: Yes
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

This toy checker does nothing by default. Hack on it to make it report resource leaks! See the [lab instructions](https://github.com/facebook/infer/blob/main/infer/src/labs/README.md).

## List of Issue Types

The following issue types are reported by this checker:
- [LAB_RESOURCE_LEAK](/docs/next/all-issue-types#lab_resource_leak)

---

### Checker Scope Leakage (`website/docs/checker-scope-leakage.md`)

---
title: "Scope Leakage"
description: "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)."
---

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).

Activate with `--scope-leakage`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [SCOPE_LEAKAGE](/docs/next/all-issue-types#scope_leakage)

---

### Checker Self In Block (`website/docs/checker-self-in-block.md`)

---
title: "Self in Block"
description: "An Objective-C-specific analysis to detect when a block captures `self`."
---

An Objective-C-specific analysis to detect when a block captures `self`.

Activate with `--self-in-block`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [CAPTURED_STRONG_SELF](/docs/next/all-issue-types#captured_strong_self)
- [CXX_REF_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#cxx_ref_captured_in_block)
- [CXX_STRING_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#cxx_string_captured_in_block)
- [MIXED_SELF_WEAKSELF](/docs/next/all-issue-types#mixed_self_weakself)
- [MULTIPLE_WEAKSELF](/docs/next/all-issue-types#multiple_weakself)
- [NSSTRING_INTERNAL_PTR_CAPTURED_IN_BLOCK](/docs/next/all-issue-types#nsstring_internal_ptr_captured_in_block)
- [SELF_IN_BLOCK_PASSED_TO_INIT](/docs/next/all-issue-types#self_in_block_passed_to_init)
- [STRONG_SELF_NOT_CHECKED](/docs/next/all-issue-types#strong_self_not_checked)
- [WEAK_SELF_IN_NO_ESCAPE_BLOCK](/docs/next/all-issue-types#weak_self_in_no_escape_block)

---

### Checker Sil Validation (`website/docs/checker-sil-validation.md`)

---
title: "SIL validation"
description: "This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL."
---

This checker validates that all SIL instructions in all procedure bodies conform to a (front-end specific) subset of SIL.

Activate with `--sil-validation`.

Supported languages:
- C/C++/ObjC: No
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [INVALID_SIL](/docs/next/all-issue-types#invalid_sil)

---

### Checker Siof (`website/docs/checker-siof.md`)

---
title: "Static Initialization Order Fiasco"
description: "Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors."
---

Catches Static Initialization Order Fiascos in C++, that can lead to subtle, compiler-version-dependent errors.

**\*\*\*DEPRECATED\*\*\*** This checker is deprecated and will be removed in a future release.

Activate with `--siof`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [STATIC_INITIALIZATION_ORDER_FIASCO](/docs/next/all-issue-types#static_initialization_order_fiasco)

---

### Checker Starvation (`website/docs/checker-starvation.md`)

---
title: "Starvation"
description: "Detect various kinds of situations when no progress is being made because of concurrency errors."
---

Detect various kinds of situations when no progress is being made because of concurrency errors.

Activate with `--starvation`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: Yes
- Python: No
- Rust: No
- Swift: No

Detect several kinds of "starvation" problems:
- deadlocks
- violations of `@Lockless` annotations
- violations of [Android's "strict mode"](https://developer.android.com/reference/android/os/StrictMode)
- doing expensive operations on the Android UI thread


## List of Issue Types

The following issue types are reported by this checker:
- [ARBITRARY_CODE_EXECUTION_UNDER_LOCK](/docs/next/all-issue-types#arbitrary_code_execution_under_lock)
- [DEADLOCK](/docs/next/all-issue-types#deadlock)
- [IPC_ON_UI_THREAD](/docs/next/all-issue-types#ipc_on_ui_thread)
- [LOCKLESS_VIOLATION](/docs/next/all-issue-types#lockless_violation)
- [LOCK_ON_UI_THREAD](/docs/next/all-issue-types#lock_on_ui_thread)
- [REGEX_OP_ON_UI_THREAD](/docs/next/all-issue-types#regex_op_on_ui_thread)
- [STARVATION](/docs/next/all-issue-types#starvation)
- [STRICT_MODE_VIOLATION](/docs/next/all-issue-types#strict_mode_violation)

---

### Checker Static Constructor Stall Checker (`website/docs/checker-static-constructor-stall-checker.md`)

---
title: "Static Constructor Stall Checker"
description: "Detect if dispatch_once is called from a static constructor."
---

Detect if dispatch_once is called from a static constructor.

Activate with `--static-constructor-stall-checker`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: No



## List of Issue Types

The following issue types are reported by this checker:
- [STATIC_CONSTRUCTOR_STALL](/docs/next/all-issue-types#static_constructor_stall)

---

### Checker Swift Objc Nullability (`website/docs/checker-swift-objc-nullability.md`)

---
title: "Swift/Obj-C Nullability"
description: "Detects missing nullability annotations in Objective-C methods called from Swift, which can lead to runtime crashes via Implicitly Unwrapped Optionals."
---

Detects missing nullability annotations in Objective-C methods called from Swift, which can lead to runtime crashes via Implicitly Unwrapped Optionals.

Activate with `--swift-objc-nullability`.

Supported languages:
- C/C++/ObjC: Yes
- C#/.Net: No
- Erlang: No
- Hack: No
- Java: No
- Python: No
- Rust: No
- Swift: Yes

# Swift/Obj-C Nullability

Reports calls from Swift code to Objective-C methods whose declaration
has no `_Nullable` or `_Nonnull` annotation on a pointer return type.
The Swift clang importer treats such results as Implicitly Unwrapped
Optionals (`T!`), so any subsequent use that assumes the result is
non-nil traps at runtime if the method ever returns `nil`. The checker
raises the trap-prone call sites at compile time so the team that owns
the Objective-C declaration can decide the contract explicitly.

The recommended fix lives on the
[`MISSING_NULLABILITY_ANNOTATION`](/docs/next/all-issue-types#missing_nullability_annotation)
issue page: annotate the Objective-C declaration with `_Nullable` or
`_Nonnull`, or cast the result with `as?` at the Swift call site.

## What is deliberately ignored

To keep reports actionable, the checker does not report at call sites
where the developer cannot or should not be asked to act:

- Callees declared in headers under an Apple SDK or under a prebuilt
  framework's public-header directory: the consumer cannot edit those
  declarations.
- Calls whose return value is null-checked by the Swift caller
  before use, e.g. `if let s = api.foo() { ... }`.
- Calls whose return value is explicitly cast through an `as?`
  Optional cast, e.g. `if let s = api.foo() as? NSString { ... }`.

A bare force-unwrap (`api.foo()!`) is intentionally NOT treated as a
fix — it makes the trap explicit but does not eliminate it.


## List of Issue Types

The following issue types are reported by this checker:
- [MISSING_NULLABILITY_ANNOTATION](/docs/next/all-issue-types#missing_nullability_annotation)

---

### Checker Topl (`website/docs/checker-topl.md`)

---
title: "Topl"
description: "Detect errors based on user-provided state machines describing temporal properties over multiple objects."
---

Detect errors based on user-provided state machines describing temporal properties over multiple objects.

Activate with `--topl`.

Supported languages:
- C/C++/ObjC: Experimental
- C#/.Net: No
- Erlang: Experimental
- Hack: No
- Java: Experimental
- Python: No
- Rust: No
- Swift: No

# Topl

## What is it?

Topl is an analysis framework, built on top of Infer, for statically finding violations of temporal properties. Many analyses can be encoded as temporal properties supported by Topl, such as taint analysis. As a simple example, suppose that we don't want a value returned by method `source()` to be sent as an argument to a method `sink()`. This can be specified as follows:

```
property Taint
  prefix "Main"
  start -> start: *
  start -> tracking: source(Ret) => x := Ret
  tracking -> error: sink(Arg, VoidRet) when x == Arg
```

This specifies an automaton called `Taint` that has three states (`start`, `tracking`, `error`). Two of those states (`start` and `error`) have special meaning; other states (`tracking`) can have any names. The first transition (`start → tracking`) is taken when a method called `source()` is called, and its return value is stored in a register called `x`; the second transition (`tracking → error`) is taken when a method called `sink()` is called, but only if its argument equals what was previously saved in register `x`.
This property is violated in the following Java code:

```
public class Main {
  static void f() { g(tito(source())); }
  static void g(Object x) { h(x); }
  static void h(Object x) { sink(x); }
  static Object tito(Object x) { return x; }
  static Object source() { return "dirty"; }
  static void sink(Object x) {}
}
```

Note that `source()` and `sink()` are not called from the same method, and that the “dirty” object is passed around a few times before finally reaching the sink. Assuming that the property is in a file `taint.topl` and the Java code in a file `Main.java`, you can invoke Infer with the following command:

```
infer --topl --topl-properties taint.topl  -- javac Main.java
```

It will display the following error:

```
Main.java:2: error: Topl Error
  property Taint reaches state error.
  1.   public class Main {
  2. >   static void f() { g(tito(source())); }
  3.     static void g(Object x) { h(x); }
  4.     static void h(Object x) { sink(x); }
```

To get a full trace, use the command

```
infer explore
```

## Specifying Properties

A property is a nondeterministic automaton that can remember values in registers. An execution that drives the automaton from the start state to the error state will make Infer report an issue, and the trace that it produces will indicate which parts of the program drive which transitions of the automaton.

The general form of a property is the following:

```
property Name
  message "Optional error message" // This line can be missing
  prefix "Prefix" // There can be zero, one, or more prefix declarations
  sourceState -> targetState: Pattern(Arg1,...,ArgN,Ret) when Condition => Action
```

The property name and the optional error message are used for reporting issues. The prefix declarations are used to simplify Patterns. The core of the property is the list of transitions.

Each transition has a source state and a target state. The special transition label * means that the transition is always taken. Typically, there is a transition

```
  start -> start: *
```

meaning that the property can start anywhere, not just at the beginning of a method.

Otherwise, the label on a transition contains:

* a *Pattern*, which indicates what kind of instruction in the program drives this transition;
* a list of transition variable bindings (above named Arg1, ..., but any identifier starting with uppercase letters works);
* possibly a boolean Condition, which can refer to transition variables, registers and fields;
* possibly and Action, which is a list sequence of assignments of the form *register* := *TransitionVariable* (registers do not need to be declared, and any identifier starting with a lowercase letter works).

There are two types of patterns:

* a regex that matches method names
    * if the regex uses non-letters (such as dots) it must be within double-quotes; otherwise, double quotes are optional
    * the prefix declarations are used to add potential prefixes to the regex. The combine regex is essentially “(prefix_regex_a | prefix_regex_b) transition_pattern_regex“
    * for a method with n arguments, there must be n+1 transition variables to get a match. The first n transition variables get bound to the argument values, and the last transition variable gets bound to the return value. *This is true even for the case in which the return type is void*.
* the special keyword **#ArrayWrite**. In that case, there should be two transition variables like “(Array, Index)” — Array gets bound to the array object, and Index gets bound to the index at which the write happens.

The condition supports the following kinds of expressions:
* Referring to identifiers: transition variables and registers
* Field access over objects in the form `Identifier:Type.FieldName`, e.g. `X:MyClass.myField` (this is currently only supported for Erlang)
* Integer literals
* The usual comparison operators (`==`, `!=`, `<`, `>`, `>=`, `<=`) and conjunctions (`&&`)
* Reachability predicates of the form `Ident1 ~~> Ident2` meaning that `Ident2` can be reached via pointers/fields from `Ident1` in the heap

For several examples, see https://github.com/facebook/infer/tree/main/infer/tests/codetoanalyze/java/topl

## Limitations

* By design, some problems may be missed. Topl is built on Pulse, which attempts to minimize false positives, at the cost of sometimes having false negatives.
* Analysis time increases exponentially with the number of registers used in properties.
    * In theory, there should be no significant slowdown if registers belong to different properties, but the implementation is not yet optimized.
    * If there are many registers within the same property, then the slowdown is unavoidable (without some significant breakthrough). However, the maximum number of registers we ever used for one practical property was 3.


## List of Issue Types

The following issue types are reported by this checker:
- [TOPL_ERROR](/docs/next/all-issue-types#topl_error)
- [TOPL_ERROR_LATENT](/docs/next/all-issue-types#topl_error_latent)

---

### Man Infer Analyze (`website/docs/man-infer-analyze.md`)

---
id: man-infer-analyze
title: infer analyze
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-analyze.1.html" />

---

### Man Infer Capture (`website/docs/man-infer-capture.md`)

---
id: man-infer-capture
title: infer capture
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-capture.1.html" />

---

### Man Infer Compile (`website/docs/man-infer-compile.md`)

---
id: man-infer-compile
title: infer compile
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-compile.1.html" />

---

### Man Infer Debug (`website/docs/man-infer-debug.md`)

---
id: man-infer-debug
title: infer debug
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-debug.1.html" />

---

### Man Infer Explore (`website/docs/man-infer-explore.md`)

---
id: man-infer-explore
title: infer explore
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-explore.1.html" />

---

### Man Infer Help (`website/docs/man-infer-help.md`)

---
id: man-infer-help
title: infer help
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-help.1.html" />

---

### Man Infer Report (`website/docs/man-infer-report.md`)

---
id: man-infer-report
title: infer report
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-report.1.html" />

---

### Man Infer Reportdiff (`website/docs/man-infer-reportdiff.md`)

---
id: man-infer-reportdiff
title: infer reportdiff
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-reportdiff.1.html" />

---

### Man Infer Run (`website/docs/man-infer-run.md`)

---
id: man-infer-run
title: infer run
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer-run.1.html" />

---

### Man Infer (`website/docs/man-infer.md`)

---
id: man-infer
title: infer
---

import HtmlWrap from "@site/src/components/HtmlWrap";

<HtmlWrap url="/man/next/infer.1.html" />

---

### Support (`website/docs/support.md`)

---
title: Infer | Need help?
id: support
---

## Need help?

Do not hesitate to ask questions using the following channels, or to submit pull
request!

### GitHub issues

The [GitHub issues](https://github.com/facebook/Infer/issues) page is a good
place to ask questions, find answers, and report issues.

Please include as many details as possible when submitting a GitHub issue. If
you are able to run Infer, please include the contents of
`infer-out/toplevel.log` in your report. If not, please include at least your
operating system and the version of Infer that you are using.

### Updates

Keep up to date with the latest Infer news on our
[Facebook page](https://www.facebook.com/inferstaticanalyzer/) and our
[Twitter account](https://twitter.com/fbinfer).

### IRC

Our IRC channel is [`#infer`](irc://irc.libera.chat/infer) on [Libera Chat](https://libera.chat/).

## Troubleshooting

### Infer cannot analyze my CocoaPods project

In the presence of CocoaPods, you should use xcworkspace and not xcodeproj in
the compilation command that you supply to Infer. Here is an example you can
adapt to your project:

```bash
infer run -- xcodebuild -workspace HelloWorld.xcworkspace -scheme HelloWorld
```

### `infer [options] -- <build command>` fails during a linking step

The linker will sometimes not work if files have been compiled using a different
compiler, such as the one Infer uses [under the hood](/docs/next/infer-workflow) to
analyze your files.

A workaround consists in setting the `LD` environment variable to a dummy
linker, for instance:

```
LD=/bin/true infer [options] -- <build command>
```

### I get a compilation error involving PCH files when running Infer

For instance,
`error: PCH file uses an older PCH format that is no longer supported`.

This is a [known issue](https://github.com/facebook/infer/issues/96).

Please run Infer with the following environment variable setting:

```bash
GCC_PRECOMPILE_PREFIX_HEADER=NO
```

### Infer reports a "Too many open files" error

The maximum number of files a program can simultaneously hold open is a bit low
on MacOs. You can increase the limit by running these commands for example:

```bash
sysctl -w kern.maxfiles=20480
sysctl -w kern.maxfilesperproc=22480
ulimit -S -n 2048
```

Note that the settings will be reset at the next reboot.

See also [this GitHub issue](https://github.com/facebook/infer/issues/22).

### I get a lint error when running Infer with gradle

You need to manually disable linters to run Infer. For instance

```bash
infer run -- gradle build -x lint
```

See also [this GitHub issue](https://github.com/facebook/infer/issues/58).

### Running `infer [options] -- <build command>` fails with some other error

Please make sure that:

- `<build command>` runs successfully on its own.
- `infer` is in your `$PATH` (try `which infer`, it should show where `infer` is
  located)

### I get errors compiling Infer

Make sure the dependencies are up to date. They may change as we
update Infer itself. See the [installation
document](https://github.com/facebook/infer/blob/main/INSTALL.md)
for an up-to-date list of dependencies and how to get them.

### My problem is not listed here

Do not hesitate to [contact us](#need-help).

## FAQ

Here are some frequently asked questions. More to come.

### How do I suppress Infer warnings on a class or method?

In Java code, you can do this *for some error types* by annotating
your class or method with `@SuppressLint("<ISSUE_TYPE>")`, for example
`@SuppressLint("NULL_DEREFERENCE")`. However, not all checkers honor
this annotation.

### Is Infer supported for Windows?

Infer is not supported on Windows at the moment. You may try installing Infer on
a Linux virtual machine if your project can be compiled on Linux.

### How does Infer compare to the Clang Static Analyzer?

Infer and Clang Static Analyzer (CSA) will typically find different
kinds of issues on the same project. One thing that sets Infer apart
from other static analysis tools is its ability to reason and find
issues across multiple files. But CSA will find many kinds of issues
that Infer doesn't find: we send big respect to CSA! Really, these
tools complement one another and it makes sense to use both.

### How does Infer compare to Android linters and Findbugs?

Infer finds deeper infer-procedural bugs sometimes spanning multiple files.
Linters, in contrast, typically implement simple syntactic checks that are local
within one procedure. But they are valuable and Infer doesn't try to duplicate
what they are good at. At Facebook we run both Infer and a collection of Android
linters. Findbugs can be useful too; it is more akin to linters.

---

### Versions (`website/docs/versions.md`)

---
id: versions
title: Documentation Versions
---

Browse the documentation for different versions:
- [latest released version (1.3.0)](/docs/getting-started)
- [previous version (1.1.0)](/docs/1.1.0/getting-started)
- [next version](/docs/next/getting-started)

---

### Dependencies Charon Docs Limitations (`dependencies/charon/docs/limitations.md`)

# Current limitations of Charon

Charon is alpha software. In particular, it is currently poorly documented, doesn't support all the
Rust features we'd like, and has several breaking changes planned in the near future.

## Planned breaking changes

- https://github.com/AeneasVerif/charon/issues/287
- https://github.com/AeneasVerif/charon/issues/194
- https://github.com/AeneasVerif/charon/issues/582
- Some potential rework of how we handle builtins like `SliceIndexMut`
- Name matcher behavior likely to change in subtle ways
  (https://github.com/AeneasVerif/charon/issues/319).

## Known unsoundnesses

- https://github.com/AeneasVerif/charon/issues/583
- https://github.com/AeneasVerif/charon/issues/584

## Unsupported Rust features

Tracked here: https://github.com/AeneasVerif/charon/issues/142

## Missing information in the translated output

- Bodies of functions in foreign crates often cause errors (https://github.com/AeneasVerif/charon/issues/543);
- Bodies of std functions (https://github.com/AeneasVerif/charon/issues/545);
- Drops (https://github.com/AeneasVerif/charon/issues/152);
- Layout information (https://github.com/AeneasVerif/charon/issues/581);
- Lifetime information inside function bodies (not planned).

---

### Dependencies Charon Docs Transformations (`dependencies/charon/docs/transformations.md`)

# Charon transformations

Charon has options to make the generated code easier to use. Some are currently not optional but
could be made so on request.

## Control-flow reconstruction

The MIR we get from rustc is a control-flow graph (CFG), where control-flow happens with gotos that
can jump arbitrarily around the code.

Charon by default transforms this CFG into structured control-flow, i.e. with nested
`match`/`if`/`loop` constructs.

To turn this off, pass `--ullbc` to `charon` (ULLBC stands for Unstructured LLBC).

## `--hide-marker-traits`

This option removes mentions of the following built-in traits from the output crate:
- `core::marker::Sized`
- `core::marker::Tuple`
- `core::marker::Send`
- `core::marker::Sync`
- `core::marker::Unpin`

This is a convenience option, meant to reduce noise for Charon consumers that output user-readable
things.

Note that for historical reasons Charon removes mentions of the `Allocator` trait regardless of this
setting. This should eventually be changed, open an issue if you have a need for it.

Note that today this is implemented by calling `IndexMap::remove` to remove the entry in the
`trait_clauses`/`trait_refs` vectors. This abuses the confusion between newtype-indexed vectors and
newtype-indexed maps we have in Charon, which can cause annoying footguns. See
https://github.com/AeneasVerif/charon/issues/490.

## `--remove-associated-types`

This option takes a pattern, and transforms the associated types of all the traits that match the
pattern. This transforms code like:
```rust
trait Iterator {
  type Item;
  fn next(&mut self) -> Option<Self::Item>;
}
fn use_iterator<I: Iterator>(it: I) { ... }
```
into:
```rust
trait Iterator<Item> {
  fn next(&mut self) -> Option<Item>;
}
fn use_iterator<I: Iterator<Clause0Item>, Clause0Item>(it: I) { ... }
```

This transformation has limitations:
- GATs cannot be transformed this way;
- Some recursive traits cannot be transformed this way, e.g.:
```rust
trait Bar {
    type BarTy;
}
trait Foo {
    type FooTy: Foo + Bar;
}
// becomes:
trait Bar<BarTy> {}
trait Foo {
    type FooTy: Foo + Bar<Self::FooTy_BarTy>;
    // We need to supply an argument to `Bar` but we can't add a type parameter, so we add a
    // new associated type.
    type FooTy_BarTy;
}
```
- We're currently missing assoc type information to transform `dyn Trait` (https://github.com/AeneasVerif/charon/issues/123).
- We currently don't track bound lifetimes in quantified clauses properly (https://github.com/AeneasVerif/charon/issues/534).
- Type aliases don't have the correct clauses in scope (https://github.com/AeneasVerif/charon/issues/531).
- We don't take into account unicity of trait implementations. This means we won't detect type
  equalities due to the same trait predicate appearing twice, or a trait predicate coinciding with
  an existing trait impl. See the `dictionary_passing_style_woes.rs` test file for an example.

## Make implied bounds explicit

WIP: https://github.com/AeneasVerif/charon/issues/585

---

### Dependencies Charon Docs Usage (`dependencies/charon/docs/usage.md`)

# Usage

To run Charon, you should run the Charon binary from *within* the crate that you
want to compile, as if you wanted to build the crate with `cargo build`. The
Charon executable is located at `bin/charon`.

Charon will build the crate and its dependencies, then extract the AST. Charon
provides various options and flags to tweak its behaviour: you can display a
detailed documentation with `--help`.
In particular, you can pretty-print the translated crate with both `--print-ullbc` and `--print-llbc`, depending on the Charon intermediate representation you wish to use.

If there is a `Charon.toml` file at the root of your project, `charon` will also take options from it.
The file supports the same options at the cli interface, except for the options that relate to
input/output like `--print-llbc`. Example `Charon.toml`:
```toml
[charon]
extract_opaque_bodies = true
[rustc]
flags = ["--cfg", "abc"]
```

**Remark**: because Charon is compiled with Rust nightly (this is a requirement to implement a rustc
driver), it will build your crate with Rust nightly. You can find the nightly version pinned for
Charon in [`rust-toolchain.template`](rust-toolchain.template).

## Names

Each item (function, trait decl, type decl etc) in Charon has a unique name, that looks like a Rust
path (e.g., `std::boxed::Box`). This name can be used to uniquely identify items using patterns.

These patterns are used most notably for the `--include`/`--exclude` cli options, and made available
in Rust and OCaml with NameMatcher. Caveat: the Rust and OCaml name matchers differ in input syntax
and behavior; this is tracked in https://github.com/AeneasVerif/charon/issues/319.

TODO: explain syntax and behavior.

Note: for well-known built-in items, you can often use `ItemMeta.lang_item` instead; it contains an
identifier meant for this purpose, documented
[here](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir/lang_items/enum.LangItem.html).

## CLI options

TODO: explain the main options, and LLBC vs ULLBC

In short: LLBC is the name we give to the output of Charon. It stands for Low-Level Borrow Calculus
and is the name used in the formalisations of the Aeneas project. Charon was initially created as
part of the Aeneas project, and therefore inherits that name. ULLBC means Unstructured LLBC, i.e.,
LLBC without the control-flow reconstruction.

ULLBC is a slightly simplified MIR, where we try to remove as much redundancies
as possible. For instance, we drastically simplify the representation of constants coming
from the Rust compiler.

LLBC is ULLBC where we restructured the control-flow with loops, `if
... then ... else ...`, etc. instead of gotos. Consequently, we merge MIR
statements and terminators into a single LLBC statement type.

**Remark**: most of the transformations which transform the MIR to ULLBC then LLBC are implemented
by means of micro-passes. Depending on the need, we could make them optional and control them with
flags. If you want to know more about the details, see `transformation_passes` in
`src/bin/charon-driver/driver.rs`, which applies the micro-passes one after the other.

---

### Dependencies Charon Docs What Charon Does For You (`dependencies/charon/docs/what_charon_does_for_you.md`)

# What Charon Does For You

The purpose of Charon is to centralize the efforts of extracting information from rustc internals
and turning them into a uniform and usable shape. Here are some things that Charon does once so you
don't have to do it yourself:

TODO: explain each item

- Trait resolution (explicitly track how each trait bound was proven to hold);
- Reconstruct expressions from all the various constant representations;
- Hide the distinction between early- and late-bound lifetime variables;
- Make non-overriden default methods in impl blocks appear as normal methods;
- Handle trait method implementations that have a more general signature than as declared in the trait (WIP: https://github.com/AeneasVerif/charon/issues/513);
- Represent closures as normal structs that implement the `Fn*` traits;
- Represent VTables as normal structs stored in statics (WIP: see https://github.com/AeneasVerif/charon/issues/123);
- Many useful post-processing transformations to make the output more usable; see [the dedicated file](./transformations.md).

---

### Dependencies Charon Docs What Charon Translates (`dependencies/charon/docs/what_charon_translates.md`)

# Charon item selection

## Items and opacity

An **item** is a module, function, type decl, static, const, trait decl, or trait impl. A crate is considered a module.

Each item has an **opacity** level[^1]:

1. **Transparent** — the item is fully translated.
2. **Foreign** — the default for items outside the current crate. Translation depends on normal Rust visibility: for types, translate fully if it's a struct with all-public fields or an enum; for other items this is equivalent to Opaque.
3. **Opaque** — only the name and signature are translated, not the contents. For functions and globals, the body is not translated. For types (structs, enums, unions), the fields/variants are not translated. For traits and trait impls, the default method is  only translated if it is used somewhere else. For modules, the contents are not explored (but items referenced from elsewhere are still translated).
4. **Invisible** — nothing is translated for this item. The corresponding map will not have an entry for the item ID. Useful when even the signature causes errors.

## Selection process

Charon starts from a set of **entry points** and explores outward using a work-queue:

1. The entry point items are enqueued for processing.
2. Each item is processed according to its opacity:
   - **Transparent module**: enqueue all items directly inside it.
   - **Non-transparent module**: do nothing (contents are not explored).
   - **Transparent non-module item**: translate it fully (including body).
   - **Foreign or opaque non-module item**: translate only the signature.
   - **Invisible item**: do nothing.
3. Whenever processing an item encounters a reference to a new item, that new item is enqueued for processing.

This is a dependency-driven algorithm that pulls in items as they are needed. With the default settings, the entry point is the current crate (a module), which is transparent, so all its direct items are enqueued. Those items reference foreign items from dependencies, which get enqueued as foreign (signatures only). The result: the whole current crate is translated, plus the signatures of all foreign items it references.

## How opacity is determined

Each item's opacity is calculated from its name by matching against a list of patterns. The patterns come from two sources: CLI flags and source annotations.

### Source annotations

The source-level attributes `#[charon::opaque]` and `#[charon::exclude]` set the opacity of individual items. They **can only make items more opaque, never less**[^2].

When both a source annotation and a CLI pattern apply, the more opaque of the two wins (`Transparent < Foreign < Opaque < Invisible`). This means `--include` **cannot** override a `#[charon::opaque]` annotation.

### CLI flags

- **`--start-from <PATTERN>`** — Entry points for translation. Can be specified multiple times. Default: `crate` (the entire current crate).
- **`--start-from-attribute[=<ATTR>]`** — Use items annotated with a given attribute as entry points. Default attribute if none specified: `verify::start_from`.
- **`--start-from-pub`** — Use all `pub` items from the current crate as entry points
- **`--include <PATTERN>`** — Set matched items to **transparent**.
- **`--opaque <PATTERN>`** — Set matched items to **opaque**.
- **`--exclude <PATTERN>`** — Set matched items to **invisible**.
- **`--extract-opaque-bodies`** — Alias for `--include *`. Makes all items transparent.
- **`--translate-all-methods`** — Include provided trait methods even if unused. Equivalent to making all trait declarations transparent.  

### Pattern list

Charon builds an ordered list of `(pattern, opacity)` pairs from the CLI flags[^3]:

```
_              → Foreign      (default: everything starts as foreign)
crate          → Transparent  (current crate is always transparent)
<--include>    → Transparent  (user whitelist)
<--opaque>     → Opaque       (user blacklist)
<--exclude>    → Invisible    (user exclusion)
```

The default is equivalent to `--opaque '*' --include crate`: everything is foreign except items in the current crate which are transparent.

### Pattern syntax

Patterns use a name-matcher syntax (`charon/src/name_matcher/`). Examples:

- `crate::module::item` — matches this item and all its subitems
- `crate::module::item::_` — matches only the subitems (not the item itself)
- `core::convert::{impl core::convert::Into<_> for _}` — a specific trait impl
- `_` or `*` — glob, matches any single path segment
- `{impl core::convert::Into<_> for _}` works without the core::convert prefix, in this case we do a global search for impls.

Patterns are **prefix matches**: `crate::foo` matches `crate::foo`, `crate::foo::bar`, `crate::foo::bar::baz`, etc.[^4]

Currently matching on inherent impl blocks isn't supported, writing `crate::module::_::method` is the standard workaround.

### Precedence

When multiple patterns match the same item, the **most precise pattern wins**[^5]:

1. **Longer patterns** beat shorter ones.
2. Among equal-length patterns, a **non-glob final element** beats a glob.

Example with `--opaque crate::module --include crate::module::_`:

| Item                  | Matching patterns                                  | Most precise                  | Result      |
|-----------------------|----------------------------------------------------|-------------------------------|-------------|
| `crate::module`       | `_`, `crate`, `crate::module`                      | `crate::module` (length 2)    | Opaque      |
| `crate::module::foo`  | `_`, `crate`, `crate::module`, `crate::module::_`  | `crate::module::_` (length 3) | Transparent |

Note: pattern matching currently has limitations — e.g. it parses `u64` as a path instead of the built-in type, and it is not possible to filter a trait impl (only its methods)[^6].

[^1]: `charon/src/ast/meta.rs:191`
[^2]: `charon/src/bin/charon-driver/translate/translate_meta.rs:776-785`
[^3]: `charon/src/options.rs:534-570`
[^4]: `charon/src/name_matcher/mod.rs:51-125`
[^5]: `charon/src/name_matcher/mod.rs:189-221`
[^6]: `charon/src/options.rs:112`

---

--- METRICS ---
- Files Extracted: 57
- Estimated Token Budget: ~69153 tokens
- Canonical Reference: https://codewiki.google/github.com/facebook/infer