A static analyzer for Java, C, C++, and Objective-C
https://github.com/facebook/infer
1.452 forks.
10.637 stars.
228 open issues.
Recent commits:

• [scheduler][callgraph] use counter instead of set of scheduled procsSummary: No reason to use a set when an integer will suffice. This further reduces GC churn.Reviewed By: fgasperijDifferential Revision: D19888300fbshipit-source-id: 9fc8c73f5, Facebook Github Bot
• [scheduler][callgraph] use a queue for graph leaves instead of a listSummary: Queues are implemented using a circular array, so should be less GC-heavy than continually allocating/freeing list nodes.Reviewed By: jberdine, fgasperijDifferential Revision: D18504104fbshipit-source-id: 93d29c253, Facebook Github Bot
• [scheduler][static callgraph] remove lazy init now that it's enforced in ProcessPoolSummary:Building the call graph should be done only in the scheduler process after having forked all workers. This was achieved by a lazy init pattern, whereby the first time `next` was called, it would build the call graph, on the assumption that `next` is only ever called in the scheduler after forking.D19769741 made this compulsory regardless the scheduler by passing a thunk to `ProcessPool` which is called to obtain the actual scheduler, on the right process and after the fork.This means we don't need the custom lazy init logic any more. In addition, that set up used a DB query to overapproximate the number of procedures to analyse, because this was supposed to be provided *before* forking. Now this is also not needed, and on top of that we can provide the exact number after building the call graph.Reviewed By: ezgicicekDifferential Revision: D19833974fbshipit-source-id: 7f6d51d93, Facebook Github Bot
• [purity] Remove duplicated/unnecessary codeSummary: clowntownReviewed By: skchoDifferential Revision: D19881696fbshipit-source-id: a01acf7b4, Facebook Github Bot
• [inferbo] Distinguish unreachable and error statusSummary:In Inferbo, the bottom memory is introduced when a node is unreachable by pruning, i.e.`[[e]] <= [0,0]` on `prune(e)`. This diff distinguishes whether `[[e]]` is `[0,0]` (unreachable)or bottom (it could not evaluate `e` by some unknown reasons).Reviewed By: ezgicicekDifferential Revision: D19902046fbshipit-source-id: 7706017d6, Facebook Github Bot