Running RMC with the --gen-c flag produces a C-like program output, but the outputted file is not valid C code.

Invalid parts:

• src/test/cbmc/FunctionCall_Ret-Param/main.rs
  • main can't return struct Unit, must return int
  • Tuple name (e.g. struct (u32, bool)) invalid
  • For tuples, .0, .1, etc. are invalid field names; replace with ._1?
  • overflow is not defined for addition, etc.
  • memcpy and memmove are macros, and so their headers cause compile errors
  • nondet_<k>() is not defined
• src/test/cbmc/FunctionCall_Ret-Param/main.rs + print at end
  • Array name (e.g. struct [&str] or struct [&str; 2]) invalid
  • Qualified type name (e.g. std::fmt::ArgumentV1) invalid
  • Dynamic types (e.g. dyn std::fmt::Write::vtable) invalid
  • Parameterized types (e.g. std::option::Option<usize>) invalid
  • Union types (e.g. Option-union) invalid
  • byte_extract_little_endian is not defined
• src/test/cbmc/FatPointers/boxtrait.c
  • _RINvNtCsj5Zaw82J3PU_5alloc5alloc8box_freeDNtCs21hi0yVfW1J_8boxtrait5TraitEL_NtB2_6GlobalEBG_(var_1._0, var_1._1);
    • Use -> instead of .
  • OBJECT_SIZE is not defined
  • dyn_Trait__vtable has wrong field names .__Trait__get -> .get, .__Trait__increment -> .increment