Skip to main content

Drop

vstd_extra::drop_tracking

Trait Drop 

Source 
pub trait Drop: TrackDrop {
    // Required method
    exec fn drop(
        self,
        Tracked(s): Tracked<&mut Self::State>,
        Tracked(obl): Tracked<Self::Obligation>,
    );
}

Required Methods§

Source

exec fn drop( self, Tracked(s): Tracked<&mut Self::State>, Tracked(obl): Tracked<Self::Obligation>, )

requires
self.drop_requires(*old(s), obl),
ensures
self.drop_ensures(*old(s), *final(s), obl),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§