Attribute Macro pre::extern_crate

#[extern_crate]

Provide preconditions for items in a different crate.

This attribute can be used when a library has documented preconditions without using pre and you want those preconditions to be checked by pre.

It works by specifying an outline of the library as a module. Every function that should have preconditions added is simply referenced by it's signature.

The module then acts as a drop-in replacement for the original library.

Example

use pre::pre;

#[pre::extern_crate(core)]
mod new_core {
    mod mem {
        // Notice that the body of the function is missing.
        // It's behavior is exactly the same as `core::mem::zeroed`.
        #[pre("an all-zero byte-pattern is valid for `T`")]
        unsafe fn zeroed<T>() -> T;

        impl<T> MaybeUninit<T> {
            #[pre("the contained value is an initialized, valid value of `T`")]
            unsafe fn assume_init(self) -> T;
        }
    }
}

#[pre]
fn main() {
    // Note the use of `new_core` instead of `core`.
    use new_core::mem;

    // When using functions from `new_core`, the preconditions applied there are checked, but
    // the behavior is the same as the original function in `core`.
    #[assure(
        "an all-zero byte-pattern is valid for `T`",
        reason = "`usize` supports an all-zero byte-pattern"
    )]
    let x: usize = unsafe { mem::zeroed() };
    assert_eq!(x, 0);

    // Functions and types available in the original library (`core` in this case) are
    // accessible unaltered through the new name `new_core`.
    let mut b = new_core::mem::MaybeUninit::uninit();

    // No preconditions were specified for `new_core::ptr::write` in this example. In a
    // realistic setting, this should be done. Here is just serves as an example that the
    // function is available in `new_core` without being explicitly mentioned.
    unsafe { new_core::ptr::write(b.as_mut_ptr(), true) };

    // The `forward` attribute here is required to find the preconditions for this function.
    #[forward(impl new_core::mem::MaybeUninit)]
    #[assure(
        "the contained value is an initialized, valid value of `T`",
        reason = "the value `true` was just written to `b`"
    )]
    let val = unsafe { b.assume_init() };
    assert_eq!(val, true);
}

Note the use of the forward attribute above. For more information about it and its use, you can read its documentation.

Visibility

Visibility modifiers on inner items of the module are ignored.

Instead it is ensured that inner modules are always visible in any place the topmost module is visible. You can think of every item in the contained module having pub visibility (though in practice it's slightly more complicated).