Rules about convert-integer-value.
These turn calls of convert-integer-value
into calls of
These are not used during the symbolic execution; they are used to prove rules used during the symbolic execution.
Theorem:
(defthm convert-integer-value-of-schar-and-sint (implies (and (scharp val) (equal type (type-sint))) (equal (convert-integer-value val type) (sint-from-schar val))))
Theorem:
(defthm convert-integer-value-of-schar-and-slong (implies (and (scharp val) (equal type (type-slong))) (equal (convert-integer-value val type) (slong-from-schar val))))
Theorem:
(defthm convert-integer-value-of-schar-and-sllong (implies (and (scharp val) (equal type (type-sllong))) (equal (convert-integer-value val type) (sllong-from-schar val))))
Theorem:
(defthm convert-integer-value-of-schar-and-uint (implies (and (scharp val) (equal type (type-uint))) (equal (convert-integer-value val type) (uint-from-schar val))))
Theorem:
(defthm convert-integer-value-of-schar-and-ulong (implies (and (scharp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-schar val))))
Theorem:
(defthm convert-integer-value-of-schar-and-ullong (implies (and (scharp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-schar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-sint (implies (and (ucharp val) (equal type (type-sint)) (<= (uchar-max) (sint-max))) (equal (convert-integer-value val type) (sint-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-slong (implies (and (ucharp val) (equal type (type-slong)) (<= (uchar-max) (slong-max))) (equal (convert-integer-value val type) (slong-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-sllong (implies (and (ucharp val) (equal type (type-sllong)) (<= (uchar-max) (sllong-max))) (equal (convert-integer-value val type) (sllong-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-uint (implies (and (ucharp val) (equal type (type-uint))) (equal (convert-integer-value val type) (uint-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-ulong (implies (and (ucharp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-uchar-and-ullong (implies (and (ucharp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-uchar val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-sint (implies (and (sshortp val) (equal type (type-sint))) (equal (convert-integer-value val type) (sint-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-slong (implies (and (sshortp val) (equal type (type-slong))) (equal (convert-integer-value val type) (slong-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-sllong (implies (and (sshortp val) (equal type (type-sllong))) (equal (convert-integer-value val type) (sllong-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-uint (implies (and (sshortp val) (equal type (type-uint))) (equal (convert-integer-value val type) (uint-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-ulong (implies (and (sshortp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-sshort-and-ullong (implies (and (sshortp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-sshort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-sint (implies (and (ushortp val) (equal type (type-sint)) (<= (ushort-max) (sint-max))) (equal (convert-integer-value val type) (sint-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-slong (implies (and (ushortp val) (equal type (type-slong)) (<= (ushort-max) (slong-max))) (equal (convert-integer-value val type) (slong-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-sllong (implies (and (ushortp val) (equal type (type-sllong)) (<= (ushort-max) (sllong-max))) (equal (convert-integer-value val type) (sllong-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-uint (implies (and (ushortp val) (equal type (type-uint))) (equal (convert-integer-value val type) (uint-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-ulong (implies (and (ushortp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-ushort-and-ullong (implies (and (ushortp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-ushort val))))
Theorem:
(defthm convert-integer-value-of-sint-and-sint (implies (and (sintp val) (equal type (type-sint))) (equal (convert-integer-value val type) val)))
Theorem:
(defthm convert-integer-value-of-sint-and-slong (implies (and (sintp val) (equal type (type-slong))) (equal (convert-integer-value val type) (slong-from-sint val))))
Theorem:
(defthm convert-integer-value-of-sint-and-sllong (implies (and (sintp val) (equal type (type-sllong))) (equal (convert-integer-value val type) (sllong-from-sint val))))
Theorem:
(defthm convert-integer-value-of-sint-and-uint (implies (and (sintp val) (equal type (type-uint))) (equal (convert-integer-value val type) (uint-from-sint val))))
Theorem:
(defthm convert-integer-value-of-sint-and-ulong (implies (and (sintp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-sint val))))
Theorem:
(defthm convert-integer-value-of-sint-and-ullong (implies (and (sintp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-sint val))))
Theorem:
(defthm convert-integer-value-of-uint-and-uint (implies (and (uintp val) (equal type (type-uint))) (equal (convert-integer-value val type) val)))
Theorem:
(defthm convert-integer-value-of-uint-and-slong (implies (and (uintp val) (equal type (type-slong)) (<= (uint-max) (slong-max))) (equal (convert-integer-value val type) (slong-from-uint val))))
Theorem:
(defthm convert-integer-value-of-uint-and-sllong (implies (and (uintp val) (equal type (type-sllong)) (<= (uint-max) (sllong-max))) (equal (convert-integer-value val type) (sllong-from-uint val))))
Theorem:
(defthm convert-integer-value-of-uint-and-ulong (implies (and (uintp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-uint val))))
Theorem:
(defthm convert-integer-value-of-uint-and-ullong (implies (and (uintp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-uint val))))
Theorem:
(defthm convert-integer-value-of-slong-and-slong (implies (and (slongp val) (equal type (type-slong))) (equal (convert-integer-value val type) val)))
Theorem:
(defthm convert-integer-value-of-slong-and-sllong (implies (and (slongp val) (equal type (type-sllong))) (equal (convert-integer-value val type) (sllong-from-slong val))))
Theorem:
(defthm convert-integer-value-of-slong-and-ulong (implies (and (slongp val) (equal type (type-ulong))) (equal (convert-integer-value val type) (ulong-from-slong val))))
Theorem:
(defthm convert-integer-value-of-slong-and-ullong (implies (and (slongp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-slong val))))
Theorem:
(defthm convert-integer-value-of-ulong-and-ulong (implies (and (ulongp val) (equal type (type-ulong))) (equal (convert-integer-value val type) val)))
Theorem:
(defthm convert-integer-value-of-ulong-and-sllong (implies (and (ulongp val) (equal type (type-sllong)) (<= (ulong-max) (sllong-max))) (equal (convert-integer-value val type) (sllong-from-ulong val))))
Theorem:
(defthm convert-integer-value-of-ulong-and-ullong (implies (and (ulongp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-ulong val))))
Theorem:
(defthm convert-integer-value-of-sllong-and-sllong (implies (and (sllongp val) (equal type (type-sllong))) (equal (convert-integer-value val type) val)))
Theorem:
(defthm convert-integer-value-of-sllong-and-ullong (implies (and (sllongp val) (equal type (type-ullong))) (equal (convert-integer-value val type) (ullong-from-sllong val))))
Theorem:
(defthm convert-integer-value-of-ullong-and-ullong (implies (and (ullongp val) (equal type (type-ullong))) (equal (convert-integer-value val type) val)))