From 9ba66e6fb7b2065a84ab13713a1efe40fd07d16a Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 18:42:41 +0000 Subject: [PATCH] Fix type of function-contracts --- doc/src/tools/kani.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index f0b2fd15ef63e..de900216c088f 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -57,7 +57,7 @@ Here is a short tutorial to get started with using Kani to verify some proofs th Create a local copy of the model-checking fork of the Rust Standard Library. The fork comes with Kani initiated, so all you'll need to do is to call Kani's building-block APIs (such as -`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `proof_for_contract` and `fake_function`) directly. +`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly. For example, insert this module into an existing file like `library/core/src/lib.rs` in your copy of the library. @@ -117,7 +117,7 @@ Complete - 2 successfully verified harnesses, 0 failures, 2 total. ### Running on a specific harness -You can specify a specific harness to be verified using the --harness flag. +You can specify a specific harness to be verified using the `--harness` flag. For example, in your local copy of the verify repo, run the following command. ```