		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-cconst

Validate a character constant.

Signature
(valid-cconst cconst) → (mv erp type)
Arguments: cconst — Guard (cconstp cconst).
Returns: type — Type (typep type).

We check the characters that form the constant, with respect to the prefix (if any). If validation is successful, we return the type of the constant. According to [C:6.4.4.4/10], a character constant without prefix has type int. According to [C:6.4.4.4/11], a character constant with a prefix has type wchar_t, char16_t, or char32_t; since for now we do not model these, we return an unknown type in this case.

The types wchar_t, char16_t, and char32_t may vary across implementations. In order to handle these in a general way, we should probably extend our implementation environments with information about which built-in types those types expand to. Once we do that, we will be able to perform a full validation of character constants here.

Definitions and Theorems

Function: valid-cconst

(defun valid-cconst (cconst)
  (declare (xargs :guard (cconstp cconst)))
  (let ((__function__ 'valid-cconst))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-type))
         ((cconst cconst) cconst)
         ((erp &)
          (valid-c-char-list cconst.cchars cconst.prefix?)))
      (if cconst.prefix? (retok (type-unknown))
        (retok (type-sint))))))

Theorem: typep-of-valid-cconst.type

(defthm typep-of-valid-cconst.type
  (b* (((mv acl2::?erp ?type)
        (valid-cconst cconst)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-cconst-of-cconst-fix-cconst

(defthm valid-cconst-of-cconst-fix-cconst
  (equal (valid-cconst (cconst-fix cconst))
         (valid-cconst cconst)))

Theorem: valid-cconst-cconst-equiv-congruence-on-cconst

(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)