Skip to content

Commit

Permalink
Minor updates in README for readability. (model-checking#1018)
Browse files Browse the repository at this point in the history
* Update readme for readability
  • Loading branch information
jaisnan authored and tedinski committed Apr 6, 2022
1 parent 380cead commit 4a40d00
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@
The Kani Rust Verifier is a bit-precise model checker for Rust.

Kani verifies:
* memory safety -- even in unsafe Rust code
* user-specified assertions
* absence of panics
* checks for some classes of undefined behavior
* Memory Safety -- even in unsafe Rust code
* User-specified assertions
* Absence of panics
* Absence of some classes of undefined behavior

## Installation

Expand All @@ -23,10 +23,13 @@ use my_crate::{function_under_test, is_valid, meets_specification};
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);

// Check that it meets the specification
assert!(meets_specification(input, output));
}
Expand Down

0 comments on commit 4a40d00

Please sign in to comment.