Extend the example code and assert the result · model-checking/verify-rust-std@2a5af32 (original) (raw)

Original file line number Diff line number Diff line change
@@ -92,21 +92,28 @@ use crate::ub_checks;
92 92 /// ```
93 93 /// use std::slice;
94 94 ///
95 +/// /// Sum the elements of an FFI slice.
96 +/// ///
95 97 /// /// # Safety
96 98 /// ///
97 99 /// /// If ptr is not NULL, it must be correctly aligned and
98 100 /// /// point to `len` initialized items of type `f32`.
99 -/// unsafe extern "C" fn handle_slice(ptr: *const f32, len: usize) {
101 +/// unsafe extern "C" fn sum_slice(ptr: *const f32, len: usize) -> f32 {
100 102 /// let data = if ptr.is_null() {
101 103 /// // `len` is assumed to be 0.
102 104 /// &[]
103 105 /// } else {
104 106 /// // SAFETY: see function docstring.
105 107 /// unsafe { slice::from_raw_parts(ptr, len) }
106 108 /// };
107 -/// dbg!(data);
108 -/// // ...
109 +/// data.sum()
109 110 /// }
111 +///
112 +/// // This could be the result of C++'s std::vector::data():
113 +/// let ptr = std::ptr::null();
114 +/// // And this could be std::vector::size():
115 +/// let len = 0;
116 +/// assert_eq!(unsafe { sum_slice(ptr, len) }, 0.0);
110 117 /// ```
111 118 ///
112 119 /// [valid]: ptr#safety