forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 57
Open
Description
I found the time of some harnesses exists in ubuntu-latest-results.json/results.json
, but not in dv's UI

Then I noticed the crate is null in results.json
for such harnesses who locate in #[cfg(kani)]
modules. src file
{
"thread_id": 2,
"result": {
"harness": "time::duration_verify::duration_as_nanos_panics",
"is_autoharness": false,
"autoharness_result": null,
"with_contract": false,
"crate": null,
"function": "time::duration::as_nanos",
"function_safeness": null,
"public_target": null,
"file_name": "/home/runner/work/verify-rust-std/verify-rust-std/library/core/src/time.rs",
"n_failed_properties": 1,
"n_total_properties": 25,
"result": "SUCCESSFUL (encountered one or more panics as expected)",
"time": "0.075194955s",
"output": [
"Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime",
" File: \"/home/runner/work/verify-rust-std/verify-rust-std/library/core/src/option.rs\", line 2139, in option::expect_failed"
]
}
},
The culprit is that kani's scan doesn't enable kani cfg in RUST_FLAGS
to incoporate these harnesses in compilation:
verify-rust-std/scripts/kani-std-analysis/std-analysis.sh
Lines 80 to 87 in f66ba41
RUST_FLAGS=( | |
"-Cpanic=abort" | |
"-Zalways-encode-mir" | |
) | |
export RUSTFLAGS="${RUST_FLAGS[@]}" | |
export RUSTC="$KANI_DIR/target/debug/scan" | |
# Compile rust with our extension | |
$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET |
Metadata
Metadata
Assignees
Labels
No labels