Search-engine friendly clone of the
ACL2 documentation
.
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
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
Java
Riscv
Taspi
Bitcoin
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
Aleo
Aleobft
Aleovm
Leo
Grammar
Early-version
Json2ast
Testing
Definition
Flattening
Abstract-syntax
Dynamic-semantics
Compilation
Static-semantics
Type-checking
Static-environments
Curve-parameterization
Function-recursion
Statements-callees
Expressions-callees
File-function-recursion-okp
Topdecl-list-call-graph
Fundecl-call-graph
Topdecl-call-graph
Expression-callees
Constdecl-callees
Console-callees
Vardecl-callees
Struct-init-list-callees
Struct-init-callees
Statement-list-callees
Expression-list-callees
Branch-list-callees
Statement-callees
Branch-callees
Struct-recursion
Input-checking
Program-checking
Type-maps-for-struct-components
Program-and-input-checking
Output-checking
Concrete-syntax
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
Function-recursion
Statements-callees
Statement-callees
Functions called by a statement.
Signature
(statement-callees stmt) → callees
Arguments
stmt
—
Guard
(
statementp
stmt)
.
Returns
callees
—
Type
(
identifier-setp
callees)
.