Add 'float' note to limitations doc (rust-lang#2050)

Author: tedinski

docs/src/rust-feature-support.md

@@ -54,7 +54,7 @@ Reference | Feature | Support | Notes |
 8.2.18 | Await expressions | No | See [Notes - Concurrency](#concurrency) |
 9 | Patterns | Partial | [#707](https://github.com/model-checking/kani/issues/707) |
 10.1.1 | Boolean type | Yes | |
-10.1.2 | Numeric types | Yes | |
+10.1.2 | Numeric types | Yes | | See [Notes - Floats](#floating-point-operations)
 10.1.3 | Textual types | Yes | |
 10.1.4 | Never type | Yes | |
 10.1.5 | Tuple types | Yes | |
@@ -200,3 +200,15 @@ related to [advanced features](#advanced-features).
 
 Please refer to [Intrinsics](rust-feature-support/intrinsics.md) for information
 on the current support in Kani for Rust compiler intrinsics.
+
+### Floating point operations
+
+Kani supports floating point numbers, but some supported operations on floats are "over-approximated."
+These are the trigonometric functions like `sin` and `cos` and the `sqrt` function as well.
+This means the verifier can raise errors that cannot actually happen when the code is run normally.
+For instance, ([#1342](https://github.com/model-checking/kani/issues/1342)) the `sin`/`cos` functions basically return a nondeterministic value between -1 and 1.
+In other words, they largely ignore their input and give very conservative answers.
+This range certainly includes the "real" value, so proof soundness is still preserved, but it means Kani could raise spurious errors that cannot actually happen.
+This makes Kani unsuitable for verifying some kinds of properties (e.g. precision) about numerical algorithms.
+Proofs that fail because of this problem can sometimes be repaired by introducing "stubs" for these functions that return a more acceptable approximation.
+However, note that the actual behavior of these functions can vary by platform/os/architecture/compiler, so introducing an "overly precise" approximation may introduce unsoundness: actual system behavior may produce different values from the stub's approximation.