		Search-engine friendly clone of the ACL2 documentation.

Unsigned-saturate

Unsigned-saturate32

Optimized implementation of 32-bit unsigned saturation.

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

Definitions and Theorems

Function: unsigned-saturate32$inline

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