• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
            • Write-object
            • Objdesign-of-var
            • Compustate-scopes-numbers
            • Create-var
            • Read-object
            • Compustate
              • Compustatep
              • Compustate-fix
              • Compustate-equiv
              • Make-compustate
              • Compustate->frames
              • Change-compustate
                • Compustate->static
                • Compustate->heap
              • Frame
              • Enter-scope
              • Compustate-scopes-numbers-aux
              • Compustate-option
              • Push-frame
              • Exit-scope
              • Compustate-frames-number
              • Compustate-option-result
              • Scope-list-result
              • Pop-frame
              • Compustate-result
              • Scope-result
              • Compustate-top-frame-scopes-number
              • Top-frame
              • Heap
              • Scope
              • Scope-list
              • Frame-list
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Compustate

    Change-compustate

    Modifying constructor for compustate structures.

    Syntax
    (change-compustate x 
                       [:static <static>] 
                       [:frames <frames>] 
                       [:heap <heap>]) 
    

    This is an often useful alternative to make-compustate.

    We construct a new compustate 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 fty::defprod.

    Macro: change-compustate

    (defmacro change-compustate (x &rest args)
      (std::change-aggregate 'compustate
                             x args
                             '((:static . compustate->static)
                               (:frames . compustate->frames)
                               (:heap . compustate->heap))
                             'change-compustate
                             'nil))