Translating C to Safe Rust: Reasoning about Pointer Types and Lifetimes