A global is program state a frame happened to touch, not part of it, so nesting it under one implies an ownership that is not there and repeats the name once per frame that reads it. One section instead, holding the union of the globals every frame on the stack references — the compiler does the choosing, since Reach.expr_refs already answers a body's reference set, and listing every global a program has would bury the one that matters under the prelude's PRNG state. Each entry says which frames touch it, by the index the stack section already numbers them with, which recovers what per-frame nesting would have told you at no cost in duplication. Ordered by the innermost frame that touches it: a deep stack makes the union large and proximity to the error is what puts the likely culprit on top. Simpler than locals, because a global is reached by name rather than by address. Emit.redefinition writes a global the host has as external, so the thunk binds to the program's own storage and nothing is asked of the stopped thread — no dev-slot round trip and no not-yet-bound case to refuse. A frame that cannot be attributed contributes nothing and is named in :skipped; the union being incomplete and the union being complete are different answers. The hole in that is stated rather than papered over: slot_fingerprint hashes a body's slots, which is the right cut for locals and not for this, so a body that names different globals while binding the same locals is not caught. The test drives the case that is. MANUAL.md also loses a stale paragraph claiming the fingerprint check never fires with a failing test pinned to it. It fires, and test_dev covers it.
Description
Languages
OCaml
67.2%
Emacs Lisp
15.2%
C
10.4%
HTML
2.9%
Standard ML
2.8%
Other
1.5%