Attribute Macro erasure 

#[erasure]

Check that the annotated function erases to another function.

See the guide: Erasure check.

Usage

#[erasure(f)]
fn g(x: usize, i: Ghost<Int>) { /* ... */ }

#[erasure(private crate_name::full::path::to::f2)]
fn g2(y: bool) { /* ... */ }

#[trusted]
#[erasure(_)]
fn split<T, U>(g: Ghost<(T, U)>) -> (Ghost<T>, Ghost<U>) {
    /* ... */
}

Inside extern_spec!

The shorter #[erasure] (without argument) can be used in extern_spec! to check that the annotated function body matches the original one.

extern_spec! {
  #[erasure]
  fn some_external_function() { /* ... */ }
}