|
| 1 | +#![feature(prelude_import)] |
| 2 | +#![feature(register_tool)] |
| 3 | +#![register_tool(Safety)] |
| 4 | +#![allow(clippy::missing_safety_doc, clippy::mut_from_ref, internal_features)] |
| 5 | +#![feature(core_intrinsics)] |
| 6 | +#[prelude_import] |
| 7 | +use std::prelude::rust_2024::*; |
| 8 | +#[macro_use] |
| 9 | +extern crate std; |
| 10 | +use safety_tool_lib::safety; |
| 11 | +/// It's undefined behavior to reach code marked with this intrinsic function. |
| 12 | +#[Safety::inner( |
| 13 | + UnReachable, |
| 14 | + kind = "precond", |
| 15 | + memo = "It's undefined behavior to reach code marked with this intrinsic function." |
| 16 | +)] |
| 17 | +pub unsafe fn test() -> ! { |
| 18 | + unsafe { std::intrinsics::unreachable() } |
| 19 | +} |
| 20 | +pub struct MyStruct { |
| 21 | + ptr: *mut u8, |
| 22 | + len: usize, |
| 23 | +} |
| 24 | +impl MyStruct { |
| 25 | + pub fn from(p: *mut u8, l: usize) -> MyStruct { |
| 26 | + MyStruct { ptr: p, len: l } |
| 27 | + } |
| 28 | + /// The ptr must be initialized first! |
| 29 | + #[Safety::inner( |
| 30 | + Init(self.ptr, u8, self.len), |
| 31 | + kind = "precond", |
| 32 | + memo = "The ptr must be initialized first!" |
| 33 | + )] |
| 34 | + /// The ptr must be within the length. |
| 35 | + #[Safety::inner( |
| 36 | + InBound(self.ptr, u8, self.len), |
| 37 | + kind = "precond", |
| 38 | + memo = "The ptr must be within the length." |
| 39 | + )] |
| 40 | + /// Slice length can't exceed isize::MAX due to allocation limit. |
| 41 | + #[Safety::inner( |
| 42 | + ValidNum(self.len*sizeof(u8), [0, isize::MAX]), |
| 43 | + kind = "precond", |
| 44 | + memo = "Slice length can't exceed isize::MAX due to allocation limit." |
| 45 | + )] |
| 46 | + /// Make sure don't alias the ptr. |
| 47 | + #[Safety::inner( |
| 48 | + Alias(self.ptr), |
| 49 | + kind = "hazard", |
| 50 | + memo = "Make sure don't alias the ptr." |
| 51 | + )] |
| 52 | + pub unsafe fn get(&self) -> &mut [u8] { |
| 53 | + unsafe { std::slice::from_raw_parts_mut(self.ptr, self.len) } |
| 54 | + } |
| 55 | +} |
0 commit comments