• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • C
        • Syntax-for-tools
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
              • Atc-symbolic-computation-states
              • Atc-symbolic-execution-rules
                • Atc-exec-expr-pure-rules
                • Atc-exec-expr-when-asg-arrsub-rules-generation
                • Integer-value-disjoint-rules
                • Atc-uaconvert-values-rules
                • Atc-exec-unary-nonpointer-rules-generation
                • Atc-exec-unary-nonpointer-rules
                • Atc-exec-expr-when-asg-indir-rules
                • Atc-exec-expr-when-asg-arrsub-rules
                • Atc-exec-cast-rules-generation
                • Atc-exec-cast-rules
                • Atc-exec-binary-strict-pure-rules-generation
                • Atc-convert-integer-value-rules
                • Atc-array-read-rules
                • Array-value-disjoint-rules
                • Atc-exec-expr-when-asg-indir-rule-generation
                • Atc-identifier-rules
                • Atc-object-designator-rules
                • Atc-flexible-array-member-rules
                • Atc-exec-stmt-rules
                • Atc-exec-indir-rules
                • Atc-uaconvert-values-rules-generation
                • Atc-exec-arrsub-rules
                • Value-bridge-theorems
                • Atc-test-value-rules
                • Atc-exec-const-rules
                • *atc-integer-ops-2-return-rewrite-rules*
                • *atc-integer-ops-2-type-prescription-rules*
                • Atc-apconvert-rules
                • Atc-integer-conv-rules
                • Atc-adjust-type-rules
                • Atc-exec-block-item-list-rules
                • Atc-exec-arrsub-rules-generation
                • Atc-exec-fun-rules
                • Atc-static-variable-pointer-rules
                • Atc-exec-indir-rules-generation
                • Atc-exec-binary-strict-pure-rules
                • Atc-array-write-rules
                • Array-value-rules
                • Atc-pointed-integer-rules
                • Atc-array-length-rules
                • *atc-exec-cast-rules*
                • Atc-value-array->elemtype-rules
                • Atc-limit-rules
                • Type-of-value-under-array-predicates
                • Atc-value-integer->get-rules
                • Atc-distributivity-over-if-rewrite-rules
                • *atc-integer-convs-type-prescription-rules*
                • Atc-value-array->elements-rules
                • Atc-syntaxp-hyp-for-expr-pure
                • *atc-uaconvert-values-rules*
                • *atc-integer-ops-1-return-rewrite-rules*
                • *atc-integer-convs-return-rewrite-rules*
                • Valuepred-when-value-kind
                • Valuepred-to-type-of-value-equalities
                • Atc-promote-value-rules
                • *atc-integer-ops-1-type-prescription-rules*
                • *atc-all-rules*
                • Atc-integer-ifix-rules
                • Atc-exec-expr-when-asg-ident-rules
                • *atc-type-prescription-rules*
                • Atc-hide-rules
                • Type-of-value-when-valuepred
                • Atc-value-integerp-rules
                • Atc-not-error-rules
                • Value-listp-when-valuepred-listp
                • Value-kind-when-valuepred
                • Atc-value-arithmeticp-rules
                • Atc-type-kind-rules
                • *atc-compound-recognizer-rules*
                • Atc-value-pointer-rules
                • Atc-boolean-equality-rules
                • Atc-tyname-to-type-rules
                • Atc-integer-size-rules
                • Atc-init-scope-rules
                • Atc-boolean-from-sint
                • Valuep-when-valuepred
                • Atc-if*-rules
                • Atc-exec-ident-rules
                • Atc-integer-const-rules
                • Atc-sint-get-rules
                • Atc-exec-expr-when-call-rules
                • Atc-type-of-value-option-rules
                • Atc-identifier-other-rules
                • Atc-boolean-from-integer-return-rules
                • *atc-exec-unary-nonpointer-rules*
                • *atc-convert-integer-value-rules*
                • Atc-lognot-sint-rules
                • Atc-sint-from-boolean-rules
                • Atc-value-optionp-rules
                • Atc-type-of-value-rules
                • Atc-exec-obj-declon-rules
                • Atc-compustatep-rules
                • Value-tau-rules
                • Atc-valuep-rules
                • Atc-exec-expr-pure-list-rules
                • Atc-exec-block-item-rules
                • Atc-boolean-fron/to-sint-rules
                • *atc-other-executable-counterpart-rules*
                • Value-promoted-arithmeticp-alt-def
                • Atc-exec-initer-rules
                • *atc-type-of-value-rules*
                • *atc-identifier-rules*
                • *atc-flexible-array-member-rules*
                • *atc-exec-expr-pure-rules*
                • *atc-boolean-from-integer-return-rules*
                • *atc-array-read-rules*
                • Valuep-possibilities
                • Value-unsigned-integerp-alt-def
                • Value-signed-integerp-alt-def
                • Atc-value-listp-rules
                • *atc-pointed-integers-type-prescription-rules*
                • *atc-pointed-integer-rules*
                • *atc-array-write-return-rewrite-rules*
                • *atc-array-read-return-rewrite-rules*
                • Atc-exec-expr-when-pure-rules
                • Array-tau-rules
                • *atc-not-error-rules*
                • *atc-integer-conv-rules*
                • *atc-exec-expr-when-asg-arrsub-rules*
                • *atc-array-write-type-prescription-rules*
                • *atc-array-read-type-prescription-rules*
                • *atc-array-length-rules*
                • *atc-adjust-type-rules*
                • Atc-sint-from-boolean
                • Atc-init-value-to-value-rules
                • *atc-value-integer->get-rules*
                • *atc-static-variable-pointer-rules*
                • *atc-integer-size-rules*
                • *atc-integer-constructors-return-rules*
                • *atc-exec-stmt-rules*
                • *atc-exec-expr-when-asg-indir-rules*
                • *atc-exec-const-rules*
                • *atc-distributivity-over-if-rewrite-rules*
                • Atc-wrapper-rules
                • Atc-value-result-fix-rules
                • Atc-value-kind-rules
                • Atc-array-length-write-rules
                • *atc-value-kind-rules*
                • *atc-value-array->elemtype-rules*
                • *atc-type-kind-rules*
                • *atc-test-value-rules*
                • *atc-promote-value-rules*
                • *atc-integer-ifix-rules*
                • *atc-integer-fix-rules*
                • *atc-integer-const-rules*
                • *atc-exec-indir-rules*
                • *atc-exec-arrsub-rules*
                • *atc-computation-state-return-rules*
                • *atc-array-length-write-rules*
                • *atc-apconvert-rules*
                • Atc-misc-rewrite-rules
                • *atc-valuep-rules*
                • *atc-tyname-to-type-rules*
                • *atc-object-designator-rules*
                • *atc-init-scope-rules*
                • *atc-exec-expr-when-call-rules*
                • *atc-exec-expr-when-asg-rules*
                • *atc-exec-expr-when-asg-ident-rules*
                • *atc-exec-block-item-rules*
                • Atc-computation-state-return-rules
                • *atc-wrapper-rules*
                • *atc-value-result-fix-rules*
                • *atc-value-optionp-rules*
                • *atc-value-listp-rules*
                • *atc-value-fix-rules*
                • *atc-type-of-value-option-rules*
                • *atc-sint-get-rules*
                • *atc-sint-from-boolean*
                • *atc-misc-rewrite-rules*
                • *atc-lognot-sint-rules*
                • *atc-limit-rules*
                • *atc-init-value-to-value-rules*
                • *atc-exec-obj-declon-rules*
                • *atc-exec-initer-rules*
                • *atc-exec-ident-rules*
                • *atc-exec-fun-rules*
                • *atc-exec-expr-when-pure-rules*
                • *atc-exec-expr-pure-list-rules*
                • *atc-exec-block-item-list-rules*
                • *atc-boolean-from-sint*
                • Atc-value-fix-rules
                • Atc-integer-fix-rules
                • Atc-integer-constructors-return-rules
                • Atc-exec-expr-when-asg-rules
              • Atc-gen-ext-declon-lists
              • Atc-function-and-loop-generation
              • Atc-statement-generation
              • Atc-gen-fileset
              • Atc-gen-everything
              • Atc-gen-obj-declon
              • Atc-gen-fileset-event
              • Atc-tag-tables
              • Atc-expression-generation
              • Atc-generation-contexts
              • Atc-gen-wf-thm
              • Term-checkers-atc
              • Atc-variable-tables
              • Term-checkers-common
              • Atc-gen-init-fun-env-thm
              • Atc-gen-appconds
              • Read-write-variables
              • Atc-gen-thm-assert-events
              • Test*
              • Atc-gen-prog-const
              • Atc-gen-expr-bool
              • Atc-theorem-generation
              • Atc-tag-generation
              • Atc-gen-expr-pure
              • Atc-function-tables
              • Atc-object-tables
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
            • Atc-macro-definition
          • Atc-tutorial
          • Pure-expression-execution
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atc-symbolic-execution-rules

*atc-exec-fun-rules*

Definition: *atc-exec-fun-rules*

(defconst *atc-exec-fun-rules*
  '(exec-fun-open-return exec-fun-open-noreturn
                         (:e fun-info->params)
                         (:e fun-info->result)
                         (:e fun-info->body)))