Skip to content

Add capacity for linking model in the same way as goto-cc for C++/Rust API #7658

Open
@NlightNFotis

Description

@NlightNFotis

Description

Add support for linking models from separate files (and potentially writing the resulting model into a separate file on disk), and specialising with the --function.

Ideally, the end result should allow interaction with the API that achieves the same outcome that the following two calls achieve:

  1. goto-cc a.out /home/ubuntu/git/kani/library/kani/kani_lib.c -o b.out
  2. goto-cc b.out --function harness -o 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