• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
          • Vl-echar-p
          • Vl-location
          • Vl-echarlist->chars
          • Vl-echarlist-from-chars
          • Vl-echarlist-from-str
            • Vl-echarlist-from-str-nice
            • Vl-echarlist-from-str-aux
          • Vl-echarlist-unsigned-value
          • Vl-change-echarlist-locations
          • Vl-echar-digit-value
          • Vl-echarlist->string
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-echarlist-from-str

Vl-echarlist-from-str-aux

Signature

(vl-echarlist-from-str-aux x n xl filename line col nrev) 
  → 
nrev

Arguments

x — Guard (stringp x).

n — Guard (natp n).

xl — Guard (equal xl (length x)).

filename — Guard (stringp filename).

line — Guard (posp line).

col — Guard (natp col).

Definitions and Theorems

Function: vl-echarlist-from-str-aux

(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))))