		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-c-char

Validate a character of a character constant.

Signature
(valid-c-char cchar prefix? ienv) → (mv erp code)
Arguments: cchar — Guard (c-char-p cchar).; prefix? — Guard (cprefix-optionp prefix?).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; code — Type (natp code).

If validation succeeds, we return the character code.

The grammar [C17:6.4.4.4/1] excludes (direct) character codes for single quote and new-line. For the latter, we check both line feed and carriage return. Note that our lexer normalizes both to line feed, and excludes line feed when lexing c-char; here we make an independent check, but in the future we could make that an invariant in the abstract syntax.

[C17:6.4.4.4/4] says that, based on the (possibly absent) prefix of the character constant of which this character is part, the character code of an octal or hexadecimal escape must fit in unsigned char, or wchar_t, or char16_t, or char32_t. To properly capture the range of the latter three types, we should probably extend our implementation environments with information about which built-in types those types expand to, and then use again the implementation environment to obtain the maximun values of such built-in types. For now, we just use the maximum Unicode code points, i.e. effectively we do not enforce any restriction.

Definitions and Theorems

Function: valid-c-char

(defun valid-c-char (cchar prefix? ienv)
 (declare (xargs :guard (and (c-char-p cchar)
                             (cprefix-optionp prefix?)
                             (ienvp ienv))))
 (b* (((reterr) 0)
      (max (if prefix? 1114111
             (ienv->uchar-max ienv))))
  (c-char-case
   cchar
   :char
   (cond
    ((= cchar.code (char-code #\'))
     (retmsg$
      "Single quote cannot be used directly ~
                            in a character constant."))
    ((= cchar.code 10)
     (retmsg$
      "Line feed cannot be used directly ~
                            in a character constant."))
    ((= cchar.code 13)
     (retmsg$
      "Carriage return cannot be used directly ~
                            in a character constant."))
    ((> cchar.code max)
     (retmsg$
      "The character with code ~x0 ~
                            exceed the maximum ~x1 allowed for ~
                            a character constant with prefix ~x2."
      cchar.code
      max (cprefix-option-fix prefix?)))
    (t (retok cchar.code)))
   :escape (valid-escape cchar.escape max))))

Theorem: maybe-msgp-of-valid-c-char.erp

(defthm maybe-msgp-of-valid-c-char.erp
  (b* (((mv acl2::?erp ?code)
        (valid-c-char cchar prefix? ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: natp-of-valid-c-char.code

(defthm natp-of-valid-c-char.code
  (b* (((mv acl2::?erp ?code)
        (valid-c-char cchar prefix? ienv)))
    (natp code))
  :rule-classes :rewrite)

Theorem: valid-c-char-of-c-char-fix-cchar

(defthm valid-c-char-of-c-char-fix-cchar
  (equal (valid-c-char (c-char-fix cchar)
                       prefix? ienv)
         (valid-c-char cchar prefix? ienv)))

Theorem: valid-c-char-c-char-equiv-congruence-on-cchar

(defthm valid-c-char-c-char-equiv-congruence-on-cchar
  (implies (c-char-equiv cchar cchar-equiv)
           (equal (valid-c-char cchar prefix? ienv)
                  (valid-c-char cchar-equiv prefix? ienv)))
  :rule-classes :congruence)

Theorem: valid-c-char-of-cprefix-option-fix-prefix?

(defthm valid-c-char-of-cprefix-option-fix-prefix?
  (equal (valid-c-char cchar (cprefix-option-fix prefix?)
                       ienv)
         (valid-c-char cchar prefix? ienv)))

Theorem: valid-c-char-cprefix-option-equiv-congruence-on-prefix?

(defthm valid-c-char-cprefix-option-equiv-congruence-on-prefix?
  (implies (cprefix-option-equiv prefix? prefix?-equiv)
           (equal (valid-c-char cchar prefix? ienv)
                  (valid-c-char cchar prefix?-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-c-char-of-ienv-fix-ienv

(defthm valid-c-char-of-ienv-fix-ienv
  (equal (valid-c-char cchar prefix? (ienv-fix ienv))
         (valid-c-char cchar prefix? ienv)))

Theorem: valid-c-char-ienv-equiv-congruence-on-ienv

(defthm valid-c-char-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-c-char cchar prefix? ienv)
                  (valid-c-char cchar prefix? ienv-equiv)))
  :rule-classes :congruence)