Rules about the composition of integer-from-sint
with
These are not used during the symbolic execution; they are used to prove rules used during the symbolic execution.
Theorem:
(defthm integer-from-sint-of-sint-from-schar (equal (integer-from-sint (sint-from-schar x)) (integer-from-schar x)))
Theorem:
(defthm integer-from-sint-of-sint-from-uchar (equal (integer-from-sint (sint-from-uchar x)) (integer-from-uchar x)))
Theorem:
(defthm integer-from-sint-of-sint-from-sshort (equal (integer-from-sint (sint-from-sshort x)) (integer-from-sshort x)))
Theorem:
(defthm integer-from-sint-of-sint-from-ushort (equal (integer-from-sint (sint-from-ushort x)) (integer-from-ushort x)))