Goto-Transcoder v0.1

This is the first release of the transcoder with a minimal set of features. This version should be able to handle a subset of C and Rust goto programs generated by CBMC and Kani.

Support

• Primitive and complex types.
• Function calls
• Expressions: "if", "member", "typecast", "notequal", "and", "or", "mod", not", "", "/", "+", "-", "=", "<", ">", "overflow_result-+", overflow_result--", "overflow_result-", "overflow_result-shr", "lshr", "ashr", "shl", address_of", "index", "byte_extract_little_endian", "pointer_object", "array_of", "sideeffect", dereference", "object_size", "bitand", "struct", "return",

Limitations

• Memory safety is not supported
• For Rust we require a custom release of esbmc: https://github.com/esbmc/esbmc/releases/tag/nightly-7867f5e5595b9e181cd36eb9155d1905f87ad241