≈ the.bay.news

FerroProve - C-to-Rust lifter emitting #![forbid(unsafe_code)] crates with a differential oracle

The Rust Programming Language Forum
FerroProve - C-to-Rust lifter emitting #![forbid(unsafe_code)] crates with a differential oracle
I built FerroProve to lift small C modules like parsers, checksums, byte-level helpers and more into crates that compile under #![forbid(unsafe_code)], with a separate extern "C" shim (ffi.rs) and .h header so existing C callers can link without changes. c2rust transpile preserves raw pointer arithmetic inside unsafe, so an out of bounds read in C stays an out-of-bounds read in Rust. An LLM rewrite avoids unsafe but can change behavior on signed promotions or off by one inputs. FerroProve pa...

0 comments

Sign in to join the discussion — your thebay.events account works here.

No comments yet.