Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Celina G. Val <celinval@amazon.com>
  • Loading branch information
jaisnan and celinval authored Jun 12, 2024
1 parent 98d0bef commit 948891f
Showing 1 changed file with 6 additions and 8 deletions.
14 changes: 6 additions & 8 deletions doc/src/intrinsics-memory.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@

- **Status:** Open
- **Tracking Issue:** *Link to issue*
- **Start date:** *YY/MM/DD*
- **End date:** *YY/MM/DD*
- **Start date:** *24/06/12*
- **End date:** *24/12/10*

-------------------

Expand All @@ -21,7 +21,7 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their
5. The verification of each intrinsic should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usage.


### Functions for verification
Intrinsic functions to be annotated with safety contracts

|Function |Location |
|--- |--- |
Expand Down Expand Up @@ -50,7 +50,7 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their



**At least 10 of the following usages of intrinsics were proven safe:**
All the following usages of intrinsics were proven safe:

|Function |Location |
|--- |--- |
Expand All @@ -59,11 +59,10 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their
|swap | core::mem |
|align_of_val | core::mem |
|zeroed | core::mem::maybe_uninit |
| | |



**At least 5 unsafe functions that expose those intrinsics are also annotated with safety contracts, and those contracts are verified:**
Annotate and verify all the functions that below that expose intrinsics with safety contracts

|Function |Location |
|--- |--- |
Expand All @@ -72,7 +71,6 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their
|swap | std::ptr |
|align_of_val | std::ptr |
|zeroed | std::ptr |
| | |



Expand All @@ -83,7 +81,7 @@ All proofs must automatically ensure the absence of the following undefined beha

* Invoking undefined behavior via compiler intrinsics.
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
* Uninitialized memory
* Reading from uninitialized memory except for padding or unions.
* Mutating immutable bytes.
* Producing an invalid value

Expand Down

0 comments on commit 948891f

Please sign in to comment.