The C standard formalized in Coq