Search-engine friendly clone of the
ACL2 documentation
.
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
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
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-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-asg-indir-rules
Atc-exec-expr-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-identifier-rules
Atc-exec-expr-asg-indir-rule-generation
Atc-object-designator-rules
Atc-flexible-array-member-rules
Atc-exec-indir-rules
Atc-uaconvert-values-rules-generation
Atc-exec-stmt-rules
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-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
Atc-exec-fun-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-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-exec-expr-asg-ident-rules
Atc-boolean-from-sint
Valuep-when-valuepred
Atc-if*-rules
Atc-exec-ident-rules
Atc-integer-const-rules
Atc-sint-get-rules
Atc-type-of-value-option-rules
Atc-identifier-other-rules
Atc-exec-block-item-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-expr-call-or-pure-rules
Atc-exec-expr-call-or-asg-rules
Atc-compustatep-rules
Value-tau-rules
Atc-valuep-rules
Atc-exec-expr-pure-list-rules
Atc-boolean-fron/to-sint-rules
*atc-other-executable-counterpart-rules*
Value-promoted-arithmeticp-alt-def
*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-exec-expr-asg-indir-rules*
*atc-array-write-return-rewrite-rules*
*atc-array-read-return-rewrite-rules*
Atc-exec-initer-rules
Array-tau-rules
*atc-not-error-rules*
*atc-integer-conv-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-exec-expr-call-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-asg-arrsub-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-call-or-pure-rules*
*atc-exec-expr-call-or-asg-rules*
*atc-exec-expr-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-initer-rules*
*atc-exec-ident-rules*
*atc-exec-fun-rules*
*atc-exec-expr-pure-list-rules*
*atc-exec-expr-call-rules*
*atc-exec-expr-asg-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-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
Syntax-for-tools
Language
Representation
Transformation-tools
Pack
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Atc-symbolic-execution-rules
*atc-exec-expr-call-rules*
Definition:
*atc-exec-expr-call-rules*
(
defconst
*atc-exec-expr-call-rules* '(exec-expr-call-open))