Limitations
Like other tools, Kani comes with some limitations. In some cases, these limitations are inherent because of the techniques it's based on. In other cases, it's just a matter of time and effort to remove these limitations (e.g., specific unsupported Rust language features).
In this chapter, we do the following to document these limitations:
- Discuss the effect of Rust undefined behaviour.
- Summarize the current support for Rust features.
- Explain the need for overrides and list all overriden symbols.