Update Unwind documentation (model-checking#1087)

* update unwind documentation Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
celinval · Apr 21, 2022 · 625298b · 625298b
1 parent 23472fc
commit 625298b
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 1 deletion.
diff --git a/docs/src/cargo-kani.md b/docs/src/cargo-kani.md
@@ -24,5 +24,5 @@ You can achieve this by adding the following lines to the package's `Cargo.toml`
 
 ```toml
 [package.metadata.kani]
-flags = { unwind = "5" }
+flags = { default-unwind = "5" }
 ```
diff --git a/docs/src/tutorial-loop-unwinding.md b/docs/src/tutorial-loop-unwinding.md
@@ -79,5 +79,28 @@ Failed Checks: dereference failure: pointer outside object bounds
 
 Kani is now sure we've unwound the loop enough to verify our proof harness, and now we're seeing just the bound checking failures from the off-by-one error.
 
+## Unwinding value specification
+
+Kani allows three options to specify the unwind value for a particular harness:
+
+1. The unwind annotation `#[kani::unwind(<num>)]`. This sets the unwind value for the harness with the annotation. Example -
+``` rust,noplaypen
+#[kani::proof]
+#[kani::unwind(3)]
+fn proof_harness() {
+[...]
+}
+```
+2. `--default-unwind` flag. This sets the global or default unwind value for the entire file/crate on which kani or cargo-kani is called. Example -
+```
+kani file.rs --default-unwind 3
+```
+3. `--unwind` flag. This overrides any annotation and forces the harness to use the specified value. This needs to be used alongside `--harness` and sets the unwind value for the harness specified. Example -
+```
+kani file.rs --unwind 2 --harness proof_harness
+```
+
+### Exercises -
+
 1. Exercise: Fix the off-by-one bounds error and get Kani to verify successfully.
 2. Exercise: After fixing the error, `--default-unwind 11` works. Why?