Skip to content

Add support for --generate-function-body-options in Rust and C++ API #7660

Open
@NlightNFotis

Description

@NlightNFotis

Description

Add support for the goto-instrument options --generate-function-body-options and --generate-function-body in the Rust and C++ API.

The end result should be facilitating an interaction with the API that achieves a similar result to the following goto-instrument invocation: goto-instrument --generate-function-body-options assert-false-assume-false --generate-function-body ".*" --drop-unused-functions 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