Rules about pointed-to integers.
Theorem:
(defthm schar-read-when-scharp (implies (scharp x) (equal (schar-read x) x)))
Theorem:
(defthm uchar-read-when-ucharp (implies (ucharp x) (equal (uchar-read x) x)))
Theorem:
(defthm sshort-read-when-sshortp (implies (sshortp x) (equal (sshort-read x) x)))
Theorem:
(defthm ushort-read-when-ushortp (implies (ushortp x) (equal (ushort-read x) x)))
Theorem:
(defthm sint-read-when-sintp (implies (sintp x) (equal (sint-read x) x)))
Theorem:
(defthm uint-read-when-uintp (implies (uintp x) (equal (uint-read x) x)))
Theorem:
(defthm slong-read-when-slongp (implies (slongp x) (equal (slong-read x) x)))
Theorem:
(defthm ulong-read-when-ulongp (implies (ulongp x) (equal (ulong-read x) x)))
Theorem:
(defthm sllong-read-when-sllongp (implies (sllongp x) (equal (sllong-read x) x)))
Theorem:
(defthm ullong-read-when-ullongp (implies (ullongp x) (equal (ullong-read x) x)))
Theorem:
(defthm schar-write-when-scharp (implies (scharp x) (equal (schar-write x) x)))
Theorem:
(defthm uchar-write-when-ucharp (implies (ucharp x) (equal (uchar-write x) x)))
Theorem:
(defthm sshort-write-when-sshortp (implies (sshortp x) (equal (sshort-write x) x)))
Theorem:
(defthm ushort-write-when-ushortp (implies (ushortp x) (equal (ushort-write x) x)))
Theorem:
(defthm sint-write-when-sintp (implies (sintp x) (equal (sint-write x) x)))
Theorem:
(defthm uint-write-when-uintp (implies (uintp x) (equal (uint-write x) x)))
Theorem:
(defthm slong-write-when-slongp (implies (slongp x) (equal (slong-write x) x)))
Theorem:
(defthm ulong-write-when-ulongp (implies (ulongp x) (equal (ulong-write x) x)))
Theorem:
(defthm sllong-write-when-sllongp (implies (sllongp x) (equal (sllong-write x) x)))
Theorem:
(defthm ullong-write-when-ullongp (implies (ullongp x) (equal (ullong-write x) x)))