Skip to content

Add flag to generate GOTO program #2296

@feliperodri

Description

@feliperodri

Kani now has an option called --gen-c, which generates a C file equivalent to the Rust program. We should add a --gen-goto option as well to get the equivalent GOTO program. CBMC has an option called --show-goto-functions with a similar functionality. It could be quite helpful for debugging purposes.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions