Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
And even then, not completely reliably it seems (from Section 2.2):
> The coercions introduced by conversion rules can however lead to subtle semantic differences
The example they give is this C code:
1 uint8_t x[1] = { 0 };
2 uint8_t *y = x;
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */
1 let x: [u8; 1] = [0; 1];
2 let mut y: Box = Box::new(x);
3 y[0] = 1;
4 assert!(x[0] == 1) /* failure */
For comparison, the scpptool (my project) auto-translation (to a memory safe subset of C++) feature would translate it to something like:
1 mse::lh::TNativeArrayReplacement x = { 0 };
2 mse::lh::TNativeArrayReplacement::iterator y = x; // implicit conversion from array to iterator
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */ // dereferencing of array supported for compatibility
2 mse::TAnyRandomAccessIterator y = x; // implicit conversion from array to iterator
edit: added translation for line 2 in an alternate hypothetical situation.