Address PR comments

model-checking · Jul 16, 2024 · 9f7ba6a · 9f7ba6a
1 parent 1fab5b1
commit 9f7ba6a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
@@ -17,4 +17,4 @@
  - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
  - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
  - [Inductive data type](./challenges/0005-linked-list.md)
- - [Memory safety of the `btree::node` module](./challenges/0006-btree-node.md)
+ - [Memory safety of BTreeMap's `btree::node` module](./challenges/0006-btree-node.md)
diff --git a/doc/src/challenges/0006-btree-node.md b/doc/src/challenges/0006-btree-node.md
@@ -1,4 +1,4 @@
-# Challenge 4: Towards the memory safety of BTreeMap
+# Challenge 4: Memory safety of BTreeMap's `btree::node` module
 
 - **Status:** Open
 - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
@@ -59,7 +59,7 @@ The verification must be unbounded for functions that are recursive or that cont
 All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
 
 * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
-* Reading from uninitialized memory except for padding or unions.
+* Reading from uninitialized memory.
 * Mutating immutable bytes.
 * Producing an invalid value