Enum OverflowMode 

pub enum OverflowMode {
    Panic,
    UB,
    Wrap,
}

Variants

Panic

If this operation overflows, it panics. Only exists in debug mode, for instance in a + b, and only if --reconstruct-fallible-operations is passed to Charon. Otherwise the bound check will be explicit.

UB

If this operation overflows, it is UB; for instance in core::num::unchecked_add. This can exists in safe code, but will always be preceded by a bounds check.

Wrap

If this operation overflows, it wraps around for instance in core::num::wrapping_add, or a + b in release mode.

Trait Implementations

impl AstVisitable for OverflowMode

where OverflowMode: PartialEq,

fn drive<V: VisitAst>(&self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_mut<V: VisitAstMut>(&mut self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn drive_two<V: ZipAst>(&self, other: &Self, v: &mut V) -> ControlFlow<V::Break>

Recursively visit this type with the provided visitor. This calls the visitor’s visit_$any method if it exists, otherwise visit_inner.

fn name(&self) -> &'static str

The name of the type, used for debug logging.

fn dyn_visit<T: AstVisitable>(&self, f: impl FnMut(&T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

fn dyn_visit_mut<T: AstVisitable>(&mut self, f: impl FnMut(&mut T))

where Self: Sized,

Visit all occurrences of that type inside self, in pre-order traversal.

impl Clone for OverflowMode

fn clone(&self) -> OverflowMode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for OverflowMode

impl Debug for OverflowMode

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for OverflowMode

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for OverflowMode

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

Formats the value using the given formatter.

impl Eq for OverflowMode

impl PartialEq for OverflowMode

fn eq(&self, other: &OverflowMode) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for OverflowMode

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for OverflowMode