Rules about promote-value on values of given types.
These are not used during the symbolic execution; they are used to prove rules used during the symbolic execution.
Theorem:
(defthm promote-value-when-scharp (implies (scharp x) (equal (promote-value x) (sint-from-schar x))))
Theorem:
(defthm promote-value-when-ucharp (implies (ucharp x) (equal (promote-value x) (if (<= (uchar-max) (sint-max)) (sint-from-uchar x) (uint-from-uchar x)))))
Theorem:
(defthm promote-value-when-sshortp (implies (sshortp x) (equal (promote-value x) (sint-from-sshort x))))
Theorem:
(defthm promote-value-when-ushortp (implies (ushortp x) (equal (promote-value x) (if (<= (ushort-max) (sint-max)) (sint-from-ushort x) (uint-from-ushort x)))))
Theorem:
(defthm promote-value-when-sintp (implies (sintp x) (equal (promote-value x) x)))
Theorem:
(defthm promote-value-when-uintp (implies (uintp x) (equal (promote-value x) x)))
Theorem:
(defthm promote-value-when-slongp (implies (slongp x) (equal (promote-value x) x)))
Theorem:
(defthm promote-value-when-ulongp (implies (ulongp x) (equal (promote-value x) x)))
Theorem:
(defthm promote-value-when-sllongp (implies (sllongp x) (equal (promote-value x) x)))
Theorem:
(defthm promote-value-when-ullongp (implies (ullongp x) (equal (promote-value x) x)))