ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
pattern_check.h File Reference

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>
Include dependency graph for pattern_check.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  pattern_checker

Detailed Description

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.