That assumes zero translation errors as well as the original C code not relying on a particular compiler's specific implementation of unspecified behavior.
That assumes zero translation errors as well as the original C code not relying on a particular compiler's specific implementation of unspecified behavior.
As for unspecified behaviour... that's true! Again I wonder if clang is a useful component here: I suspect if C code behaves correctly with clang, then the translation to Rust compiled with rustc probably works too, both because the translator uses clang, and because both compilers use LLVM.
The point (in contrast to the usual complaint of Animats) I was trying to convey, but was nitpicked was: a correct translation from fully-specified C to unsafe Rust doesn't add any unsafety. Whether this applies in practice is slightly different, but there's questions about whether pretty much any statement about C code applies in practice: since undefined behaviour is so rife and easy to trigger, many/most programs are outside the specification (fuzzing C programs often results in segfaults---undefined behaviour---and so the program is outside the bounds of C).
Wrapping up, I'll emphasise that the value in this sort of translation is as a stepping stone towards safe Rust, not as a final `unsafe` product.
The approach we've taken so far with C2Rust is to build compiler plugins that instrument C and Rust code so we can dynamically check their behavior when fed the same input.