• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
        • Ps
        • Basic-printing
        • Verilog-printing
          • Vl-fmt
          • Vl-ppc-module
          • Vl-pp-expr
          • Vl-maybe-escape-identifier
          • Vl-print-ext-wirename
          • Vl-pp-module
          • Vl-print-wirename
          • Vl-print-loc
          • Vl-print-modname
          • Vl-pp-origexpr
          • Vl-pps-module
          • Vl-pps-expr
          • Vl-ppc-modulelist
          • Vl-ppcs-module
          • Vl-ps-update-show-atts
          • Vl-pps-origexpr
          • Vl-pps-modulelist
          • Vl-ppcs-modulelist
          • Vl-cw-obj
          • Vl-ps->show-atts-p
          • Vl-cw
        • Printing-locally
        • Formatted-printing
        • Accessing-printed-output
        • Vl-printedlist
        • Json-printing
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Verilog-printing

Vl-print-loc

(vl-print-loc x &key (ps 'ps)) prints a vl-location-p.

Signature

(vl-print-loc x &key (ps 'ps)) → ps

Arguments

x — Guard (vl-location-p x).

In text mode, this function basically prints the string produced by vl-location-string. But when HTML mode is active, we instead print something along the lines of:

<a class="vl_loclink"
   href="javascript:void(0);"
   onClick="showLoc('foo', 'line', 'col')">
  foo:line:col
</a>

This function is used in various warning messages, reports, and other displays. The module browser's web pages are responsible for defining the showLoc function to carry out some sensible behavior.

Definitions and Theorems

Function: vl-print-loc-fn

(defun vl-print-loc-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-location-p x)))
 (let ((__function__ 'vl-print-loc))
  (declare (ignorable __function__))
  (if (not (vl-ps->htmlp))
      (let* ((str (vl-location-string x))
             (len (length str))
             (col (vl-ps->col))
             (autowrap-col (vl-ps->autowrap-col))
             (autowrap-ind (vl-ps->autowrap-ind)))
        (cond ((or (< (+ col len) autowrap-col)
                   (< col (+ autowrap-ind 10)))
               (vl-print-str str))
              (t (vl-ps-seq (vl-println "")
                            (vl-indent autowrap-ind)
                            (vl-print-str str)))))
   (let* ((filename (vl-location->filename x))
          (line (vl-location->line x))
          (col (vl-location->col x))
          (flen (length filename))
          (last-slash (str::strrpos "/" filename))
          (shortname (if (and last-slash (< last-slash flen))
                         (subseq filename (1+ last-slash) nil)
                       filename)))
    (vl-ps-seq
     (vl-print-markup
      "<a class=\"vl_loclink\" href=\"javascript:void(0);\" onClick=\"showLoc('")
     (vl-print-url (vl-location->filename x))
     (vl-print-markup "', '")
     (vl-print-url line)
     (vl-print-markup "', '")
     (vl-print-url col)
     (vl-print-markup "')\")>")
     (vl-print-str shortname)
     (vl-print-str ":")
     (vl-print-nat line)
     (vl-print-str ":")
     (vl-print-nat col)
     (vl-print-markup "</a>"))))))

Theorem: vl-print-loc-fn-of-vl-location-fix-x

(defthm vl-print-loc-fn-of-vl-location-fix-x
  (equal (vl-print-loc-fn (vl-location-fix x) ps)
         (vl-print-loc-fn x ps)))

Theorem: vl-print-loc-fn-vl-location-equiv-congruence-on-x

(defthm vl-print-loc-fn-vl-location-equiv-congruence-on-x
  (implies (vl-location-equiv x x-equiv)
           (equal (vl-print-loc-fn x ps)
                  (vl-print-loc-fn x-equiv ps)))
  :rule-classes :congruence)