infer

This is a binary release of Infer for Linux and MacOS. To use it follow these instructions.

Changes

A lot has happened in the years since 1.1.0 so these are just the highlights. Full Changelog: https://github.com/facebook/infer/compare/v1.1.0...v1.2.0.

Checkers

• Pulse is now enabled by default and replaces Biabduction as the default memory and value analysis engine for Infer. Pulse powers a lot of issue types historically reported by other checkers, such as null dereferences, memory/resource leaks, reads of uninitialised values, as well as a range of new issue types such as (user-configurable) tainted data flows and C++ unnecessary object copies.

• The Resource Leak checker for .NET and Uninitialized Value checkers have been removed and their functionality moved to Pulse for improved precision.

• The linter framework ASTLanguage (AL) has been removed (previously deprecated). Other clang-based linter frameworks such as clang-tidy can be used instead.

• Eradicate has been removed (previously deprecated).

• Two other checkers have been deleted: Config Checks between Markers (previously experimental) and Immutable Cast (previously deprecated).

• Biabduction is now deprecated in favour of Pulse.

• Quandary is now deprecated in favour of Pulse's taint analysis.

• New checker: Lineage produces inter-procedural data flow graphs for Erlang code and provides commands to query taint paths in it.

• New checker: Parameter Not Null Checked for Objective-C, replacing the PARAMETER_NOT_NULL_CHECKED bug type reported by biabduction.

• New checker: Scope Leakage for Java and Kotlin, verifying that certain classes can never retain others in a configurable way.

• Annotation Reachability: support for C++ was dropped and Java support was improved to support using regexps to model annotated functions, and having field accesses as sinks.

Languages

• New Erlang frontend. You can analyse Erlang code compiling with erlc, rebar3 or buck2.

• New Hack frontend, based on hackc.

• New "Textual" intermediate frontend. Textual is a new input format that frontend writers may use to emit SIL, either in text form or from OCaml directly. It is currently used by the Hack frontend. Textual can also be used to write analysis models, i.e. stubs for certain functions that will be used during the analysis as if they were these functions' implementations.

Build System Integrations

• Clang upgraded to version 18.

• buck2 support.

Backend

• Incremental mode much improved, see the new --incremental-analysis flag in the updated workflow for CI d

This is a new release of Infer, with a binary tarball for Linux. On MacOS, using Homebrew is recommended. Please follow these instructions.

Frontends

• New JSON input format for SIL. This new format was contributed from Infer#, whose C# frontend for Infer emits SIL as JSON using this format.

Build System Integrations

• Clang upgraded to version 11.0

Checkers

• Liveness: properly handle exceptional control flow
• Pulse:
  • Added preliminary Java support
  • New Uninitialized value bug type, aiming to replace the previous Uninit checker as this one is inter-procedural and more precise.
  • OPTIONAL_EMPTY_ACCESS is now enabled by default
• NEW checker Topl(early alpha): An experimental checker framework: write your own analysis as a state machine representing a temporal property over multiple memory objects at once, eg to write a taint analysis. Topl is based on Pulse.
• Miscellaneous improvements to cost, inferbo, nullsafe, racerd, starvation

The sha256 checksums of the tarballs are:

$ shasum -a 256 infer-linux64-v1.1.0.tar.xz
5f5d453814422e93e2a70998d8946b09a2721628ff427f67ff0123dea87461d4  infer-linux64-v1.1.0.tar.xz

This is a binary release of Infer for Linux and MacOS. To use it follow these instructions.

The Linux binary is built for Ubuntu 18 and may require adjustments to run on other configurations.

The Mac binary is built for the Catalina version. MacOS users may get an error "developer cannot be verified" and need to allow the app to run manually following these instructions, or alternatively get infer from Homebrew when it is released there.

The sha256 checksums of the tarballs are:

$ shasum -a 256 infer-*-v1.0.0.tar.xz              
510eeccc7e6bcc2678ac92a88f8e1cb9c07c3e14d272dcc06834e93845bb120f  infer-linux64-v1.0.0.tar.xz
4f188959f7c61e2ef3b935c8a9e5e66632d7fcb90c5362336fb8305d4f74d6b7  infer-osx-v1.0.0.tar.xz

