Skip to content

Commit

Permalink
Small adjustments to our doc / help (rust-lang#1153)
Browse files Browse the repository at this point in the history
* Remove redundant check from README.md

In the example, we were calling is_valid after `kani::any()` which is
redundant since the type has to implement the Arbitrary type.

* Also adjust Kani help
  • Loading branch information
celinval authored May 4, 2022
1 parent f2d9efb commit 4e43f69
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 5 deletions.
5 changes: 1 addition & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,13 @@ See [the installation guide](https://model-checking.github.io/kani/install-guide
Similar to testing, you write a harness, but with Kani you can check all possible values using `kani::any()`:

```rust
use my_crate::{function_under_test, is_valid, meets_specification};
use my_crate::{function_under_test, meets_specification};

#[kani::proof]
fn check_my_property() {
// Create a nondeterministic input
let input = kani::any();

// Constrain it to represent valid values
kani::assume(is_valid(input));

// Call the function under verification
let output = function_under_test(input);

Expand Down
2 changes: 1 addition & 1 deletion kani-driver/src/args.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ const DEFAULT_OBJECT_BITS: u32 = 16;
#[derive(Debug, StructOpt)]
#[structopt(
name = "kani",
about = "Verify a single Rust file. For more information, see https://github.com/model-checking/kani",
about = "Verify a single Rust crate. For more information, see https://github.com/model-checking/kani",
setting = structopt::clap::AppSettings::AllArgsOverrideSelf
)]
pub struct StandaloneArgs {
Expand Down

0 comments on commit 4e43f69

Please sign in to comment.