search

model-checking / verify-rust-std

Verifying the Rust standard library
https://model-checking.github.io/verify-rust-std/
Other
18 stars 16 forks source link

Tracking issue for verifying the memory safety of the `alloc::collections::btree::node` module #25

Closed zhassan-aws closed 4 weeks ago

zhassan-aws commented 3 months ago

This module is used in implementing the BTreeMap collection and it contains a lot of unsafe code:

https://github.com/rust-lang/rust/blob/fda509e817abeeecb5b76bc1de844f355675c81e/library/alloc/src/collections/btree/node.rs

Link to challenge: https://model-checking.github.io/verify-rust-std/challenges/0004-btree-node.html

EDIT: link to challenge PR: https://github.com/model-checking/verify-rust-std/pull/26

jaisnan commented 3 months ago

Tracking issues should have links to the challenges they're tracking.

  1. In case, they're already added to the book, I am linking them to the issues.
  2. If not, can we add the links to the challenges to the issue description once the PR for that challenge has been merged?
zhassan-aws commented 3 months ago

Added a link to the challenge PR in the description.