• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Vl-loadstate
          • Lexer
          • Parser
          • Vl-load-merge-descriptions
          • Vl-find-basename/extension
          • Vl-load-file
          • Vl-loadresult
          • Scope-of-defines
          • Vl-find-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-read-file
          • Vl-includeskips-report-gather
          • Vl-load-main
          • Extended-characters
            • Vl-location
              • Vl-location-p
              • Vl-string-between-locs
              • Vl-location-between-p
              • Vl-string-findloc
              • Vl-linecol
              • Vl-location-string
              • Vl-location-fix
              • Vl-location->line
              • Vl-location->filename
              • Vl-location->col
              • Vl-locationlist
              • *vl-fakeloc*
            • Vl-echar-p
            • Vl-echarlist->chars
            • Vl-echarlist-from-chars
            • Vl-echarlist-from-str
            • Vl-echarlist-unsigned-value
            • Vl-change-echarlist-locations
            • Vl-echar-digit-value
            • Vl-echarlist->string
          • Vl-load
          • Vl-load-description
          • Vl-descriptions-left-to-load
          • Inject-warnings
          • Vl-preprocess-debug
          • Vl-write-preprocessor-debug-file
          • Vl-read-file-report-gather
          • Vl-load-descriptions
          • Vl-load-files
          • Translate-off
          • Vl-load-read-file-hook
          • Vl-read-file-report
          • Vl-loadstate-pad
          • Vl-load-summary
          • Vl-collect-modules-from-descriptions
          • Vl-loadstate->warnings
          • Vl-iskips-report
          • Vl-descriptionlist
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Extended-characters

Vl-location

Representation of a point in a source file.

Signature
(vl-location filename line col) → loc
Arguments
filename — Guard (stringp filename).
line — Guard (posp line).
col — Guard (natp col).
Returns
loc — Type (vl-location-p loc).

A vl-location structure represents some location in a source code file. These locations are attached to characters and module items to provide context during error reporting.

Historically, vl-location was an ordinary, tagged defprod with three fields: a filename, line number, and column number. Because there are many locations, this representation used a lot of memory.

We now instead represent locations using a custom structure, essentially of the form:

(linecol . (:vl-location . filename))

Where the line and column number typically are only a single fixnum; see vl-linecol. It looks like this takes 2 conses, but we hons the (:vl-location . filename) pair so that we only need one such cons per file. So for all practical purposes, each vl-location really only costs us a single cons.

Despite this fancy representation, the interface to locations still acts as though it is a defprod with just a filename, line, and column number. You can use the ordinary b* binders and make/change macros to access and create locations, as you would expect.

A downside of this representation is that vl-location structures are no longer very readable when you encounter them in traces, etc. However, the :vl-location tag is still there, which allows vl-fmt to understand when it has encountered a location, and to print these locations in a readable way.

Subtopics

Vl-location-p
Recognizer for vl-location structures.
Vl-string-between-locs
Given a string, extract all text that occurs between two vl-location-ps.
Vl-location-between-p
(vl-location-between-p x min max) is true exactly when x is in the same file as min and max, and inclusively falls between these bounds.
Vl-string-findloc
Traverse a string to determine the position of a vl-location-p.
Vl-linecol
Packed representation of a line number and column number.
Vl-location-string
Convert an vl-location-p into a string.
Vl-location-fix
Fixing function for vl-location structures.
Vl-location->line
Get the line number from a vl-location.
Vl-location->filename
Get the filename from a vl-location.
Vl-location->col
Get the column number from a vl-location.
Vl-locationlist
A list of vl-location-p objects.
*vl-fakeloc*
A "fake" vl-location-p which we use when generating our own extended-characters and module items.