Skip to content

Add missing call for C++/Rust API: --ensure-one-backedge #7661

Open
@NlightNFotis

Description

@NlightNFotis

Description

Add support for the goto-instrument option --ensure-one-backedge in the C++/Rust API.

The end result should facilitate an API interaction similar to what you can achieve with the following binary invocation: goto-instrument --ensure-one-backedge-per-target b_harness.out b_harness.out

Context

[This is to track items outlined in #7042 that are missing to make the C++ and Rust API more useful]

Metadata

Metadata

Assignees

No one assigned

    Labels

    KaniBugs or features of importance to Kani Rust VerifierRust APIIssues pertaining to the CBCM Rust API

    Type

    No type

    Projects

    Status

    No status

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions