Skip to main content

Drop

vstd_extra::drop_tracking

Trait Drop 

Source 
pub trait Drop: TrackDrop {
    // Required method
    exec fn drop(
        self,
        verus_tmp_s: Tracked<&mut Self::State>,
        verus_tmp_obl: Tracked<DropObligation<Self::Key>>,
    );
}

Required Methods§

Source

exec fn drop( self, verus_tmp_s: Tracked<&mut Self::State>, verus_tmp_obl: Tracked<DropObligation<Self::Key>>, )

requires
self.consume_requires(*old(s), obl.value()),
self.drop_requires(*old(s)),
obl.value() == self.key(),
ensures
self.drop_ensures(*old(s), *final(s), obl.value()),

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§