Skip to content

Fix hard-coded assumptions about debug target #841

@tedinski

Description

@tedinski

Note: this applies to debug/release builds of our binaries (kani-compiler, cargo-kani, etc), not of user code.

We encode several assumptions that we're running debug builds:

$ git grep -- 'target\/\*'
scripts/cargo-kani:KANI_CANDIDATES=("$REPO_DIR"/target/*/cargo-kani)
scripts/cargo-kani:    echo "Looked for: '$REPO_DIR/target/*/cargo-kani'"
scripts/kani:KANI_CANDIDATES=("$REPO_DIR"/target/*/cargo-kani)
scripts/kani:    echo "Looked for: '$REPO_DIR/target/*/cargo-kani'"
scripts/kani-rustc:    local KANI_CANDIDATES=("$REPO_DIR"/target/*/kani-compiler)
scripts/kani-rustc:            echo "Looked for: '$REPO_DIR/target/*/kani-compiler'"
$ git grep "target/debug"
src/cargo-kani/src/session.rs:        if exe.ends_with("target/debug") {
src/cargo-kani/src/session.rs:                path.push("target/debug/kani-link-restrictions");
tools/compiletest/src/main.rs:    let kani_bin_path = &rust_src_dir.join("target/debug/kani-compiler");

Most of these affect only debug/local/development builds. But the assumption in kani-rustc is one that we will need to fix when we make a release of Kani.

Fixing the rest might be helpful for e.g. a benchmarking suite.

Metadata

Metadata

Assignees

Labels

[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions