Infer

https://fbinfer.com/docs
Admin
Infer is a static analysis tool that detects bugs in Java, C/C++, and Objective-C code before it...
Tokens:58,448
Snippets:1,015
Trust Score:10
Update:4 months ago
Show doc for...
Tokens:
Raw
### Example .inferconfig File

Source: https://fbinfer.com/docs/man-infer

An example of an .inferconfig file, which stores infer options in JSON format. Fields correspond to long-form options without the leading '--'.

```json
{
  "cxx": false,
  "infer-block-list-files-containing": ["@gen","/* no infer */"]
}
```

--------------------------------

### Android Hello World Example

Source: https://fbinfer.com/docs/hello-world

An example of analyzing an Android application using Infer. This snippet shows the command to run Infer on a Gradle-based Android project and the types of errors it can report, such as NULL_DEREFERENCE and RESOURCE_LEAK.

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

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

--------------------------------

### Inferbo Square Root FP Example

Source: https://fbinfer.com/docs/all-issue-types

Example of T cost due to Inferbo's interval analysis limitation with affine expressions.

```Java
// Expected: square root(x), got T
void square_root_FP(int x) {
 int i = 0;
 while (i * i < x) {
   i++;
 }
}

```

--------------------------------

### Objective-C Hello World Example

Source: https://fbinfer.com/docs/hello-world

A basic Objective-C example demonstrating a NULL_DEREFERENCE error. Infer can detect dereferencing a nil object. The fix involves using the property getter.

```objective-c
// Hello.m  
#import <Foundation/Foundation.h>  
@interface Hello: NSObject  
@property NSString* s;  
@end  
@implementation Hello  
NSString* m() {  
    Hello* hello = nil;  
    return hello->_s;  
}
@end
```

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

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

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

--------------------------------

### Unreachable Code Example

Source: https://fbinfer.com/docs/all-issue-types

Provides examples of code that is unreachable, either due to an explicit exit or an infeasible path that is pruned by the analysis.

```C++
void exit_unreachable() {
  exit(0); // modeled as unreachable
}

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

--------------------------------

### Java Hello World Example

Source: https://fbinfer.com/docs/hello-world

A simple Java class with a potential NULL_DEREFERENCE error. Run Infer to detect the bug and then modify the code to include null checks.

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

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

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

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

--------------------------------

### Litho Component Usage (Optional Prop Missing)

Source: https://fbinfer.com/docs/all-issue-types

Example of building a Litho component when an optional prop is missing, which is acceptable.

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

```

--------------------------------

### Inferbo Alloc Is Zero Example

Source: https://fbinfer.com/docs/all-issue-types

malloc is called with a zero size. Fix the size argument.

```C
int n = 3 - 3; malloc(n);

```

--------------------------------

### Litho Component Usage (Required Prop Missing)

Source: https://fbinfer.com/docs/all-issue-types

Example of building a Litho component when a required prop is missing, which will result in an error.

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

```

--------------------------------

### Force Infer Integration for Unsupported Build Systems

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

If Infer doesn't recognize your build system, you can force an integration, for example, treating an unknown command as 'make'.

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

infer run --force-integration make -- foo  

```

--------------------------------

### Linear Execution Time Example

Source: https://fbinfer.com/docs/all-issue-types

A simple Java function that calculates the sum of elements in a list, demonstrating linear execution time complexity.

```Java
int sum_linear(ArrayList<Integer> list){
 int sum = 0;
 for (Integer el: list){
   sum += el;
 }
 return sum;
}
```

--------------------------------

### Erlang NO_MATCHING_FUNCTION_CLAUSE Example

Source: https://fbinfer.com/docs/all-issue-types

Illustrates a NO_MATCHING_FUNCTION_CLAUSE error in Erlang. This error is reported when none of the function clauses match the arguments of a call.

```erlang
tail([_|Xs]) -> Xs.  

```

--------------------------------

### Inferbo Call Top Cost FP Example

Source: https://fbinfer.com/docs/all-issue-types

Example of T cost due to calling another T-costed function.

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

```

--------------------------------

### Erlang NO_TRUE_BRANCH_IN_IF Example

Source: https://fbinfer.com/docs/all-issue-types

Provides an example of a NO_TRUE_BRANCH_IN_IF error in Erlang. This happens when no branches in an 'if' expression evaluate to true.

```erlang
sign(X) ->  
    if  
        X > 0 -> positive;  
        X < 0 -> negative  
    end.  

```

--------------------------------

### Run Infer on Make Hello World Project

Source: https://fbinfer.com/docs/hello-world

Execute Infer on the sample C project using 'make' for compilation. This will output a list of found bugs.

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

--------------------------------

### Inferbo Loop Over CharArray FP Example

Source: https://fbinfer.com/docs/all-issue-types

Example of T cost due to unmodeled calls, where Infer cannot determine the range of values for loop bounds.

```Java
void loop_over_charArray_FP(StringBuilder builder, String input) {
  for (Character c : input.toCharArray()) {}
}

```

--------------------------------

### Running Infer with a Make Build Command

Source: https://fbinfer.com/docs/infer-workflow

Illustrates running Infer on a make-based project. It emphasizes the need to clean build products before analysis to ensure all files are analyzed.

```bash
infer run -- make clean && infer run -- make 
```

--------------------------------

### Run Infer on iOS Hello World Project

Source: https://fbinfer.com/docs/hello-world

Execute Infer on the sample iOS app using xcodebuild for compilation. This will output a list of found bugs.

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

--------------------------------

### Erlang NO_MATCH_OF_RHS Example

Source: https://fbinfer.com/docs/all-issue-types

Shows an example of a NO_MATCH_OF_RHS error in Erlang. This occurs when the right-hand side of a 'match' expression does not match the left-hand side pattern.

```erlang
[H|T] = []

```

--------------------------------

### Run Infer in Reactive Mode on Make Hello World Project

Source: https://fbinfer.com/docs/hello-world

Use '--reactive' with 'make' to analyze only the changes in the C project, improving analysis speed.

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

--------------------------------

### Constant Address Dereference Example

Source: https://fbinfer.com/docs/all-issue-types

This C++ example shows a dereference of a pointer that holds a constant address (non-zero). Infer reports this as a CONSTANT_ADDRESS_DEREFERENCE error.

```C++
int *p = (int *) 123;
*p = 42;

```

--------------------------------

### C/C++: Buffer Overrun Example

Source: https://fbinfer.com/docs/all-issue-types

This C/C++ example illustrates a buffer overrun where an array index is out of bounds. This can lead to memory corruption and security vulnerabilities.

```C/C++
int a[3];
a[5] = 42;
```

--------------------------------

### Configure Projects with './configure' Script using infer-compile

Source: https://fbinfer.com/docs/man-infer-compile

For projects using a './configure' script that hardcodes compiler paths, use infer-compile to execute the script within the infer environment before capturing compilation commands.

```bash
infer compile -- ./configure
infer capture -- make
```

--------------------------------

### Run Infer in Reactive Mode on iOS Hello World Project

Source: https://fbinfer.com/docs/hello-world

Use '--reactive' with xcodebuild to analyze only the changes in the iOS project, improving analysis speed.

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

--------------------------------

### Analyze with Gradle

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

Use this command to analyze projects managed by Gradle or Gradle Wrapper.

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

```

--------------------------------

### Check-then-Act Bug Example

Source: https://fbinfer.com/docs/checker-racerd

This example demonstrates a check-then-act bug where a race condition can occur between checking if a list is empty and adding an item to it. This type of bug is not automatically detected by RacerD.

```Java
@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);
    }
  }
}

```

--------------------------------

### Download and Install Infer Binary

Source: https://fbinfer.com/docs/getting-started

This command downloads the latest Infer binary release for Linux, extracts it to the /opt directory, and creates a symbolic link for easy access. Ensure you replace VERSION with the actual latest release number.

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

```

--------------------------------

### Running Infer with a Clang Compilation Command

Source: https://fbinfer.com/docs/infer-workflow

Shows how to run Infer by providing a clang compilation command. This captures the compilation process to translate C files into Infer's intermediate language.

```bash
infer run -- clang -c file.c
```

--------------------------------

### Objective-C Nil Argument Example

Source: https://fbinfer.com/docs/all-issue-types

Illustrates passing nil as an argument where a non-nil value is expected, leading to a runtime exception. This example shows an error when `NSString stringWithString:` is called with nil.

```Objective-C
#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;
}

```

--------------------------------

### Erlang Bad Argument Example (Correct Type)

Source: https://fbinfer.com/docs/all-issue-types

Shows an Erlang example where concatenating a list with a number does not produce a 'badarg' error, highlighting type flexibility in Erlang list concatenation.

```Erlang
g() ->  
    [1,2] ++ 3. // no error. Result: [1,2|3]  
```

--------------------------------

### Run Intraprocedural Analysis with Infer.AI

Source: https://fbinfer.com/docs/absint-framework

This code demonstrates how to execute an intraprocedural analysis using the Infer.AI framework. It computes the postcondition for a given procedure and logs progress or handles cases where computation fails.

```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 -> ()  
```

--------------------------------

### Java Null Dereference Example

Source: https://fbinfer.com/docs/checker-pulse

Demonstrates a Null dereference scenario in Java where an attempt is made to access a field of a null object. This example is useful for understanding how Pulse identifies such memory safety issues.

```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);
    }
}

```

--------------------------------

### Erlang Bad Record Example

Source: https://fbinfer.com/docs/all-issue-types

Demonstrates an Erlang '{badrecord,Name}' error when accessing a record field using the wrong record name. The example shows attempting to access a 'person' record field from a 'rabbit' record.

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

--------------------------------

### Running Infer Capture and Analyze Separately

Source: https://fbinfer.com/docs/infer-workflow

Shows how to run the capture and analysis phases of Infer as separate commands. This allows for more control over the workflow and is equivalent to a single 'infer run' command.

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

--------------------------------

### Infinite Loop Example

Source: https://fbinfer.com/docs/all-issue-types

An infinite loop detected by Pulse. The program will not terminate.

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

```

--------------------------------

### Construct Litho Component with Specified Props

Source: https://fbinfer.com/docs/checker-litho-required-props

Demonstrates how to use the generated builder pattern to construct a Litho component, providing values for both optional and required props. This is the correct way to instantiate a component based on its spec.

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

```

--------------------------------

### Running Infer with a Javac Compilation Command

Source: https://fbinfer.com/docs/infer-workflow

Demonstrates running Infer with a Javac compilation command for Java files. This captures the compilation process to translate Java files into Infer's intermediate language.

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

--------------------------------

### Lockless Violation Example

Source: https://fbinfer.com/docs/all-issue-types

Illustrates a violation where a method annotated with @Lockless acquires a lock, which is not permitted.

```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();
  }
}
```

--------------------------------

### Analyze with Maven

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

Use this command to analyze projects managed by Maven.

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

```

--------------------------------

### Initial Infer Capture with Gradle

Source: https://fbinfer.com/docs/infer-workflow

Capture compilation commands for a Gradle project before performing analysis. This step is necessary for reactive mode.

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

--------------------------------

### Inferbo Alloc Is Negative Example

Source: https://fbinfer.com/docs/all-issue-types

malloc is called with a negative size. Fix the size argument.

```C
int n = 3 - 5; malloc(n);

```

--------------------------------

### Impure Function Example

Source: https://fbinfer.com/docs/all-issue-types

Demonstrates an impure function that modifies the state of objects within a collection during iteration.

```Java
void makeAllZero_impure(ArrayList<Foo> list) {
  Iterator<Foo> listIterator = list.iterator();
  while (listIterator.hasNext()) {
    Foo foo = listIterator.next();
    foo.x = 0;
  }
}

```

--------------------------------

### Initialize Variables Before Use

Source: https://fbinfer.com/docs/all-issue-types

Variables must be assigned an initial value before being used. Using uninitialized variables can lead to unpredictable behavior, crashes, security failures, and invalid results.

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

```

--------------------------------

### Wildcard Transition

Source: https://fbinfer.com/docs/checker-topl

Represents a transition that is always taken, often used to allow properties to start anywhere.

```Topl
start -> start: *
```

--------------------------------

### Analyze Xcodebuild Projects with Compilation Database

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

This is the most robust method for Xcode projects. It generates a compilation database using xcodebuild and xcpretty.

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

```

--------------------------------

### Recursive Factorial Function

Source: https://fbinfer.com/docs/all-issue-types

Example of a recursive function that calculates factorial. This can lead to a stack overflow if not handled carefully.

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

```

--------------------------------

### C Hello World Example

Source: https://fbinfer.com/docs/hello-world

A C code snippet with a NULL_DEREFERENCE error due to dereferencing a null pointer. Infer analyzes C code by running clang. The fix includes a null check.

```c
// hello.c  
#include <stdlib.h>  
void test() {  
  int *s = NULL;  
  *s = 42;  
}
```

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

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

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

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

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

--------------------------------

### Objective-C Block Multiple 'weakSelf' Use

Source: https://fbinfer.com/docs/all-issue-types

Example of an Objective-C block using 'weakSelf' more than once, which can lead to unexpected behavior.

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

```

--------------------------------

### C Memory Leak Example

Source: https://fbinfer.com/docs/all-issue-types

Reports memory leaks in C code when objects allocated with malloc are not freed.

```Objective-C
-(void) memory_leak_bug {
    struct Person *p = malloc(sizeof(struct Person));
}

```

--------------------------------

### Null Dereference in Objective-C

Source: https://fbinfer.com/docs/all-issue-types

This Objective-C example shows a crash occurring when dereferencing a pointer that is nil after a message passing to nil.

```Objective-C
(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  
}
```

--------------------------------

### Analyze with CMake using Compilation Database

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

This is the most robust method for CMake projects. It generates a compilation database first.

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

```

--------------------------------

### Analyze with Ant

Source: https://fbinfer.com/docs/analyzing-apps-or-projects

Use this command to analyze projects managed by Ant.

```bash
infer run -- ant  

```

--------------------------------

### Lock on UI Thread Example

Source: https://fbinfer.com/docs/all-issue-types

Shows a potential performance issue where a lock is acquired within a method annotated with @UiThread.

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

--------------------------------

### Erlang Bad Map Example

Source: https://fbinfer.com/docs/all-issue-types

Shows an Erlang '{badmap,...}' error that occurs when attempting to update a list as if it were a map.

```Erlang
f() ->  
    L = [1,2,3],  
    L#{1 => 2}.  
```

--------------------------------

### Clean Make Project Before Infer Run

Source: https://fbinfer.com/docs/hello-world

Run 'make clean' to reinitialize the directory before running Infer again, ensuring a fresh analysis.

```bash
make clean
```

--------------------------------

### Impure Function Examples in Java

Source: https://fbinfer.com/docs/all-issue-types

Illustrates impure functions. The first modifies an input array, and the second modifies a global variable.

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

```
Tokens:
Raw