Documentation cleanup of UB detected by Kani (#4245)

Cleanup of documentation previously introduced in #1141:

1. No need to repeatedly discuss compiler intrinsics.
2. I am not aware of invalid dereferences that we would _not_ catch,
even place expressions.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

docs/src/undefined-behaviour.md

@@ -19,7 +19,7 @@ Rust’s [definition of UB](https://doc.rust-lang.org/reference/behavior-conside
 > The following list is not exhaustive. There is no formal model of Rust's semantics for what is and is not allowed in unsafe code, so there may be more behavior considered unsafe. The following list is just what we know for sure is undefined behavior. Please read the Rustonomicon (https://doc.rust-lang.org/nomicon/index.html) before writing unsafe code.
 
 
-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.
+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, or only makes a best-effort attempt to detect them.
 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. 
@@ -29,7 +29,7 @@ A non-exhaustive list of these, based on the non-exhaustive list from the [Rust
 * Mutating immutable data.
     * 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.
+    * Kani makes a best effort attempt to check the preconditions of compiler intrinsics, but does not guarantee to do so in all cases. See also [current support for compiler intrinsics](./rust-feature-support/intrinsics.md).
 * 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)).
     * Kani relies on `rustc` to check for this case.
 * Calling a function with the wrong call ABI or unwinding from a function with the wrong unwind ABI.
@@ -40,9 +40,3 @@ A non-exhaustive list of these, based on the non-exhaustive list from the [Rust
     * Kani does not support inline assembly.
 * Using uninitialized memory.
     * See the corresponding section in our [Rust feature support](./rust-feature-support.md#uninitialized-memory).
-
-Kani makes a best-effort attempt to detect some cases of UB:
-* Evaluating a dereference expression (`*expr`) on a raw pointer that is dangling or unaligned.
-    * 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).