Skip to content

Commit

Permalink
docs: fix typos (rust-lang#1268)
Browse files Browse the repository at this point in the history
* docs: fix typos

* docs: revert UB repetition because it's used in different contexts

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
  • Loading branch information
sanjit-bhat and adpaco-aws authored Jun 9, 2022
1 parent 528b115 commit 217f45a
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 8 deletions.
2 changes: 1 addition & 1 deletion docs/src/cheat-sheets.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# Command cheat sheets

Development work in the Kani project depends on multiple tools. Regardless of
your familiriaty with the project, the commands below may be useful for
your familiarity with the project, the commands below may be useful for
development purposes.

## Kani
Expand Down
2 changes: 1 addition & 1 deletion docs/src/rust-feature-support/unstable.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
In general, unstable Rust features are out of scope and any support
for them available in Kani should be considered unstable as well.

The following are exampels of unstable features that are not supported
The following are examples of unstable features that are not supported
in Kani:
* Generators
* C-variadics
Expand Down
2 changes: 1 addition & 1 deletion docs/src/tutorial/arbitrary-variables/src/inventory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ mod verification {
let quantity: NonZeroU32 = unsafe { kani::any_raw() };

// The assert bellow would fail if we comment it out.
// assert!(id.get() != 0, "NonZeroU32 is internally a u32 but it should never be 0.");
// assert!(quantity.get() != 0, "NonZeroU32 is internally a u32 but it should never be 0.");

// Update the inventory and check the result.
inventory.update(id.clone(), quantity);
Expand Down
9 changes: 4 additions & 5 deletions docs/src/undefined-behaviour.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,14 @@ Rust’s [definition of UB](https://doc.rust-lang.org/reference/behavior-conside

Given the lack of a formal semantics for UB, and given Kani's focus on memory safety, there are classes of UB which Kani does not detect.
A non-exhaustive list of these, based on the the non-exhaustive list from the [Rust documentation](https://doc.rust-lang.org/reference/behavior-considered-undefined.html), is:
A non-exhaustive list of these, based on the non-exhaustive list from the [Rust documentation](https://doc.rust-lang.org/reference/behavior-considered-undefined.html), is:

* Data races.
* Kani focuses on sequential code.
* Breaking the pointer aliasing rules (http://llvm.org/docs/LangRef.html#pointer-aliasing-rules).
* Kani can detect if misuse of pointers causes memory safety or assertion violations, but does not not track reference lifetimes.
* Kani can detect if misuse of pointers causes memory safety or assertion violations, but does not track reference lifetimes.
* Mutating immutable data.
* Kani can detect if modification of immutable data causes memory safety or assertion violations, but does not not track reference lifetimes.
* Kani can detect if modification of immutable data causes memory safety or assertion violations, but does not track reference lifetimes.
* Invoking undefined behavior via compiler intrinsics.
* Kani makes a best effort attempt to check the preconditions of compiler intrinsics, but does not guarantee to do so in all cases.
* Executing code compiled with platform features that the current platform does not support (see [target_feature](https://doc.rust-lang.org/reference/attributes/codegen.html#the-target_feature-attribute)).
Expand All @@ -44,6 +44,5 @@ Kani makes a best-effort attempt to detect some cases of UB:
* Kani can detect invalid dereferences, but may not detect them in [place expression context](https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions).
* Invoking undefined behavior via compiler intrinsics.
* See [current support for compiler intrinsics](./rust-feature-support/intrinsics.md).
* Producing an invalid value, even in private fields and locals.
* Producing an invalid value, even in private fields and locals.
* Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types.

0 comments on commit 217f45a

Please sign in to comment.