		Search-engine friendly clone of the ACL2 documentation.

Signed-saturate

Signed-saturate32

Optimized implementation of 32-bit signed saturation.

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

Definitions and Theorems

Function: signed-saturate32$inline

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