Rules for array length operations.
These are not operations in C, as we know, but we have functions in our C semantics for array length. We introduce rules to turn value-array->length into more specific array length functions like uchar-array-length. We also add existing (i.e. proved elsewhere) rules about uchar-array-length and the others being natp.
Theorem:
(defthm value-array->length-when-uchar-arrayp (implies (uchar-arrayp x) (equal (value-array->length x) (uchar-array-length x))))
Theorem:
(defthm value-array->length-when-schar-arrayp (implies (schar-arrayp x) (equal (value-array->length x) (schar-array-length x))))
Theorem:
(defthm value-array->length-when-ushort-arrayp (implies (ushort-arrayp x) (equal (value-array->length x) (ushort-array-length x))))
Theorem:
(defthm value-array->length-when-sshort-arrayp (implies (sshort-arrayp x) (equal (value-array->length x) (sshort-array-length x))))
Theorem:
(defthm value-array->length-when-uint-arrayp (implies (uint-arrayp x) (equal (value-array->length x) (uint-array-length x))))
Theorem:
(defthm value-array->length-when-sint-arrayp (implies (sint-arrayp x) (equal (value-array->length x) (sint-array-length x))))
Theorem:
(defthm value-array->length-when-ulong-arrayp (implies (ulong-arrayp x) (equal (value-array->length x) (ulong-array-length x))))
Theorem:
(defthm value-array->length-when-slong-arrayp (implies (slong-arrayp x) (equal (value-array->length x) (slong-array-length x))))
Theorem:
(defthm value-array->length-when-ullong-arrayp (implies (ullong-arrayp x) (equal (value-array->length x) (ullong-array-length x))))
Theorem:
(defthm value-array->length-when-sllong-arrayp (implies (sllong-arrayp x) (equal (value-array->length x) (sllong-array-length x))))