• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
        • Vl-main
        • Split-plusargs
          • Split-plusargs-exec
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Split-plusargs

Split-plusargs-exec

Signature

(split-plusargs-exec args acc plusacc) → (mv acc plusacc)

Arguments

args — Guard (string-listp args).

acc — Guard (string-listp acc).

plusacc — Guard (string-listp plusacc).

Returns

acc — Type (string-listp acc).

plusacc — Type (string-listp plusacc).

Definitions and Theorems

Function: split-plusargs-exec

(defun split-plusargs-exec (args acc plusacc)
  (declare (xargs :guard (and (string-listp args)
                              (string-listp acc)
                              (string-listp plusacc))))
  (let ((__function__ 'split-plusargs-exec))
    (declare (ignorable __function__))
    (b* (((when (atom args))
          (mv (string-list-fix acc)
              (string-list-fix plusacc)))
         ((cons first rest) args)
         ((mv acc plusacc)
          (if (and (< 0 (length first))
                   (eql (char first 0) #\+))
              (mv acc (cons (subseq first 1 nil) plusacc))
            (mv (cons first acc) plusacc))))
      (split-plusargs-exec rest acc plusacc))))

Theorem: string-listp-of-split-plusargs-exec.acc

(defthm string-listp-of-split-plusargs-exec.acc
  (b* (((mv ?acc ?plusacc)
        (split-plusargs-exec args acc plusacc)))
    (string-listp acc))
  :rule-classes :rewrite)

Theorem: string-listp-of-split-plusargs-exec.plusacc

(defthm string-listp-of-split-plusargs-exec.plusacc
  (b* (((mv ?acc ?plusacc)
        (split-plusargs-exec args acc plusacc)))
    (string-listp plusacc))
  :rule-classes :rewrite)