Skip to main content Module reentrancy Copy item path Source Analyzer 🔒 BalanceForm 🔒 A supported additive source pattern on one path. An empty term list is balance-independent.
At most two balance terms are retained: a stale/current comparison needs one of each. More
terms are rejected rather than cancelled, since Solidity arithmetic may wrap or revert. BalanceTerm 🔒 One signed balance read, retaining the calls across which it was cached. BalanceValue 🔒 Balance-related facts about a value flowing into a local, parameter or return slot. CallCollector 🔒 Collects the internal functions and modifiers a function invokes directly. FlowState 🔒 Facts that hold along one execution path. InlineCallKey 🔒 Operand 🔒 A local variable or constant appearing in a predicate or lock expression. PathPredicate 🔒 ReentrantCallKind 🔒 REENTRANCY_GAS_STIPEND 🔒 Gas stipend forwarded by transfer/send; a call capped at or below it cannot reenter. REENTRANCY_BALANCE REENTRANCY_ETH REENTRANCY_NO_ETH balance_reentry_lock 🔒 The reentrancy-guard lock, if any, that protects every entry point of every deployable
contract exposing entry. branch_stops_current_path 🔒 break/continue or anything that exits the function, so the current path stops here.call_option 🔒 call_options_allow_reentrancy 🔒 True unless a gas: option provably leaves the callee too little gas to reenter. call_sends_eth 🔒 call_uses_delegate_context 🔒 delegatecall/callcode, which run the callee in the caller’s storage context.callee_can_reenter 🔒 An external call that hands control to another contract: a low-level call/callcode/
delegatecall on an address, or a state-changing external function call. cast_args 🔒 Arguments of a plain type conversion such as uint256(x) or address(x). collect_internal_calls 🔒 common_path_predicates 🔒 const_value 🔒 Constant-folds expr over literals, constant variables, casts, ! and ==/!=; lock
supplies the value of the lock variable. constrain_boolean_outcome 🔒 Records in state that expr evaluated to outcome; returns false if that is impossible. constrain_paths 🔒 Keeps the paths compatible with active, extended by the active predicates. forget_path_predicates 🔒 Drops every path fact that mentions the (re)assigned local var_id. guard_activation 🔒 The lock and value set by the last of stmts (directly or via an argument-less helper), if
an earlier statement rejects that value. guard_locks 🔒 Locks of the standard reentrancy guards among function’s modifiers. guard_restoration 🔒 The lock and value restored by stmt (directly or via a single-statement helper). is_entry_point 🔒 Non-view functions an external caller can invoke: public/external functions, fallback and
receive. is_uncapped_value_call 🔒 .call{value: v}(...) with a non-zero value and no gas cap other than gasleft().is_view_or_pure 🔒 is_zero_value 🔒 join_branches 🔒 Replaces state with the union of the reachable branches, keeping only the path predicates
all of them agree on. Returns whether any branch was reachable. merge_maps 🔒 owned_by 🔒 The variables of func_id. path_predicate 🔒 The boolean fact expr establishes when it evaluates to true: a local flag, its negation,
or an ==/!= between locals and literals. paths_compatible 🔒 predicate_operand 🔒 remap_return_paths 🔒 Rewrites the callee-local predicates in the returned values into the caller’s terms. simple_internal_call 🔒 f(); naming exactly one function.standard_reentrancy_guard_lock 🔒 The lock state variable of a standard reentrancy guard modifier: it rejects re-entry, sets
the lock, runs _ exactly once and restores the lock right after. state_lock_assignment 🔒 lock = <constant>; on a state variable.static_internal_callee 🔒 Internal function statically named by callee: a bare identifier or super.f. stmt_rejects_lock_value 🔒 True if stmt reverts whenever lock_var holds entered. ModifierContinuation 🔒 What to analyse when a modifier’s _ is reached: the remaining modifiers, the function body
and the reentrancy-guard lock the current modifier holds. PathAlternatives 🔒 PathPredicates 🔒