Changelog

Checkers

AL is now deprecated and may be removed in future versions.

Annotation Reachability

• reporting format improvements (the trace is no longer included in the report text, only as metadata)

Biabduction

• disable some less-used bug types

Eradicate

• remove "Field not mutable" check

RacerD

• Now defaults to "angelic" ownership: an unknown function is assumed to return owned objects.
• No more reports on races on paths rooted on temporary or local variables, as these are unreliably modelled.

Litho Required Properties: new Java checker to check that all non-optional @Props have been specified when constructing Litho components. Self in Block: new Objective-C checker to detect when an Objective-C block incorrectly captures self Starvation

• New experimental "global" analysis mode. Enable with --starvation-whole-program

Miscellaneous improvements to most checkers, in particular Annotation Reachability, Cost Analysis, Eradicate, Inefficient Keyset Iterator, InferBO, Pulse, RacerD, Starvation, and Uninitialized Value.

Build System Integrations

• The Gradle integration now captures Java files in parallel
• New Buck integration for Java, enable with --buck-java-flavor
• Clang upgraded to version 9.0

Command Line Interface

• New subcommand infer help to display information about checkers and issue types.
• New subcommand infer debug that replaces the uses of infer explore not related to reported issues.
• --debug no longer disables filtering, you have to pass -g -F to get the previous behaviour back.
• All disk artefacts (except the Java type environment) are now stored in the SQLite database in infer-out/results.db. The contents of the database can be explored with infer debug.
• Changed how to select the Buck integration. The old command line interface is still supported but is now deprecated.
  • clang via "flavors", activated with --flavors, now with --buck-clang
  • clang via "compilation DB", activated with --buck-compilation-database, unchanged
  • Java via "genrule", activated with --genrule-master-mode, now with --buck-java
  • Java "without genrules", used to be activated b

This is a binary release of Infer for Linux and MacOS. To use it follow these instructions.

Highlights:

• There’s a new --inefficient-keyset-iterator checker for finding inefficient uses of Java's keyset iterators that retrieve both key and value (on by default).
• Complete the set of Android thread annotations and Java nullability annotations. Updated artifacts are available on Maven Central.
• --starvation is now on by default. This analysis catches problems with threads not being able to make progress due to locking issues, incorrect scheduling priorities, etc. For instance, on Android calling Future.get from a UiThread without a sensible timeout will be flagged as a starvation issue.
• New Objective-C linter for calls to @optional methods: UNSAFE_CALL_TO_OPTIONAL_METHOD, enabled by default.
• A new call-graph scheduler (--call-graph-schedule) improves performance of the analysis phase of Infer, especially when the number of files to analyze is less than available CPUs.
• A new flag --oom-threshold allows to throttle the analysis when the amount of free memory is below the provided threshold.
• New genrule based Buck/Java integration is much faster than the previous one, use with --genrule-master-mode.
• Infer’s internal clang is now in version 8.0.0.
• Update to javalib 3.1 provides better compatibility with Java 9 and Java 11. Refer to their change log for more details.
• Infer can now be built and run on MacOS Mojave without fiddling with SDKROOT (although you still might need it with non-standard toolchain setup).
• [β] Pulse is a new experimental lifetime analysis for C++, give it a try with --pulse. Beware that it doesn’t report much yet.
• --ownership checker was superseded by Pulse and removed.

... and many other fixes and improvements. For the full list of changes included see here.

The facebook-clang-plugins version used for this release is https://github.com/facebook/facebook-clang-plugins/commit/9386890e42043d04f9 cd9e7b204cb525d4417c41.

The sha256 checksums of the tarballs are:

$ shasum -a 256 infer-*-v0.17.0.tar.xz
de972ba3043f18b29a8eff6cd7612e24f5ffaef038dc7949befeaf490931725e  infer-linux64-v0.17.0.tar.xz
1a3ef6fb51846ae63ffd7fde3b0255f75bab6157f5de1842606fa32988d101f8  infer-osx-v0.17.0.tar.xz