kani icon indicating copy to clipboard operation
kani copied to clipboard

Published 20 hours ago • verified publisher icon model-checking

Workspaces and Features

Open YoshikiTakashima opened this issue 3 years ago • 2 comments

Requested feature: Ability to deal with --workspaces and Cargo.toml features Use case: Potential customer code (see prost below) contain workspaces. Link to relevant documentation (Rust reference, Nomicon, RFC): https://doc.rust-lang.org/cargo/reference/manifest.html

Test case: https://github.com/informalsystems/prost

YoshikiTakashima avatar Aug 11 '22 19:08 YoshikiTakashima

BTW I'd add the same flags as cargo build

So --workspace and --all-features looks like

tedinski avatar Aug 11 '22 19:08 tedinski

@tedinski Agreed. cargo kani should look very similar to cargo test

YoshikiTakashima avatar Aug 12 '22 00:08 YoshikiTakashima

@tedinski Shall we change these flags in the compiletest to add these flags when running?

YoshikiTakashima avatar Aug 16 '22 18:08 YoshikiTakashima