Clang LibTooling + Z3 BV-64 encoding. 11 detectors: clone, equiv, class-dup, dead, null-deref, div-by-zero, int-overflow, oob, int-truncation, sign-conversion, taint-track. Interfaces: CLI, MCP (JSON-RPC 2.0), LSP. Output: SARIF 2.1.0, JSON, Markdown.
5 lines
195 B
C++
5 lines
195 B
C++
// `x + x` and `x * 2` are equivalent over bit-vector arithmetic. Different
|
|
// ops, same semantics — a clean Type-4 case.
|
|
|
|
int dbl_a(int x) { return x + x; }
|
|
int dbl_b(int x) { return x * 2; }
|