diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md index 4136c03e8e737..f8cecac019995 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -63,6 +63,15 @@ and that they maintain the overall safety invariant of `CStr` when called correc | `from_bytes_with_nul_uncheked` | `core::ffi::c_str` | | `strlen` | `core::ffi::c_str` | +4. Verify that the following trait implementations for the `CStr` type are safe: + + +| Trait | Implementation Location | +|-------------------------------------|-------------------------| +| `CloneToUninit` [^unsafe-fn] | `core::clone` | +| `ops::Index>` | `core::ffi::c_str` | + +[^unsafe-fn]: Unsafe functions will require safety contracts. All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): @@ -71,5 +80,5 @@ All proofs must automatically ensure the absence of the following undefined beha - Mutating immutable bytes. - Accessing uninitialized memory. -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](general-rules.md) -in addition to the ones listed above. +Note: All solutions to verification challenges need to satisfy the criteria established in the +[challenge book](../general-rules.md) in addition to the ones listed above. diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md index 474b1d089c6ee..5e7b054ed6891 100644 --- a/doc/src/tool_template.md +++ b/doc/src/tool_template.md @@ -20,9 +20,9 @@ _Please list the license(s) that are used by your tool, and if to your knowledge ## Steps to Use the Tool -1. [First Step] -2. [Second Step] -3. [and so on...] +1. \[First Step\] +2. \[Second Step\] +3. \[and so on...\] ## Artifacts _If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._