		Search-engine friendly clone of the ACL2 documentation.

Signed-saturate

Signed-saturate8

Optimized implementation of 8-bit signed saturation.

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

Definitions and Theorems

Function: signed-saturate8$inline

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