Rules about flexible array members.
In our symbolic execution, the only use of structures with flexible array members is accessing their members; they are never copied, and thus the removal of the flexible array member never happens. In order to simplify away remove-flexible-array-member, we need rules showing that our values being copied do not satisfy remove-flexible-array-member.
Here we prove rules for the non-structure values. For structure values, defstruct generates rules saying that the recognizer implies that the flag is unset; here we provide a rule saying that if the flag is unset then flexible-array-member-p does not hold.
We also include the rule
Theorem:
(defthm not-flexible-array-member-p-when-ucharp (implies (ucharp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-scharp (implies (scharp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ushortp (implies (ushortp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sshortp (implies (sshortp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-uintp (implies (uintp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sintp (implies (sintp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ulongp (implies (ulongp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-slongp (implies (slongp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ullongp (implies (ullongp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sllongp (implies (sllongp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-uchar-arrayp (implies (uchar-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-schar-arrayp (implies (schar-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ushort-arrayp (implies (ushort-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sshort-arrayp (implies (sshort-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-uint-arrayp (implies (uint-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sint-arrayp (implies (sint-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ulong-arrayp (implies (ulong-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-slong-arrayp (implies (slong-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-ullong-arrayp (implies (ullong-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-sllong-arrayp (implies (sllong-arrayp val) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-value-pointer (implies (value-case val :pointer) (not (flexible-array-member-p val))))
Theorem:
(defthm not-flexible-array-member-p-when-value-struct (implies (and (value-case val :struct) (not (value-struct->flexiblep val))) (not (flexible-array-member-p val))))