_shb

Infer has a thread-safety checker that identifies races in classes annotated with `@ThreadSafe` (http://fbinfer.com/docs/experimental-checkers.html).

I added some documentation on using Inferbo and other experimental checkers we are working on: http://fbinfer.com/docs/experimental-checkers.html.

All you need to do to use Inferbo is add `-a bufferoverrun` to your normal Infer command. Inferbo isn't included in 0.9.4.1, but we'll be creating a new release soon.

Thanks for pointing this out! Fixed in an update to the post.

Infer does bottom-up analysis: it starts at the bottom of the call graph and analyzes each procedure once independently of its callers. Analyzing the procedure produces a concise summary of its behavior that can be used in each calling procedure. This means that the cost of the analysis is roughly linear in the number of nodes in the call graph, which is not true for a lot of other interprocedural analysis techniques.

It's true that it a procedure changes that you may have to re-analyze all dependent procedures (and calling procedures!) in the worst case. However, in the bottom-up scheme you only need to re-analyze a procedure when the code change produces a change in the computed summary, and in practice summaries are frequently quite stable.

There was indeed a typo in the description; it has been fixed. Sorry for the confusion!

To paint these tools with an overfly broad brush, they linter-like in that they perform shallow intra-procedural analysis to identify common bug patterns (e.g., if (x != null) { y = x.f } z = x.f // possible NPE; x was previously checked for null or foo(String s) { if ("x" == s) // oops, should use .equals() for Java String comparison. }).

By contrast, Infer performs deeper inter-procedural reasoning that can track the flow of values across long chains of procedure calls to identify subtle bugs that are hard to see with the naked eye. Infer doesn't support as many bug patterns as these existing tools do yet, but it can find some deep bugs that these tools will miss.

Yes, it can be used with most Java code you can build on the command line. Just run "infer -- <your_build_command>". Currently, this works with javac, Ant, Maven, and Gradle. See http://fbinfer.com/docs/hello-world.html#hello-world-android for a Gradle example.

This paper describes some aspects of the system: http://research.microsoft.com/pubs/189242/pldi097-burckhardt...