Function extern_spec_i16_saturating_div 

pub fn extern_spec_i16_saturating_div(self_: i16, rhs: i16) -> i16

extern spec for i16::saturating_div

This is not a real function: its only use is for documentation.

terminates

ghost

requires

rhs@ != 0

ensures

$type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add);
        spec_op_common!($type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub);
        spec_op_common!($type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul);

        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result == -self)]
                fn wrapping_neg(self) -> $type;
            }
        }

        // Specify division separately, because it has the additional precondition that the divisor
        // is non-zero. Overflow on division can only occur on signed types and only when computing
        // `$type::MIN / -1`.
        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns `None` iff the divisor is zero or the division overflows
                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
                // Else, returns the result of the division
                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
                fn checked_div(self, rhs: $type) -> Option<$type>;

                #[allow(dead_code)]
                #[check(ghost)]
                // Panics if the divisor is zero
                #[requires(rhs@ != 0)]
                // Returns `self` if the division overflows
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == self@)]
                // Else, returns the result of the division
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
                fn wrapping_div(self, rhs: $type) -> $type;

                #[allow(dead_code)]
                #[check(ghost)]
                // Panics if the divisor is zero
                #[requires(rhs@ != 0)]
                // Returns `$type::MIN` if the division overflows
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == $type::MIN@

ensures

(self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@