diff --git a/lib/x86.ml b/lib/x86.ml
index 61fc65c..814903c 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -2451,6 +2451,36 @@ and cast f (a : Tast.expr) (target : Types.t) dst =
     cvttf2si f.b ~f64:(f64_of src_t) ~dst:rax ~src:xmm0;
     store_loc f ~reg:rax dst dst_t
 
+(* ── Call frame information ──────────────────────────────────────────── *)
+
+(* The whole frame model, in five directives.
+
+   [.cfi] is the one thing the assembler gets right against a file with no
+   instructions in it, and it is worth saying so beside the debug-information
+   section above, which is about the thing it gets wrong: CFI advances are
+   computed from frag positions, where the line table's are computed from
+   having assembled an instruction. Measured — a [.byte]-only function comes
+   out of [readelf --debug-dump=frames] with exact advances.
+
+   The content is a constant because of the header's own claim that [rsp] is
+   written exactly twice. On entry the CFA is [rsp+8]; [push rbp] makes it
+   [rsp+16] and puts the saved [rbp] at [cfa-16]; [mov rsp, rbp] moves the
+   rule onto [rbp], where it stays for the whole body, because the only other
+   write to [rsp] is the [leave]. After that [rsp] is [rbp+8] again and the
+   CFA is [rsp+8]. Register 6 is [rbp] and 7 is [rsp] in DWARF's numbering;
+   the return address is column 16 and the CIE already says it is at
+   [cfa-8].
+
+   Emitted only in a [--debug] build, so that a release build's assembly stays
+   byte-for-byte what it was. That is a conservative call rather than a
+   principled one: this description is correct in every build, and a release
+   build is where an unwind through a crash would most want it. What stops it
+   from being unconditional today is only that nothing measures the [.eh_frame]
+   it would add. *)
+let cfi_after_push b = text b "\t.cfi_def_cfa_offset 16\n\t.cfi_offset 6, -16\n"
+let cfi_after_mov b = text b "\t.cfi_def_cfa_register 6\n"
+let cfi_after_leave b = text b "\t.cfi_def_cfa 7, 8\n"
+
 (* ── A function ──────────────────────────────────────────────────────── *)
 
 (* The frame is rounded to 16 and reserves the outgoing-argument area in the
@@ -2509,6 +2539,7 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
      column even when it is on the same line, so it gets a row of its own, and
      two rows are what let a debugger put a breakpoint after the prologue
      rather than on it. *)
+  let cfi = match dw with None -> false | Some _ -> true in
   let sub =
     match dw with
     | None -> None
@@ -2641,7 +2672,9 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
   (* The prologue, now that the frame size is known. *)
   let pb = create () in
   push_r pb rbp;
+  if cfi then cfi_after_push pb;
   mov_rr pb ~dst:rbp ~src:rsp;
+  if cfi then cfi_after_mov pb;
   let n = frame_bytes f in
   if n > 0 then sub_imm pb ~dst:rsp n;
   (match sret_at with
@@ -2703,6 +2736,7 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
     load_scalar f ~reg:(if is_float fn.Tast.ret then xmm0 else rax)
       ~off:f.retval fn.Tast.ret;
   leave f.b;
+  if cfi then cfi_after_leave f.b;
   ret f.b;
   flush pb;
   flush f.b;
@@ -2718,6 +2752,7 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
   if hidden then Buffer.add_string out (Printf.sprintf "\t.hidden\t%s\n" sym);
   Buffer.add_string out (Printf.sprintf "\t.type\t%s, @function\n" sym);
   Buffer.add_string out (sym ^ ":\n");
+  if cfi then Buffer.add_string out "\t.cfi_startproc\n";
   Buffer.add_string out (Buffer.contents pb.out);
   Buffer.add_string out (Buffer.contents f.b.out);
   (* One past the last byte, which is what [DW_AT_high_pc] and the line
@@ -2728,6 +2763,7 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
    | Some s -> Buffer.add_string out (s.send ^ ":\n")
    | None -> ());
   (match dw with Some d -> d.dcur <- None | None -> ());
+  if cfi then Buffer.add_string out "\t.cfi_endproc\n";
   Buffer.add_string out (Printf.sprintf "\t.size\t%s, . - %s\n\n" sym sym);
   Buffer.contents out, Buffer.contents f.rodata
 
@@ -2738,10 +2774,12 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false)
    the loader put them in, the program's own end of the transfer channel is a
    null cell on this frame, and the exit goes through [flan_exit] because
    stdout is a FILE* and something has to flush it. *)
