Infer

Facebook Infer is a static analysis tool - if you give Infer some Objective-C, Java, or C code, it produces a list of potential bugs.

Version

0.11.0 (e77c1d8ea6d7b1fb3e027bf9458e994728f7d0b3)

Runtime

Ubuntu Xenial OpenJDK 8

Supported Languages

C C++ Java

Official Documentation

http://fbinfer.com/

YAML Configuration

infer:

  • input:

    Patterns to include in execution and reports.

  • ignore:

    Patterns to exclude from execution and reports.

  • auto-fix:

    N/A

  • config-file:

    Path to your .inferconfig file the directory of which is specified to Infer via --inferconfig-home option.

  • machine:

    • cpu:

      Amount of CPU. The default machine has 0.75 CPU with 2880 MiB RAM.

      Inspecode automatically specifies --jobs option to Infer according to this value. For example, --jobs 1 is specified by default (for 0.75 CPU), --jobs 2 is specified for 1.1 CPU.

  • options:

    Below is the list of options that are supported:

    --abs-struct <int>                          Specify abstraction level for fields of structs:
                                                - 0 = no
                                                - 1 = forget some fields during matching (and so lseg abstraction) (default: 1)
    --abs-val <int>                             Specify abstraction level for expressions:
                                                - 0 = no abstraction
                                                - 1 = evaluate all expressions abstractly
                                                - 2 = 1 + abstract constant integer values during join (default: 2)
    --allow-leak                                Activates: Forget leaked memory during abstraction (Conversely: --no-allow-leak)
    --analyzer | -a { capture | compile | infer | eradicate | checkers | tracing | crashcontext | linters | quandary | threadsafety | bufferoverrun }
                                                Specify which analyzer to run (only one at a time is supported):
                                                - infer, eradicate, checkers, quandary, threadsafety, bufferoverrun: run the specified
                                                analysis
                                                - capture: run capture phase only (no analysis)
                                                - compile: run compilation command without interfering (not supported by all frontends)
                                                - crashcontext, tracing: experimental (see --crashcontext and --tracing)
                                                - linters: run linters based on the ast only (Objective-C and Objective-C++ only)
    --<analyzer>-blacklist-files-containing <string>
                                                blacklist files containing the specified string for the given analyzer (see --analyzer for
                                                valid values)
    --<analyzer>-blacklist-path-regex <path regex>
                                                blacklist the analysis of files whose relative path matches the specified OCaml-style regex
                                                (to whitelist: --<analyzer>-whitelist-path-regex)
    --<analyzer>-suppress-errors <error name>   do not report a type of errors
    --android-harness                           Activates: (Experimental) Create harness to detect issues involving the Android lifecycle
                                                (Conversely: --no-android-harness)
    --no-angelic-execution                      Deactivates: Angelic execution, where the analysis ignores errors caused by unknown procedure
                                                calls (Conversely: --angelic-execution)
    --array-level <int>                         Level of treating the array indexing and pointer arithmetic:
                                                - 0 = treats both features soundly
                                                - 1 = assumes that the size of every array is infinite
                                                - 2 = assumes that all heap dereferences via array indexing and pointer arithmetic are correct
                                                (default: 0)
    --bootclasspath                             Specify the Java bootclasspath
    --bufferoverrun                             Activates: Activate the buffer overrun analysis (Conversely: --no-bufferoverrun)
    --checkers                                  Activates: Activate the checkers instead of the full analysis (Conversely: --no-checkers)
    --checkers-repeated-calls                   Activates: Check for repeated calls (Conversely: --no-checkers-repeated-calls)
    --clang-frontend-action { lint | capture | lint_and_capture }
                                                Specify whether the clang frontend should capture or lint or both.
    --clang-include-to-override <dir>           Use this option in the uncommon case where the normal compilation process overrides the
                                                location of internal compiler headers. This option should specify the path to those headers so
                                                that infer can use its own clang internal headers instead.
    --classpath                                 Specify the Java classpath
    --copy-propagation                          Activates: Perform copy-propagation on the IR (Conversely: --no-copy-propagation)
    --coverage                                  analysis mode to maximize coverage (can take longer)
    --no-cxx                                    Deactivates: Analyze C++ methods (Conversely: --cxx)
    --disable-checks <error name>               Do not show reports coming from this type of errors
    --dump-duplicate-symbols                    Activates: Dump all symbols with the same name that are defined in more than one file.
                                                (Conversely: --no-dump-duplicate-symbols)
    --enable-checks <error name>                Show reports coming from this type of errors
    --eradicate                                 Activates: Activate the eradicate checker for Java annotations (Conversely: --no-eradicate)
    --eradicate-condition-redundant             Activates: Condition redundant warnings (Conversely: --no-eradicate-condition-redundant)
    --eradicate-field-not-mutable               Activates: Field not mutable warnings (Conversely: --no-eradicate-field-not-mutable)
    --eradicate-field-over-annotated            Activates: Field over-annotated warnings (Conversely: --no-eradicate-field-over-annotated)
    --eradicate-optional-present                Activates: Check for @Present annotations (Conversely: --no-eradicate-optional-present)
    --eradicate-propagate-return-nullable       Activates: Propagation of nullable to the return value (Conversely:
                                                --no-eradicate-propagate-return-nullable)
    --eradicate-return-over-annotated           Activates: Return over-annotated warning (Conversely: --no-eradicate-return-over-annotated)
    --linter                                    From the linters available, only run this one linter. (Useful together with
                                                --linters-developer-mode)
    --linters-def-file <file>                   Specify the file containing linters definition (e.g. 'linters.al')
    --linters-ignore-clang-failures             Activates: Continue linting files even if some compilation fails. (Conversely:
                                                --no-linters-ignore-clang-failures)
    --quandary                                  Activates: Activate the quandary taint analysis (Conversely: --no-quandary)
    --quandary-sinks <json>                     Specify custom sinks for Quandary (default: [])
    --quandary-sources <json>                   Specify custom sources for Quandary (default: [])
    --siof-safe-methods                         Methods that are SIOF-safe; "foo::bar" will match "foo::bar()", "foo<int>::bar()", etc. (can
                                                be specified multiple times)
    --skip-analysis-in-path <path prefix OCaml regex>
                                                Ignore files whose path matches the given prefix (can be specified multiple times)
    --skip-translation <json>                   Matcher or list of matchers for names of files that should not be analyzed at all. (default:
                                                [])
    --skip-translation-headers <path prefix>    Ignore headers whose path matches the given prefix
    --sourcepath                                Specify the sourcepath
    --                                          Stop argument processing, use remaining arguments as a build command
    

    Note: Infer itself supports various analyzers, however, Inspecode supports only the following ones:

    • infer
    • eradicate
    • checkers
    • tracing
    • crashcontext
    • linters
    • quandary
    • threadsafety
    • bufferoverrun
  • thresholds:

    • num-issues:

      In addition to general severity levels, the following tool specific severity levels can be specified:

      • ADVICE (equivalent to general severity level info)
  • experimental:

    • incremental:

      N/A

      Note: The incremental analysis cannot be supported for Infer. This is because Infer performs a regular build with requiring all build dependencies and the results on unchanged files can be affected by changed files.

