		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

General-of-spec-fn

Signature
(general-of-spec-fn result-nbits signed-raw-result) → *

General OF Specification (Source: Intel Manuals, Vol. 1, Section 3.4.3.1):

Overflow flag Set if the integer result is too large a positive number or too small a negative number (excluding the sign-bit) to fit in the destination operand; cleared otherwise. This flag indicates an overflow condition for signed-integer (two s complement) arithmetic.

Definitions and Theorems

Function: general-of-spec-fn

(defun general-of-spec-fn (result-nbits signed-raw-result)
 (declare (xargs :guard (and (natp result-nbits)
                             (integerp signed-raw-result))))
 (let ((__function__ 'general-of-spec-fn))
  (declare (ignorable __function__))
  (bool->bit (not (signed-byte-p result-nbits signed-raw-result)))))

Theorem: n01p-general-of-spec-fn

(defthm n01p-general-of-spec-fn
  (unsigned-byte-p
       1
       (general-of-spec-fn result-nbits signed-raw-result))
  :rule-classes (:rewrite))