• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
          • Vl-translation-p
            • Vl-translation
            • Make-vl-translation
            • Change-vl-translation
              • Vl-translation-has-module
              • Honsed-vl-translation
              • Make-honsed-vl-translation
              • Vl-translation-get-esim
              • Vl-translation->orig
              • Vl-translation->good
              • Vl-translation->filemap
              • Vl-translation->defines
              • Vl-translation->bad
            • Vl-simplify
            • Defmodules-fn
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-translation-p

    Change-vl-translation

    A copying macro that lets you create new vl-translation-p structures, based on existing structures.

    Syntax:

    (change-vl-translation x 
                           [:good <good>] 
                           [:bad <bad>] 
                           [:orig <orig>] 
                           [:filemap <filemap>] 
                           [:defines <defines>]) 
    

    This is a sometimes useful alternative to make-vl-translation. It constructs a new vl-translation-p structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

    This is an ordinary change- macro introduced by defaggregate.

    Macro: change-vl-translation

    (defmacro change-vl-translation (x &rest args)
      (std::change-aggregate 'vl-translation
                             x args
                             '((:good . vl-translation->good)
                               (:bad . vl-translation->bad)
                               (:orig . vl-translation->orig)
                               (:filemap . vl-translation->filemap)
                               (:defines . vl-translation->defines))
                             'change-vl-translation
                             'nil))