Enum DropKind 

pub enum DropKind {
    Precise,
    Conditional,
}

A Drop statement/terminator can mean two things, depending on what MIR phase we retrieved from rustc: it could be a real drop, or it could be a “conditional drop”, which is where drop may happen depending on whether the borrow-checker determines a drop is needed.

Variants

Precise

A real drop. This calls <T as Destruct>::drop_in_place(&raw mut place) and marks the place as moved-out-of. Use --desugar-drops to transform all such drops to an actual function call.

The drop_in_place method is added by Charon to the Destruct trait to make it possible to track drop code in polymorphic code. It contains the same code as the core::ptr::drop_in_place<T> builtin would.

Drop are precise in MIR elaborated and optimized.

Conditional

A conditional drop, which may or may not end up running drop code depending on the code path that led to it. A conditional drop may also become a partial drop (dropping only the subplaces that haven’t been moved out of), may be conditional on the code path that led to it, or become an async drop. The exact semantics are left intentionally unspecified by rustc developers. To elaborate such drops into precise drops, pass --precise-drops to Charon.

A conditional drop may also be passed an unaligned place when dropping fields of packed structs. Such a thing is UB for a precise drop.

Drop are conditional in MIR built and promoted.

Trait Implementations

impl Clone for DropKind

fn clone(&self) -> DropKind

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for DropKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for DropKind

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<'s, V> Drive<'s, V> for DropKind

where V: Visitor,

fn drive_inner(&'s self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl<'s, V> DriveMut<'s, V> for DropKind

where V: Visitor,

fn drive_inner_mut(&'s mut self, visitor: &mut V) -> ControlFlow<V::Break>

Call v.visit() on the immediate contents of self.

impl Serialize for DropKind

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Copy for DropKind