Ethereum Detectors

Manticore has built-in "detectors" for certain properties of Ethereum smart contracts. Used in this way, Manticore acts like a linter that reports on these conditions as they are observed while exploring the state space of a smart contract. These detectors may or may not apply to the contract being explored, may falsely detect issues, or may fail to report a true issue. These detectors are a default set of properties that we expect most contracts will share. It is always best to reason about the properties of your contract, and build analyses to verify them.

List of Ethereum Detectors

Note, no detectors are run by default. To enable all detectors, run Manticore with --detect-all.

Detector	Description
--detect-overflow	Integer overflows
--detect-invalid	INVALID instructions
--detect-uninitialized-memory	Use of uninitialized memory
--detect-uninitialized-storage	Use of uninitialized storage
--detect-reentrancy	Re-entrancy
--detect-reentrancy-advanced	Re-entrancy (best used by API, not CLI)
--detect-unused-retval	Unused internal transaction return value
--detect-delegatecall	Problematic use of DELEGATECALL
--detect-selfdestruct	Reachable SELFDESTRUCT instructions
--detect-externalcall	Reachable external call or ether leak to sender or arbitrary address
--detect-env-instr	Use of potentially unsafe or manipulable instructions
--detect-race-condition	Possible transaction race conditions (transaction order dependence)