forked from unom/punktfunk
enricobuehler
d72822ced7
`linux/mod.rs`'s fifteen sites are the same kind as `video_vulkan.rs`'s, not the ash kind: nine raw pointer dereferences and six libav calls, all inside `CudaHw::new`, which had no `unsafe` block and therefore no proof of the one thing worth proving here — that the pointer chain it walks is live. The marker STAYS (`cu_ctx: *mut c_void` is a `CUcontext` the caller must supply valid). The body is now two blocks, one per phase, because there are two distinct arguments to make. Both turn on the same non-obvious fact: `av_hwdevice_ctx_alloc`/`av_hwframe_ctx_alloc` return null or a ref whose `data` libav has ALREADY initialized, and `AvBuffer::from_raw` rejects null — so the `?` leaves before any of the field stores below it can run. That is what makes the `(*dev_ctx)`/`(*fc)` writes in-bounds stores on live allocations rather than a hope, and it is exactly the reasoning that was missing. The device block also records the ordering constraint that was implicit: `cuda_ctx` must be stored BEFORE `av_hwdevice_ctx_init`, which reads it. Two files now need no exemption: 14 fenced -> 12. Both were removable for the same reason — their sites are pointer dereferences, where a proof carries an argument, unlike the ash backends where it could only restate the call. That is the criterion for which fence to attack next, not file size. Verified on .21: fmt + `clippy --workspace --all-targets -- -D warnings` + the feature-gated `-p pf-encode --features nvenc,vulkan-encode,pyrowave` step, all rc=0 with no allow in either file.