Validate a character constant.
[C:6.4.4.4] states a number of requirements, but for now we do not actually impose any requirement, and we just return the type of the character constant.
The requirements have to do with the size of the characters
with respect to the optional prefix of the character constant.
However, those refer to types defined in the standard library,
specifically
The character constant may also have one of those types [C:6.4.4.4/11].
So, for now, we return type
Function:
(defun valid-cconst (cconst) (declare (xargs :guard (cconstp cconst))) (let ((__function__ 'valid-cconst)) (declare (ignorable __function__)) (b* (((cconst cconst) cconst)) (if cconst.prefix? (type-unknown) (type-sint)))))
Theorem:
(defthm typep-of-valid-cconst (b* ((type (valid-cconst cconst))) (typep type)) :rule-classes :rewrite)
Theorem:
(defthm valid-cconst-of-cconst-fix-cconst (equal (valid-cconst (cconst-fix cconst)) (valid-cconst cconst)))
Theorem:
(defthm valid-cconst-cconst-equiv-congruence-on-cconst (implies (cconst-equiv cconst cconst-equiv) (equal (valid-cconst cconst) (valid-cconst cconst-equiv))) :rule-classes :congruence)