Skip to content

Concrete playback requires nightly rustc #1609

@celinval

Description

@celinval

I tried the following:

$ cargo init dummy
$ cd dummy
$ cargo --version
cargo 1.63.0 (fd9c4297c 2022-07-01)

I added the following line to Cargo.toml

[dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }

I opened src/main.rs

#[kani::proof]
fn force_failure() {
  assert!(kani::any());
}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback
cargo test

with Kani version: 0.9.0

I expected to see this happen: Cargo runs the new test and fail.

Instead, this happened: Cargo failed to build kani library with the following error:

error[E0554]: `#![feature]` may not be used on the stable release channel
 --> ~/.cargo/git/checkouts/kani-0ce0dacf5e98886d/281d0bb/library/kani/src/lib.rs:5:1
  |
5 | #![feature(rustc_attrs)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^

Metadata

Metadata

Assignees

Labels

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

Type

No type

Projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions