;;;; A stopped stack holding two pointers into Vec storage, one of which is ;;;; already dead. The allocation registry is what lets the inspector tell ;;;; them apart, and this is the program that shows it: ;;;; ;;;; ("live" "(Ptr Enemy)" "") ;;;; ("dead" "(Ptr Enemy)" "") ;;;; ;;;; N is the registry's own event counter and is no part of the claim: it ;;;; moves if anything allocates or frees ahead of this program's two Vecs. ;;;; A test that asserts these lines should match around it, not on it. ;;;; ;;;; Both lines are what `(:op "locals" :frame 1)` answers with today, and ;;;; both were read off a running session by hand. **No test drives this ;;;; program yet**: the case belongs beside the other `locals` and `inspect` ;;;; cases in test_dev.ml, which is another lane's file. NEXT.md says so ;;;; rather than letting the verification read as automated. ;;;; ;;;; Why a Vec rather than a struct on the stack: a stack address is not in ;;;; the registry by design — the shadow stack already answers for a local by ;;;; name — so a pointer to one renders , which is neither half of what ;;;; this is demonstrating. (import agent "vendor:agent") (defstruct Boom [why i32]) (defstruct Enemy [hp i32 x i32]) (defn deeper [] i64 (restart-case (do (error (Boom {.why 7})) 1) (carry-on [] 5))) (defn outer [] i64 (let [v (vec-new Enemy) w (vec-new Enemy)] (push v (Enemy {.hp 41 .x 2})) (push w (Enemy {.hp 7 .x 9})) (let [live (addr (at v 0)) dead (addr (at w 0))] (free w) (deeper)))) (defvar ticks i64) (defn main [] i32 (agent/start "/tmp/flan-dev-ptr-fallback.sock") (print (outer)) (println "") (dotimes [i 4000] (agent/wait 5) (set ticks (+ ticks 1))) 0)