		Search-engine friendly clone of the ACL2 documentation.

Opcode

Change-opcode

Modifying constructor for opcode structures.

Syntax

(change-opcode x 
               [:op <op>] 
               [:mode <mode>] 
               [:reg <reg>] 
               [:mod <mod>] 
               [:r/m <r/m>] 
               [:pfx <pfx>] 
               [:rex <rex>] 
               [:vex <vex>] 
               [:evex <evex>] 
               [:feat <feat>] 
               [:superscripts <superscripts>] 
               [:group <group>])

This is an often useful alternative to make-opcode.

We construct a new opcode 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 defprod.

Macro: change-opcode

(defmacro change-opcode (x &rest args)
  (std::change-aggregate 'opcode
                         x args
                         '((:op . opcode->op)
                           (:mode . opcode->mode)
                           (:reg . opcode->reg)
                           (:mod . opcode->mod)
                           (:r/m . opcode->r/m)
                           (:pfx . opcode->pfx)
                           (:rex . opcode->rex)
                           (:vex . opcode->vex)
                           (:evex . opcode->evex)
                           (:feat . opcode->feat)
                           (:superscripts . opcode->superscripts)
                           (:group . opcode->group))
                         'change-opcode
                         'remake-opcode))