Clang Static Analyzer vs SeaHorn

Clang Static Analyzer finds selected bugs in C, C++, and Objective-C programs. It uses symbolic execution to examine paths through code across function calls, and is part of the open-source Clang project. The analyzer is also implemented as a reusable C++ library for other tools and applications. Official releases include scan-build, a command-line tool for analyzing a codebase. On macOS, users can invoke it from Xcode; it can also run alongside clang-tidy when clang-analyzer checks are enabled. Clang-based IDEs may integrate the analyzer directly, and the documentation covers scan-build and CodeChecker. It runs on Linux, macOS, and Windows, and is self-hosted. The tool only detects bugs it has been designed to find, and analysis can take much longer than compilation. Some algorithms have exponential worst-case time, and results may include false positives. The listed free plan costs nothing.

SeaHorn is a free, open-source framework for automated analysis of C and other LLVM-based programs, developed mainly for research in automated verification. It is not an out-of-the-box static analyzer. Its frontend prepares LLVM IR bitcode, and its middle end converts optimized bitcode into verification conditions written as Constrained Horn Clauses. Backend engines use SMT-based model checking, including PDR/IC3 techniques, and CRAB can provide numerical invariants through abstract interpretation. SeaHorn supports abstract interpretation, context-sensitive pointer analysis, bounded model checking, constrained-Horn-clause software model checking, and termination or non-termination analysis. For C programs with assertions, `sea pf` translates the program, generates and solves verification conditions, displays invariants for safe results, or saves a counterexample for violations. `sea inspect` reports program structure and can produce memory or call-graph data. The framework also checks generated clauses for inconsistent code fragments using path coverage. Docker is described as the easiest starting point, with a nightly image refreshed daily. Building requires LLVM, Z3, and Boost, whose exact versions change. SeaHorn runs on Linux, macOS, or self-hosted systems under a modified BSD license.