-let emit_main (md : Emit.m) (fn : Tast.fn) =
+let emit_main ?(cfi = false) (md : Emit.m) (fn : Tast.fn) =
   let b = create () in
   push_r b rbp;
+  if cfi then cfi_after_push b;
   mov_rr b ~dst:rbp ~src:rsp;
+  if cfi then cfi_after_mov b;
   sub_imm b ~dst:rsp 48;
   (* [al] is zero at every call this backend makes, variadic or not — see
      [call_native]. Setting it here too costs two bytes and keeps the rule
@@ -2771,7 +2809,13 @@ let emit_main (md : Emit.m) (fn : Tast.fn) =
   ignore md;
   let out = Buffer.create 256 in
   Buffer.add_string out "\t.globl\tmain\n\t.type\tmain, @function\nmain:\n";
+  (* No [.cfi_def_cfa 7, 8] to close with, because this one has no epilogue:
+     it leaves through [flan_exit] and the [ud2] after that is unreachable.
+     The rbp rule therefore holds to the last byte, which is what a backtrace
+     out of anything [main] called needs. *)
+  if cfi then Buffer.add_string out "\t.cfi_startproc\n";
   Buffer.add_string out (Buffer.contents b.out);
+  if cfi then Buffer.add_string out "\t.cfi_endproc\n";
   Buffer.add_string out "\t.size\tmain, . - main\n\n";
   Buffer.contents out
 
@@ -2799,7 +2843,8 @@ let emit_globals_data (md : Emit.m) (globals : Tast.global list) =
 
 let init_sym = "\"flan..init-globals\""
 
-let emit_globals_init (md : Emit.m) ~externs ~fns (globals : Tast.global list) =
+let emit_globals_init ?(cfi = false) (md : Emit.m) ~externs ~fns
+      (globals : Tast.global list) =
   let b = create () in
   let f =
     { b; md; fnname = "<globals>"; retlbl = new_label () "ginit";
@@ -2830,7 +2875,9 @@ let emit_globals_init (md : Emit.m) ~externs ~fns (globals : Tast.global list) =
   end;
   let pb = create () in
   push_r pb rbp;
+  if cfi then cfi_after_push pb;
   mov_rr pb ~dst:rbp ~src:rsp;
+  if cfi then cfi_after_mov pb;
   let n = frame_bytes f in
   if n > 0 then sub_imm pb ~dst:rsp n;
   (* No caller hands this one a channel, so it gets a null cell of its own and
@@ -2841,13 +2888,16 @@ let emit_globals_init (md : Emit.m) ~externs ~fns (globals : Tast.global list) =
   store_int pb ~src:rax ~mm:(Frame f.xfer_off) ~size:8;
   lbl f.b f.retlbl;
   leave f.b;
+  if cfi then cfi_after_leave f.b;
   ret f.b;
   flush pb; flush f.b;
   let out = Buffer.create 512 in
   Buffer.add_string out
     (Printf.sprintf "\t.type\t%s, @function\n%s:\n" init_sym init_sym);
+  if cfi then Buffer.add_string out "\t.cfi_startproc\n";
   Buffer.add_string out (Buffer.contents pb.out);
   Buffer.add_string out (Buffer.contents f.b.out);
+  if cfi then Buffer.add_string out "\t.cfi_endproc\n";
   Buffer.add_string out (Printf.sprintf "\t.size\t%s, . - %s\n\n" init_sym init_sym);
   Buffer.contents out, Buffer.contents f.rodata
 
@@ -3185,11 +3235,11 @@ let program ~checks ?(dev = false) ?(debug = false) (p : Tast.program) : string
        Buffer.add_string text t;
        Buffer.add_string rodata r)
     p.Tast.fns;
-  let ginit, gr = emit_globals_init md ~externs ~fns p.Tast.globals in
+  let ginit, gr = emit_globals_init ~cfi:debug md ~externs ~fns p.Tast.globals in
   Buffer.add_string text ginit;
   Buffer.add_string rodata gr;
   (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = "main") p.Tast.fns with
-   | Some fn -> Buffer.add_string text (emit_main md fn)
+   | Some fn -> Buffer.add_string text (emit_main ~cfi:debug md fn)
    (* No [main] is not an error, and [emit.ml] treats it the same way: a
       program can be linked against a C host that brings its own entry point,
       which is what [reload_host.c] is. Refusing here made a --x86 host for the