		Search-engine friendly clone of the ACL2 documentation.

Unsigned-saturate

Unsigned-saturate16

Optimized implementation of 16-bit unsigned saturation.

Signature
(unsigned-saturate16 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: unsigned-saturate16$inline

(defun unsigned-saturate16$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'unsigned-saturate16))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-saturate-fn 16 x)
         :exec (cond ((>= x 65535) 65535)
                     ((<= x 0) 0)
                     (t x)))))