Function:
(defun vl-echarlist-from-str-aux (x n xl filename line col nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (and (stringp x) (natp n) (stringp filename) (posp line) (natp col) (equal xl (length x))))) (declare (type string x filename) (type (integer 0 *) n xl line col)) (declare (xargs :split-types t :guard (<= n xl))) (let ((__function__ 'vl-echarlist-from-str-aux)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (nfix xl) (nfix n))) :exec (eql n xl))) (nrev-fix nrev)) ((the character char) (mbe :logic (char-fix (char x n)) :exec (char x n))) (echar (make-vl-echar-fast :char char :filename filename :line line :col col)) (nrev (nrev-push echar nrev)) (line (if (eql char #\Newline) (the (integer 0 *) (+ 1 line)) line)) (col (if (eql char #\Newline) 0 (the (integer 0 *) (+ 1 col))))) (vl-echarlist-from-str-aux (the string x) (the (integer 0 *) (+ 1 (lnfix n))) xl filename line col nrev))))