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

    MaintenanceMaintenance related issues for the challange

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions