tutorial 2.1 and 2.2 updates

docs/src/reference/attributes.md

@@ -60,7 +60,7 @@ For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so t
 
 > **NOTE**: The `#[kani::should_panic]` is only recommended for writing
 > harnesses which complement existing harnesses that don't use the same
-> attribute. In order words, it's only recommended to write *negative harnesses*
+> attribute. In other words, it's only recommended to write *negative harnesses*
 > after having written *positive* harnesses that successfully verify interesting
 > properties about the function under verification.
 

docs/src/tutorial-first-steps.md

@@ -200,17 +200,22 @@ Fortunately, Kani is able to report a coverage metric for each proof harness.
 Try running:
 
 ```
-cargo kani --visualize --harness verify_success
+cargo kani --coverage -Z line-coverage --harness verify_success
 ```
 
-The beginning of the report includes coverage information.
-Clicking through to the file will show fully-covered lines in green.
-Lines not covered by our proof harness will show in red.
+which verifies the harness, then prints coverage information for each line.
+In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage.
 
 Try changing the assumption in the proof harness to `x < 2048`.
 Now the harness won't be testing all possible cases.
-Rerun `cargo kani --visualize`.
-Look at the report: you'll see we no longer have 100% coverage of the function.
+Rerun the command.
+You'll see this line:
+
+```
+src/lib.rs, 24, NONE
+```
+
+which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`.
 
 ## Summary
 

docs/src/tutorial-kinds-of-failure.md

@@ -86,33 +86,23 @@ How does Kani's output change, compared to the unsafe operation?
 <details>
 <summary>Click to see explanation for exercise 1</summary>
 
-Having switched back to the safe indexing operation, Kani reports two failures:
+Having switched back to the safe indexing operation, Kani reports a bounds check failure:
 
 ```
-SUMMARY: 
- ** 2 of 350 failed
+SUMMARY:
+ ** 1 of 343 failed (8 unreachable)
 Failed Checks: index out of bounds: the length is less than or equal to the given index
- File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
-Failed Checks: dereference failure: pointer outside object bounds
- File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
+ File: "src/bounds_check.rs", line 11, in bounds_check::get_wrapped
 
 VERIFICATION:- FAILED
 ```
 
-The first is Rust's runtime bounds checking for the safe indexing operation.
-The second is Kani's check to ensure the pointer operation is actually safe.
-This pattern (two checks for similar issues in safe Rust code) is common to see, and we'll see it again in the next section.
-
-> **NOTE**: While Kani will always be checking for both properties, [in the future the output here may change](https://github.com/model-checking/kani/issues/1349).
-> You might have noticed that the bad pointer dereference can't happen, since the bounds check would panic first.
-> In the future, Kani's output may report only the bounds checking failure in this example.
-
 </details>
 
 <details>
 <summary>Click to see explanation for exercise 2</summary>
 
-Having run `cargo kani --harness bound_check --visualize` and clicked on one of the failures to see a trace, there are three things to immediately notice:
+Having run `cargo kani --harness bound_check --visualize --enable-unstable` and clicked on one of the failures to see a trace, there are three things to immediately notice:
 
 1. This trace is huge. Because the standard library `Vec` is involved, there's a lot going on.
 2. The top of the trace file contains some "trace navigation tips" that might be helpful in navigating the trace.
@@ -126,13 +116,15 @@ In this case, where we just have a couple of `kani::any` values in our proof har
 In this trace we find (and the values you get may be different):
 
 ```
-Step 36: Function bound_check, File src/bounds_check.rs, Line 37
-let size: usize = kani::any();
-size = 2464ul
-
-Step 39: Function bound_check, File src/bounds_check.rs, Line 39
-let index: usize = kani::any();
-index = 2463ul
+Step 523: Function bound_check, File src/bounds_check.rs, Line 37
+<- kani::any::<usize>
+Step 524: Function bound_check, File src/bounds_check.rs, Line 37
+size = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
+...
+Step 537: Function bound_check, File src/bounds_check.rs, Line 39
+<- kani::any::<usize>
+Step 538: Function bound_check, File src/bounds_check.rs, Line 39
+index = 18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)
 ```
 
 You may see different values here, as it depends on the solver's behavior.

docs/src/tutorial-real-code.md

@@ -74,7 +74,7 @@ A first proof will likely start in the following form:
 Running Kani on this simple starting point will help figure out:
 
 1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures.
-2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
+2. Whether you're over-constrained. Check the coverage report using `--coverage -Z line-coverage`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
 3. Whether Kani will support all the Rust features involved.
 4. Whether you've started with a tractable problem.
 (Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.)