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
C
Syntax-for-tools
Atc
Transformation-tools
Simpadd0
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
Free-vars
Abstract-syntax-rename-fn
Call-graphs
Fresh-ident-utility
Collect-idents
Subst-free
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
Transformation-tools
Utilities
Utilities for C transformations.
Subtopics
Free-vars
A utility to collect free variables over a C AST.
Abstract-syntax-rename-fn
Call-graphs
Utilities to build a call graph from C translation units.
Fresh-ident-utility
A utility to create a globally fresh C identifier.
Collect-idents
A utility to collect identifiers within a C program.
Subst-free
A utility to substitute expressions in for free variables in a C AST.