(vl-write-preprocessor-debug-file filename preprocessed state) → (mv filename state)
Function:
(defun vl-write-preprocessor-debug-file (filename preprocessed state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (stringp filename) (vl-echarlist-p preprocessed)))) (let ((__function__ 'vl-write-preprocessor-debug-file)) (declare (ignorable __function__)) (b* (((mv okp state) (oslib::mkdir "./vl-debug")) ((unless okp) (cw "Error: Can't create ./vl-debug directory.~%") (mv nil state)) (nameidx (nfix (and (boundp-global 'vl-preprocess-debug-file-nameidx state) (f-get-global 'vl-preprocess-debug-file-nameidx state)))) (state (f-put-global 'vl-preprocess-debug-file-nameidx (+ 1 nameidx) state)) ((mv err basename state) (oslib::basename filename)) (basename (if err "basename-error" basename)) (tempname (cat "./vl-debug/" (natstr nameidx) "-" basename ".vpp")) (- (cw "Saving preprocessed ~s0 as ~s1.~%" filename tempname)) (state (with-ps-file tempname (vl-print-str (vl-echarlist->string preprocessed))))) (mv tempname state))))
Theorem:
(defthm maybe-stringp-of-vl-write-preprocessor-debug-file.filename (b* (((mv ?filename acl2::?state) (vl-write-preprocessor-debug-file filename preprocessed state))) (maybe-stringp filename)) :rule-classes :type-prescription)
Theorem:
(defthm state-p1-of-vl-write-preprocessor-debug-file.state (implies (state-p1 state) (b* (((mv ?filename acl2::?state) (vl-write-preprocessor-debug-file filename preprocessed state))) (state-p1 state))) :rule-classes :rewrite)