		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-cconst

Validate a character constant.

Signature
(valid-cconst cconst ienv) → (mv erp type)
Arguments: cconst — Guard (cconstp cconst).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; 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 [C17:6.4.4.4/10], a character constant without prefix has type int. According to [C17: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 ienv)
  (declare (xargs :guard (and (cconstp cconst) (ienvp ienv))))
  (let ((__function__ 'valid-cconst))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-type))
         ((cconst cconst) cconst)
         ((erp &)
          (valid-c-char-list cconst.cchars cconst.prefix? ienv)))
      (if cconst.prefix? (retok (type-unknown))
        (retok (type-sint))))))

Theorem: maybe-msgp-of-valid-cconst.erp

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

Theorem: typep-of-valid-cconst.type

(defthm typep-of-valid-cconst.type
  (b* (((mv acl2::?erp ?type)
        (valid-cconst cconst ienv)))
    (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) ienv)
         (valid-cconst cconst ienv)))

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 ienv)
                  (valid-cconst cconst-equiv ienv)))
  :rule-classes :congruence)

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

(defthm valid-cconst-of-ienv-fix-ienv
  (equal (valid-cconst cconst (c::ienv-fix ienv))
         (valid-cconst cconst ienv)))

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

(defthm valid-cconst-ienv-equiv-congruence-on-ienv
  (implies (c::ienv-equiv ienv ienv-equiv)
           (equal (valid-cconst cconst ienv)
                  (valid-cconst cconst ienv-equiv)))
  :rule-classes :congruence)