Struct vstd::arithmetic::overflow::CheckedU32

source ·

pub struct CheckedU32 { /* private fields */ }

Expand description

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§

source §

impl CheckedU32

source

pub closed spec fn spec_new(v: u32) -> CheckedU32

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

source

pub exec fn new(v: u32) -> result : Self

ensures

result@ == v,

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

source

pub exec fn new_overflowed(Ghost(i): Ghost<int>) -> result : Self

requires

i > u32::MAX,

ensures

result@ == i,

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.

source

pub open spec fn spec_is_overflowed(&self) -> bool

{ self@ > u32::MAX }

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

source

pub exec fn is_overflowed(&self) -> result : bool

ensures

result == self.spec_is_overflowed(),

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

source

pub exec fn unwrap(&self) -> result : u32

requires

!self.is_overflowed(),

ensures

result == self@,

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

source

pub exec fn to_option(&self) -> result : Option<u32>

ensures

match result {
    Some(v) => self@ == v && v <= u32::MAX,
    None => self@ > u32::MAX,
},

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

source

pub exec fn add_value(&self, v2: u32) -> result : Self

ensures

result@ == self@ + v2,

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

source

pub exec fn add_checked(&self, v2: &CheckedU32) -> result : Self

ensures

result@ == self@ + v2@,

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

source

pub exec fn mul_value(&self, v2: u32) -> result : Self

ensures

result@ == self@ as int * v2 as int,

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

source

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

ensures

result@ == self@ as int * v2@ as int,

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