		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-maybe-escape-string

Signature
(vl-maybe-escape-string x i len acc) → new-acc
Arguments: x — Guard (stringp x).; i — Guard (natp i).; len — Guard (and (natp len) (eql len (length x))).; acc — Guard (character-listp acc).
Returns: new-acc — Type (character-listp new-acc), given the guard.

Definitions and Theorems

Function: vl-maybe-escape-string

(defun vl-maybe-escape-string (x i len acc)
  (declare
       (xargs :guard (and (stringp x)
                          (natp i)
                          (character-listp acc)
                          (and (natp len) (eql len (length x))))))
  (declare (xargs :guard (<= i len)))
  (let ((__function__ 'vl-maybe-escape-string))
    (declare (ignorable __function__))
    (if (mbe :logic (zp (- (nfix len) (nfix i)))
             :exec (int= i len))
        (reverse acc)
      (let ((car (char x i)))
        (vl-maybe-escape-string
             x (+ 1 (lnfix i))
             len
             (case car (#\Newline (list* #\n #\\ acc))
                   (#\Tab (list* #\t #\\ acc))
                   (#\\ (list* #\\ #\\ acc))
                   (#\" (list* #\" #\\ acc))
                   (t (cons car acc))))))))

Theorem: character-listp-of-vl-maybe-escape-string

(defthm character-listp-of-vl-maybe-escape-string
  (implies (and (force (stringp x))
                (force (natp i))
                (force (character-listp acc))
                (force (if (natp len)
                           (eql len (length x))
                         'nil))
                (force (not (< len i))))
           (b* ((new-acc (vl-maybe-escape-string x i len acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)