BT

New Early adopter or innovator? InfoQ has been working on some new features for you. Learn more

Facebook Open Sources Infer, a Static Analysis Tool

| by Abel Avram on Jun 11, 2015. Estimated reading time: 1 minute |

Facebook has open sourced Infer, a static analysis tool for C, Java and Objective-C.

Facebook Infer is a static analyzer that runs incrementally on code submitted internally for review by their teams, finding bugs before the code is committed to the codebase or deployed on people’s devices. Infer currently signals Null pointer accesses, resource and memory leaks, it runs on C, Java and Objective-C code, and has been written in OCaml. Facebook uses Infer to automatically verify the code of their mobile applications for iOS and Android, correctly reporting on bugs in 80% of the cases.

Infer catches compilation commands, and translates files that are to be compiled into an intermediate language that is analyzed for possible errors. The process is incremental, meaning that only files that were modified and submitted to compilation are usually analyzed.  Infer is integrated with a number of build or compilation tools: Gradle, Maven, Buck, Xcodebuild, clang, make, javac.

This page contains more details on the type of errors found by Infer. The tool will be probably enhanced to detect array bounds errors , cast exceptions and leaking of tainted data, considering that Facebook has been working on these but the features are not yet ready.

When asked about enhancing the tool to discover other errors and covering other languages, a Facebook spokesperson told InfoQ that “Facebook feels that this journey is only one percent finished and the company is continually working to unlock more value for programmers in the future”, expressing their intent to collaborate with the community to take it further:

Infer does things well, but there are still a number of open problems across engineering organizations to be addressed. There are a lot of engineering organizations, research and academia groups that Facebook can collaborate with once it’s shared openly and from that community Facebook might eventually see new features added, new bugs checked or even new languages.

According to Facebook, Infer is built on two foundational theories, Hoare Logic – a formal system for reasoning about a computer correctness - and Abstract Interpretation - a theory for sound approximation of a program’s semantics-,  and other researches such as Separation Logic and Bi-abduction.

The source code of this tool can be found on GitHub.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT