• 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
        • Vl-lintconfig-p
        • Lucid
        • Skip-detection
          • Sd-problem-p
          • Sd-keylist-find-skipped
          • Sd-keylist->indicies
          • Sd-key-p
          • Sd-patalist-compare
          • Sd-analyze-ctxexprs
          • Sd-problemlist-p
          • Sd-patalist-p
          • Sd-keygen
          • Sd-patalist
          • Sd-keylist-p
          • Sd-analyze-modulelist
          • Sd-analyze-module-aux
          • Sd-analyze-module
          • Sd-pp-problem-long
          • Sd-analyze-modulelist-aux
          • Sd-problem-score
          • Sd-pp-problem-header
          • Sd-analyze-design
          • Sd-problem->
          • Sd-pp-problem-brief
          • Sd-pp-problemlist-long
          • Sd-pp-problemlist-brief
          • Sd-natlist-linear-increments-p
          • Sd-keylist-linear-increments-p
        • Vl-lintresult-p
        • Lint-warning-suppression
        • Condcheck
        • Selfassigns
        • Leftright-check
        • Dupeinst-check
        • Oddexpr-check
        • Remove-toohard
        • Qmarksize-check
        • Portcheck
        • Duplicate-detect
        • Vl-print-certain-warnings
        • Duperhs-check
        • *vl-lint-help*
        • Lint-stmt-rewrite
        • Drop-missing-submodules
        • Check-case
        • Drop-user-submodules
        • Check-namespace
        • Vl-lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Skip-detection

Sd-pp-problem-long

Signature

(sd-pp-problem-long x &key (ps 'ps)) → ps

Arguments

x — Guard (sd-problem-p x).

Definitions and Theorems

Function: sd-pp-problem-long-fn

(defun sd-pp-problem-long-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (sd-problem-p x)))
  (let ((__function__ 'sd-pp-problem-long))
    (declare (ignorable __function__))
    (b* (((sd-problem x) x)
         (modname (vl-context1->mod x.ctx))
         (loc (vl-ctxelement->loc (vl-context1->elem x.ctx))))
      (if (not (vl-ps->htmlp))
          (vl-ps-seq (vl-print "In ")
                     (vl-print-modname modname)
                     (vl-print " (")
                     (vl-print-loc loc)
                     (vl-println ")")
                     (sd-pp-problem-header x)
                     (vl-indent 2)
                     (vl-println "")
                     (vl-print (vl-pp-context-modest x.ctx))
                     (vl-println "")
                     (vl-println ""))
        (vl-ps-seq (vl-println-markup "<dl class=\"sd_prob\">")
                   (sd-pp-problem-header x)
                   (vl-print-markup "<dt class=\"sd_loc\">")
                   (vl-print "In ")
                   (vl-print-modname modname)
                   (vl-print " at ")
                   (vl-print-loc loc)
                   (vl-println-markup "</dt>")
                   (vl-print-markup "<dd class=\"sd_context\">")
                   (vl-print (vl-pp-context-modest x.ctx))
                   (vl-println-markup "</dd>")
                   (vl-println-markup "</dl>"))))))