From 6d45f4659aa9f7aba42ae8ecc906abf6c581ccc3 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 11 Jun 2024 21:01:31 +0000 Subject: [PATCH] Remove empty sections --- doc/src/intrinsics-memory.md | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/doc/src/intrinsics-memory.md b/doc/src/intrinsics-memory.md index 3fbc65bb95c54..49e44e7329acb 100644 --- a/doc/src/intrinsics-memory.md +++ b/doc/src/intrinsics-memory.md @@ -12,18 +12,6 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract and verify their usage in the standard library are in fact safe. -## Motivation - -*Explain why this is a challenge that should be prioritized. Consider using a motivating example.* - -## Description - -*Describe the challenge in more details.* - -### Assumptions - -*Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".* - ### Success Criteria* 1. All the following intrinsic functions must be annotated with safety contracts. @@ -102,5 +90,3 @@ All proofs must automatically ensure the absence of the following undefined beha 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. - -[^challenge_id]: The number of the challenge sorted by publication date.