• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
          • Transformation-tools
            • Simpadd0
            • Deftrans
            • Splitgso
            • Constant-propagation
              • Value-to-expr
              • Const-prop-eval-impure-binop-expr
              • Env
              • Const-prop-eval-pure-binop-expr
              • Const-prop-filepath-transunit-map
              • Const-prop-eval-unop-expr
              • Const-prop-transunit-ensemble
              • Const-prop-fundef
              • Value-result-to-option
              • Const-prop-extdecl-list
              • Const-prop-extdecl
              • Zero-valuep
              • Iconst-to-value
              • Const-to-value
              • Expr-to-ident
              • Const-prop-transunit
              • Pure-binopp
              • Const-prop-initdeclor-list
              • Const-prop-initdeclor
              • Const-prop-structdeclor-list
              • Const-prop-structdecl-list
              • Const-prop-param-declon-list
              • Const-prop-initer-option
              • Const-prop-initer
              • Const-prop-expr-option
              • Const-prop-dirabsdeclor-option
              • Const-prop-dirabsdeclor
              • Const-prop-const-expr-option
              • Const-prop-absdeclor-option
              • Const-prop-type-spec
              • Const-prop-strunispec
              • Const-prop-structdeclor
              • Const-prop-structdecl
                • Const-prop-statassert
                • Const-prop-spec/qual-list
                • Const-prop-spec/qual
                • Const-prop-param-declor
                • Const-prop-param-declon
                • Const-prop-member-designor
                • Const-prop-genassoc-list
                • Const-prop-genassoc
                • Const-prop-expr-list
                • Const-prop-expr
                • Const-prop-enumspec
                • Const-prop-enumer-list
                • Const-prop-dirdeclor
                • Const-prop-desiniter-list
                • Const-prop-desiniter
                • Const-prop-designor-list
                • Const-prop-designor
                • Const-prop-declor-option
                • Const-prop-decl-spec-list
                • Const-prop-decl-spec
                • Const-prop-decl-list
                • Const-prop-block-item-list
                • Const-prop-align-spec
                • Const-prop-absdeclor
                • Const-prop-tyname
                • Const-prop-stmt
                • Const-prop-label
                • Const-prop-enumer
                • Const-prop-declor
                • Const-prop-decl
                • Const-prop-const-expr
                • Const-prop-block-item
              • Split-fn
              • Copy-fn
              • Specialize
              • Split-all-gso
              • Rename
              • Utilities
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Constant-propagation

    Const-prop-structdecl

    Propagate a constant through a c$::structdecl.

    Signature
    (const-prop-structdecl structdecl env) 
      → 
    (mv new-structdecl new-env)
    Arguments
    structdecl — Guard (structdeclp structdecl).
    env — Guard (envp env).
    Returns
    new-structdecl — Type (structdeclp new-structdecl).
    new-env — Type (envp new-env).