		Search-engine friendly clone of the ACL2 documentation.

Unsigned-saturate

Unsigned-saturate8

Optimized implementation of 8-bit unsigned saturation.

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

Definitions and Theorems

Function: unsigned-saturate8$inline

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