generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 134
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.
Description
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.This is a bug. Something isn't working.