• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
          • Simpadd0
            • Simpadd0-dirdeclor
            • Simpadd0-implementation
              • Simpadd0-event-generation
                • Simpadd0-exprs/decls/stmts
                  • Simpadd0-dirdeclor
                  • Simpadd0-declor
                    • Simpadd0-init-declor
                    • Simpadd0-init-declor-list
                    • Simpadd0-declon
                    • Simpadd0-comp-stmt
                    • Simpadd0-param-declor
                    • Simpadd0-param-declon-list
                    • Simpadd0-param-declon
                    • Simpadd0-expr-option
                    • Simpadd0-struct-declor-list
                    • Simpadd0-struct-declon-list
                    • Simpadd0-dirabsdeclor-option
                    • Simpadd0-desiniter-list
                    • Simpadd0-struni-spec
                    • Simpadd0-struct-declor
                    • Simpadd0-struct-declon
                    • Simpadd0-statassert
                    • Simpadd0-spec/qual-list
                    • Simpadd0-spec/qual
                    • Simpadd0-genassoc-list
                    • Simpadd0-dirabsdeclor
                    • Simpadd0-desiniter
                    • Simpadd0-designor-list
                    • Simpadd0-decl-spec-list
                    • Simpadd0-const-expr-option
                    • Simpadd0-align-spec
                    • Simpadd0-absdeclor-option
                    • Simpadd0-type-spec
                    • Simpadd0-tyname
                    • Simpadd0-member-designor
                    • Simpadd0-initer-option
                    • Simpadd0-initer
                    • Simpadd0-genassoc
                    • Simpadd0-expr-list
                    • Simpadd0-enumer-list
                    • Simpadd0-enumer
                    • Simpadd0-enum-spec
                    • Simpadd0-designor
                    • Simpadd0-declor-option
                    • Simpadd0-declon-list
                    • Simpadd0-decl-spec
                    • Simpadd0-const-expr
                    • Simpadd0-block-item-list
                    • Simpadd0-block-item
                    • Simpadd0-absdeclor
                    • Simpadd0-stmt
                    • Simpadd0-label
                    • Simpadd0-expr
                  • Simpadd0-expr-binary
                  • Simpadd0-fundef
                  • Simpadd0-filepath-transunit-map
                  • Simpadd0-transunit
                  • Simpadd0-ext-declon-list
                  • Simpadd0-transunit-ensemble
                  • Simpadd0-ext-declon
                  • Simpadd0-code-ensemble
                  • Simpadd0-gen-everything
                • Simpadd0-process-inputs-and-gen-everything
                • Simpadd0-fn
                • Simpadd0-input-processing
                • Simpadd0-macro-definition
              • Simpadd0-declor
                • Simpadd0-init-declor
                • Simpadd0-init-declor-list
                • Simpadd0-declon
                • Simpadd0-comp-stmt
                • Simpadd0-param-declor
                • Simpadd0-param-declon-list
                • Simpadd0-param-declon
                • Simpadd0-expr-option
                • Simpadd0-struct-declor-list
                • Simpadd0-struct-declon-list
                • Simpadd0-dirabsdeclor-option
                • Simpadd0-desiniter-list
                • Simpadd0-struni-spec
                • Simpadd0-struct-declor
                • Simpadd0-struct-declon
                • Simpadd0-statassert
                • Simpadd0-spec/qual-list
                • Simpadd0-spec/qual
                • Simpadd0-genassoc-list
                • Simpadd0-dirabsdeclor
                • Simpadd0-desiniter
                • Simpadd0-designor-list
                • Simpadd0-decl-spec-list
                • Simpadd0-const-expr-option
                • Simpadd0-align-spec
                • Simpadd0-absdeclor-option
                • Simpadd0-type-spec
                • Simpadd0-tyname
                • Simpadd0-member-designor
                • Simpadd0-initer-option
                • Simpadd0-initer
                • Simpadd0-genassoc
                • Simpadd0-expr-list
                • Simpadd0-enumer-list
                • Simpadd0-enumer
                • Simpadd0-enum-spec
                • Simpadd0-designor
                • Simpadd0-declor-option
                • Simpadd0-declon-list
                • Simpadd0-decl-spec
                • Simpadd0-const-expr
                • Simpadd0-block-item-list
                • Simpadd0-block-item
                • Simpadd0-absdeclor
                • Simpadd0-stmt
                • Simpadd0-label
                • Simpadd0-expr
              • Proof-generation
              • Split-gso
              • Wrap-fn
              • Constant-propagation
              • Specialize
              • Split-fn
              • Split-fn-when
              • Split-all-gso
              • Copy-fn
              • Variables-in-computation-states
              • Rename
              • Utilities
              • Proof-generation-theorems
              • Input-processing
            • Language
            • Representation
            • Insertion-sort
            • Pack
          • Proof-checker-array
          • Soft
          • Farray
          • Rp-rewriter
          • Instant-runoff-voting
          • Imp-language
          • Sidekick
          • Ethereum
          • Leftist-trees
          • Java
          • Riscv
          • Taspi
          • Bitcoin
          • Zcash
          • Des
          • X86isa
          • Sha-2
          • Yul
          • Proof-checker-itp13
          • Regex
          • ACL2-programming-language
          • Json
          • Jfkr
          • Equational
          • Cryptography
          • Axe
          • Poseidon
          • Where-do-i-place-my-book
          • Aleo
          • Bigmems
          • Builtins
          • Execloader
          • Solidity
          • Paco
          • Concurrent-programs
          • Bls12-377-curves
        • Debugging
        • Community
        • Std
        • Proof-automation
        • Macro-libraries
        • ACL2
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Simpadd0
      • Simpadd0-exprs/decls/stmts

      Simpadd0-declor

      Transform a declarator.

      Signature
      (simpadd0-declor declor fundefp gin) 
        → 
      (mv new-declor new-fundefp gout)
      Arguments
      declor — Guard (declorp declor).
      fundefp — Guard (booleanp fundefp).
      gin — Guard (ginp gin).
      Returns
      new-declor — Type (declorp new-declor).
      new-fundefp — Type (booleanp new-fundefp).
      gout — Type (goutp gout).

      The fundefp flag is set iff the declarator is (part of) the one of a function definition whose parameters have not been transformed yet; see the callers of this function. A possibly changed flag is returned as output: see simpadd0-dirdeclor for its use and possile change.