c2rust defines some undefined behavior in input C programs #1253
Description
This may or may not be a problem depending on what kind of translation is desired, but this came up in discussions about using c2rust and verifying the relation between the input and transpiled code.
In short, some cases of undefined behavior in input C code have their behavior defined in the generated Rust code. For example, signed integer overflow is UB in C, and compilers are free to do whatever they like with it. c2rust, on the other hand, translates C signed integer operations to the corresponding Rust signed integer operations, which do not exhibit UB in any case.
This kind of modification to add further definedness would be legal for a C compiler to do, but not all users of c2rust are OK with that kind of transformation, as it is not strictly semantics-preserving.
I'm not sure how much work it would be to audit the transpiler and identify all the locations where we further define the behavior of input C, but we could look into this.