Struct CheckedU16 

pub struct CheckedU16 { /* private fields */ }

This struct represents a $uty value that can overflow. The i field is a ghost value that represents the true value, while the v field is None when the value has overflowed and Some(x) when the value x fits in a $uty.

Implementations

impl CheckedU16

pub fn new(v: u16) -> Self

Creates a new $cty instance from a $uty value. Ensures the internal representation matches the provided value.

pub fn new_overflowed(verus_tmp_i: Ghost<int>) -> Self

Creates a new $cty instance with an overflowed value. Requires the provided value to be greater than $uty::MAX. Ensures the internal representation matches the provided value.

pub fn is_overflowed(&self) -> bool

Checks if the $cty instance is overflowed. Returns true if the value is greater than $uty::MAX.

pub fn unwrap(&self) -> u16

Unwraps the $cty instance to get the $uty value. Requires the instance to not be overflowed. Ensures the returned value matches the internal representation.

pub fn to_option(&self) -> Option<u16>

Converts the $cty instance to an Option<$uty>. Ensures the returned option matches the internal representation.

pub fn add_value(&self, v2: u16) -> Self

Adds a $uty value to the $cty instance. Ensures the resulting value matches the sum of the internal representation and the provided value.

pub fn add_checked(&self, v2: &CheckedU16) -> Self

Adds another $cty instance to the current instance. Ensures the resulting value matches the sum of the internal representations of both instances.

pub fn mul_value(&self, v2: u16) -> Self

Multiplies the $cty instance by a $uty value. Ensures the resulting value matches the product of the internal representation and the provided value.

pub fn mul_checked(&self, v2: &Self) -> Self

Multiplies the $cty instance by another $cty instance. Ensures the resulting value matches the product of the internal representations of both instances.

Trait Implementations

impl Clone for CheckedU16

fn clone(&self) -> Self

Clones the $cty instance. Ensures the cloned instance has the same value as the original.

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

Performs copy-assignment from source.

impl View for CheckedU16

The view of an $cty instance is the true value of the instance.

type V = nat