		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-iconst

Check an integer constant.

Signature
(check-iconst ic) → type
Arguments: ic — Guard (iconstp ic).
Returns: type — Type (type-resultp type).

This is according to [C:6.4.4.1/5]: based on the suffixes and the base, we find the first type that suffices to represent the value, in the lists indicated in the table, and we return that type. If the value is too large, the integer constant is illegal.

This is the static counterpart of eval-iconst.

Definitions and Theorems

Function: check-iconst

(defun check-iconst (ic)
 (declare (xargs :guard (iconstp ic)))
 (let ((__function__ 'check-iconst))
  (declare (ignorable __function__))
  (b* ((ic (iconst-fix ic)) ((iconst ic) ic))
   (if ic.unsignedp
    (iconst-length-case
         ic.length
         :none (cond ((uint-integerp ic.value) (type-uint))
                     ((ulong-integerp ic.value) (type-ulong))
                     ((ullong-integerp ic.value)
                      (type-ullong))
                     (t (reserrf (list :iconst-out-of-range ic))))
         :long (cond ((ulong-integerp ic.value) (type-ulong))
                     ((ullong-integerp ic.value)
                      (type-ullong))
                     (t (reserrf (list :iconst-out-of-range ic))))
         :llong (cond ((ullong-integerp ic.value)
                       (type-ullong))
                      (t (reserrf (list :iconst-out-of-range ic)))))
    (iconst-length-case
         ic.length :none
         (if (iconst-base-case ic.base :dec)
             (cond ((sint-integerp ic.value) (type-sint))
                   ((slong-integerp ic.value) (type-slong))
                   ((sllong-integerp ic.value)
                    (type-sllong))
                   (t (reserrf (list :iconst-out-of-range ic))))
           (cond ((sint-integerp ic.value) (type-sint))
                 ((uint-integerp ic.value) (type-uint))
                 ((slong-integerp ic.value) (type-slong))
                 ((ulong-integerp ic.value) (type-ulong))
                 ((sllong-integerp ic.value)
                  (type-sllong))
                 ((ullong-integerp ic.value)
                  (type-ullong))
                 (t (reserrf (list :iconst-out-of-range ic)))))
         :long
         (if (iconst-base-case ic.base :dec)
             (cond ((slong-integerp ic.value) (type-slong))
                   ((sllong-integerp ic.value)
                    (type-sllong))
                   (t (reserrf (list :iconst-out-of-range ic))))
           (cond ((slong-integerp ic.value) (type-slong))
                 ((ulong-integerp ic.value) (type-ulong))
                 ((sllong-integerp ic.value)
                  (type-sllong))
                 ((ullong-integerp ic.value)
                  (type-ullong))
                 (t (reserrf (list :iconst-out-of-range ic)))))
         :llong
         (if (iconst-base-case ic.base :dec)
             (cond ((sllong-integerp ic.value)
                    (type-sllong))
                   (t (reserrf (list :iconst-out-of-range ic))))
           (cond ((sllong-integerp ic.value)
                  (type-sllong))
                 ((ullong-integerp ic.value)
                  (type-ullong))
                 (t (reserrf (list :iconst-out-of-range ic))))))))))

Theorem: type-resultp-of-check-iconst

(defthm type-resultp-of-check-iconst
  (b* ((type (check-iconst ic)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-iconst-of-iconst-fix-ic

(defthm check-iconst-of-iconst-fix-ic
  (equal (check-iconst (iconst-fix ic))
         (check-iconst ic)))

Theorem: check-iconst-iconst-equiv-congruence-on-ic

(defthm check-iconst-iconst-equiv-congruence-on-ic
  (implies (iconst-equiv ic ic-equiv)
           (equal (check-iconst ic)
                  (check-iconst ic-equiv)))
  :rule-classes :congruence)