CrabArchitecture

Crab has been designed in a modular fashion so that new components (abstract domains, fixpoint algorithms, and inter-procedural or backward analyses) can be easily plugged in. The only fixed component is its intermediate representation, called CrabIR.

The input to Crab is a set of CFGs expressed in CrabIR. The syntax and concrete semantics of CrabIR are described in the paper "Abstract Interpretation of LLVM with a Region-Based Memory Model" (VSTTE'21) (PDF).

The output of Crab consists of: invariants (per basic block), summaries (pairs of preconditions and postconditions per functions, if inter-procedural analysis is enabled), and necessary preconditions (if backward analysis is enabled). In addition, CrabIR supports assertions (similar semantics to C asserts) so that Crab can check them (Assertion Checker).