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