		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-oct-escape

Validate an octal escape.

Signature
(valid-oct-escape esc max) → (mv erp code)
Arguments: esc — Guard (oct-escapep esc).; max — Guard (natp max).
Returns: code — Type (natp code).

[C:6.4.4.4/9] states restrictions on the numeric value of an octal escape used in a character constant, based on the prefix of the character constant; similarly restrictions apply to octal escapes in string literals [C:6.4.5/4]. This ACL2 function is used to check both octal escapes in character constants and octal escapes in string literals: we pass as input the maximum allowed character code, which is determined from the character constant or string literal prefix if present (see callers), and suffices to express the applicable restrictions.

Definitions and Theorems

Function: valid-oct-escape

(defun valid-oct-escape (esc max)
 (declare (xargs :guard (and (oct-escapep esc) (natp max))))
 (let ((__function__ 'valid-oct-escape))
  (declare (ignorable __function__))
  (b*
   (((reterr) 0)
    (code
     (oct-escape-case
      esc
      :one (str::oct-digit-char-value esc.digit)
      :two (str::oct-digit-chars-value (list esc.digit1 esc.digit2))
      :three (str::oct-digit-chars-value
                  (list esc.digit1 esc.digit2 esc.digit3)))))
   (if (<= code (nfix max))
       (retok code)
    (reterr
     (msg
      "The octal escape sequence ~x0 ~
                    has value ~x1, which exceeds the maximum allowed ~x2, ~
                    required in the context of where this octal escape occurs."
      (oct-escape-fix esc)
      code (nfix max)))))))

Theorem: natp-of-valid-oct-escape.code

(defthm natp-of-valid-oct-escape.code
  (b* (((mv acl2::?erp ?code)
        (valid-oct-escape esc max)))
    (natp code))
  :rule-classes :rewrite)

Theorem: valid-oct-escape-of-oct-escape-fix-esc

(defthm valid-oct-escape-of-oct-escape-fix-esc
  (equal (valid-oct-escape (oct-escape-fix esc)
                           max)
         (valid-oct-escape esc max)))

Theorem: valid-oct-escape-oct-escape-equiv-congruence-on-esc

(defthm valid-oct-escape-oct-escape-equiv-congruence-on-esc
  (implies (oct-escape-equiv esc esc-equiv)
           (equal (valid-oct-escape esc max)
                  (valid-oct-escape esc-equiv max)))
  :rule-classes :congruence)

Theorem: valid-oct-escape-of-nfix-max

(defthm valid-oct-escape-of-nfix-max
  (equal (valid-oct-escape esc (nfix max))
         (valid-oct-escape esc max)))

Theorem: valid-oct-escape-nat-equiv-congruence-on-max

(defthm valid-oct-escape-nat-equiv-congruence-on-max
  (implies (acl2::nat-equiv max max-equiv)
           (equal (valid-oct-escape esc max)
                  (valid-oct-escape esc max-equiv)))
  :rule-classes :congruence)