|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Pattern-based vulnerability detection for Solidity contracts. More...
#include <memory>#include <iomanip>#include <util/symtab/context.h>#include <util/symtab/namespace.h>#include <util/irep/std_types.h>#include <fmt/core.h>#include <nlohmann/json.hpp>#include <solidity-frontend/solidity_grammar.h>Go to the source code of this file.
Classes | |
| class | pattern_checker |
Pattern-based vulnerability detection for Solidity contracts.
Declares pattern_checker, which performs static pattern matching on the solc JSON AST to detect known vulnerability patterns (e.g., authorization via tx.origin, reentrancy patterns) without requiring full symbolic execution. Complements ESBMC's reasoning-based verification pipeline.