3 ms·
How would you prove stuff about your code like memory safety.
by Ygg2 2y ago
How would you prove stuff about your code like memory safety.
- deleted 2y ago[deleted]
- synack 2y agoOut of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well. You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html https://docs.adacore.com/spark2014-docs/html/ug/index.html