repository·main·Indexed 12 days ago
https://github.com/facebook/inferA static analysis tool written in OCaml used to detect bugs and analyze code quality for Java, C++, Objective-C, and C projects, designed for large-scale software verification.
Infer is a static program analyzer designed to detect deep software defects such as null pointer dereferences and data races. It performs inter-procedural analysis, meaning it can reason about multiple functions or methods across different files.
Supported Languages:
Charon is a tool designed to extract the complete contents of a Rust crate and its dependencies into a structured JSON file. This output is intended for semantic analysis and code verification, providing a uniform way to access information from rustc internals.
The exported JSON includes:
crate_name: The name of the crate.type_decls: Type declarations.fun_decls: Function declarations.global_decls: Global declarations.trait_decls: Trait declarations.trait_impls: Trait implementations.Additionally, it provides simplified MIR (Mid-level Intermediate Representation) bodies of functions and source information for each item.
ppx_show is an OCaml PPX deriver based on ppxlib. It reimplements the show plugin functionality from ppx_deriving, allowing you to automatically derive show capabilities for your types.Infer includes checkers designed to detect various types of "starvation" problems in your code, including:
@Lockless annotation violations: Detecting code that violates the contract of @Lockless annotations.StrictMode policies.The repository is organized into two main components:
clang-to-json AST exporter.In Litho, components are defined using spec classes where inputs are annotated with @Prop. If a @Prop is not marked as optional = true, it is considered a required prop.
When a component is constructed using the generated builder pattern, all required props must be set. If they are omitted, the annotation processor throws a runtime exception. The litho-required-props checker performs inter-procedural analysis to detect these missing calls statically, even if the create() and build() calls are separated by complex control flows or function calls.
// Spec definition
class MyComponentSpec {
static void onCreate(
ComponentContext c,
@Prop(optional = true) String prop1,
@Prop int prop2) {
...
}
}
// Correct usage (both props provided)
MyComponent.create(c)
.prop1("My prop 1")
.prop2(256)
.build();
// Incorrect usage (prop2 is missing and will trigger MISSING_REQUIRED_PROP)
MyComponent.create(c)
.prop1("My prop 1")
.build();The IMPURE_FUNCTION issue type in Infer identifies functions that exhibit side effects by modifying their input arguments or external state rather than just returning a value. In Java, a common example is a function that iterates through a collection passed as an argument and modifies the internal state of the objects within that collection.
void makeAllZero_impure(ArrayList<Foo> list) {
Iterator<Foo> listIterator = list.iterator();
while (listIterator.hasNext()) {
Foo foo = listIterator.next();
foo.x = 0;
}
}The SwiftObjCNullability checker identifies potential runtime crashes caused by calling Objective-C methods from Swift when those methods lack explicit nullability annotations (_Nullable or _Nonnull) on pointer return types.
When an Objective-C method lacks these annotations, the Swift clang importer treats the return type as an Implicitly Unwrapped Optional (T!). If the method returns nil at runtime, any subsequent use of that value will cause a trap (crash). This checker flags these call sites at compile time so the contract can be explicitly defined.
_Nullable or _Nonnull to the pointer return type in the Objective-C header.as? at the Swift call site to handle the result as a standard Optional instead of an implicitly unwrapped one.WEAK_SELF_IN_NO_ESCAPE_BLOCK check is an intra-procedural analysis. To maintain simplicity, it identifies weak pointers to self by name. It assumes that any captured weak pointer whose name contains the string self is a weak reference to the current self object.Infer reports an issue when a config value (typically a boolean used to enable experimental features or gatekeepers) is used as a branch condition within a function.
This issue is intended to provide semantic information about the code's structure rather than reporting a bug, error, or actual problem. It helps identify which functions are gated by specific configuration flags.
void foo() {
if(config_check("my_new_feature")){ ... }
}