YAML Examples

  • With default options:

    inspecode:
      infer: default
    
  • With custom machine:

    inspecode:
      infer:
        machine:
          cpu: 1.5 # 1.5 CPU, 5760 MiB RAM
    
  • With custom options:

    inspecode:
      infer:
        options:
          - --dump-duplicate-symbols
          - --: [gcc, -c, hello.c]
    
  • With a configuration file:

    inspecode:
      infer:
        config-file: ./config/infer.config
    

    The above configuration sets the path to the configuration file to the INFERCONFIG environment variable.

Available Toolchain

  • autoconf (GNU Autoconf) 2.69
  • automake (GNU automake) 1.14.1
  • clang 3.8.1
  • cmake 3.0.2
  • gcc 4.9.2
  • g++ 4.9.2
  • javac 1.8.0_111
  • make (GNU Make) 4.0
  • musl 1.1.5
  • Apache Maven 3.0.5
  • Apache Ant 1.9.4
  • Gradle 3.4
  • Buck v2016.11.11.01

Note: Although Infer is focusing on Android and iOS apps, Inspecode does not support them as of now.

Build Command Detection

If no build commands are explicitly specified via -- option such as when using default built-in configuration, Inspecode recursively scans your repository to detect project directories enabling one of the following build systems, and then run build commands at each directory accordingly.

  • CMake (build commands: cmake . && make)
  • ./configure (build commands: ./configure && make)
  • Make (build commands: make)
  • Gradle (build commands: ./gradlew clean build)
  • Maven (build commands: mvn clean compile)
  • Ant (build commands: ant [clean|clear|clobber] [compile|build|release|debug|<default target>])

In addition, if no project directories are detected and there are any *.java files in your repository, Inspecode runs javac *.java as a build command at the root of your repository.

If the automatic detection does not suit your project, explicitly specify build commands via -- option.

Resolving Dependencies

Infer requires all build dependencies to run, so Inspecode tries to download dependencies before running Infer:

As of now, Inspecode can download:

  • submodules available to the public
  • submodules provided from your private repositories which:
    • belong to the same GitHub organization or Bitbucket team as the repository on which Infer runs
    • have been already registered to Inspecode
    • can be accessed via http://<hostname>/<path>, https://<hostname>/<path>, ssh://git@<hostname>/<path> or git@<hostname>:<path>

Note: If resolving dependencies fails due to some reasons, you can see the error log, however, Inspecode continues the process unless running Infer itself fails.

results matching ""

    No results matching ""