		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Value-integer->get

Turn a C integer value into a mathematical (i.e. ACL2) integer.

Signature
(value-integer->get val) → int
Arguments: val — Guard (valuep val).
Returns: int — Type (integerp int).

Definitions and Theorems

Function: value-integer->get

(defun value-integer->get (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (value-integerp val)))
  (let ((__function__ 'value-integer->get))
    (declare (ignorable __function__))
    (value-case val
                :uchar val.get
                :schar val.get
                :ushort val.get
                :sshort val.get
                :uint val.get
                :sint val.get
                :ulong val.get
                :slong val.get
                :ullong val.get
                :sllong val.get
                :pointer (ifix (impossible))
                :array (ifix (impossible))
                :struct (ifix (impossible)))))

Theorem: integerp-of-value-integer->get

(defthm integerp-of-value-integer->get
  (b* ((int (value-integer->get val)))
    (integerp int))
  :rule-classes :rewrite)

Theorem: value-integer->get-bounds

(defthm value-integer->get-bounds
  (and (<= (integer-type-min (type-of-value val))
           (value-integer->get val))
       (<= (value-integer->get val)
           (integer-type-max (type-of-value val))))
  :rule-classes
  ((:linear :trigger-terms ((value-integer->get val)))))

Theorem: value-integer->get-of-value-fix-val

(defthm value-integer->get-of-value-fix-val
  (equal (value-integer->get (value-fix val))
         (value-integer->get val)))

Theorem: value-integer->get-value-equiv-congruence-on-val

(defthm value-integer->get-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (value-integer->get val)
                  (value-integer->get val-equiv)))
  :rule-classes :congruence)