Skip to content

Kani scanner fails to detect harnesses that are gated behind #[cfg(kani)] #463

@zjp-CN

Description

@zjp-CN

I found the time of some harnesses exists in ubuntu-latest-results.json/results.json, but not in dv's UI

Image

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:

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

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions