Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Known Limitations

This page documents the current analysis boundaries of ilold. Understanding these limitations is necessary for interpreting slice, timeline, and trace results correctly.

Intraprocedural slicing only

The dataflow slicer operates within a single function body (plus its inlined modifiers). It does not follow values across function call boundaries. If deposit calls an internal helper _updateBalance(amount), the slice for amount in deposit will show the call site but not the writes inside _updateBalance. Use tr <func> to inspect internal call bodies separately.

Assignment-only DEF extraction

Only Assignment expressions (x = ..., x += ..., x -= ...) produce DEF entries in the slicer’s use-def analysis. Solidity mutations that are not modeled as assignments – specifically x++, x--, ++x, --x, delete x, arr.push(v), and arr.pop() – are captured as USEs of the target variable but not as DEFs. A backward slice on a variable mutated exclusively through .push() will miss the mutating statement as a definition point.

Modifier placeholder split

Modifier bodies are split at the first top-level _; (placeholder) statement to separate “before” code from “after” code. If the placeholder appears inside a nested block (e.g., inside an if branch), the entire modifier body is treated as “before” code. This is over-inclusive: statements that should execute after the function body will appear before it in the flattened view. In practice, most modifiers place _; at the top level, so this rarely triggers.

Forward slice over-tainting via ancestor merge

When a statement is included in a forward slice, its lexical ancestors (enclosing if, for, while blocks) are also included so that the rendered slice shows control-flow context. The ancestor’s condition variables are merged into the tainted set. This means an if (unrelatedCondition) enclosing a tainted write will add unrelatedCondition to the taint set, potentially pulling in unrelated statements in subsequent iterations. The result is a conservative (larger) slice rather than a precise one.

Tuple destructuring

Tuple destructuring assignments such as (a, b) = foo() may not be recognized as DEFs depending on how the Solidity frontend lowers them. If the frontend does not emit a top-level Assignment node, the individual targets (a, b) are treated as USEs only. This can cause a backward slice to miss the destructuring as a definition point for a or b.

Timeline tracks state mutations only

The timeline command tracks writes to state variables across session steps. Local variable assignments within a function body are recorded separately (local_entries) but are not visible in the default timeline output. If you need to trace a local variable, use slice within the specific function instead.

Session requires at least one call

The timeline, state, and sequence endpoints require an active session with at least one Call step. The timeline and state commands return empty results if no steps have been added. The sequence command requires at least two steps. Use tr <func> for read-only inspection of a function’s flow without adding it to the session.

Internal and private functions cannot be session entry points

Session steps model real external transactions. Functions with internal or private visibility cannot be called from outside the contract, so they cannot be added as session steps via c <func>. Use tr <func> to inspect their execution flow, or call a public/external function that invokes them to see their effects through the modifier and internal-call inlining in the trace.