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
Syntax-for-tools
Atc
Language
Transformation-tools
Simpadd0
Splitgso
Constant-propagation
Specialize
Split-fn
Split-fn-implementation
Abstract-fn
Split-fn-block-item-list
Decl-to-ident-param-declon-map
Split-fn-fundef
Split-fn-extdecl
Split-fn-filepath-transunit-map
Split-fn-extdecl-list
Split-fn-transunit-ensemble
Split-fn-transunit
Param-declon-to-ident-param-declon-map
Param-declon-list-to-ident-param-declon-map
Ident-param-declon-map-filter
Decl-to-ident-param-declon-map0
Decl-list-to-ident-param-declon-map
Add-pointer-param-declon
Map-address-ident-list
Map-add-pointer-param-declon
Make-deref-subst
Ident-param-declon-map
Split-fn-event-generation
Split-fn-input-processing
Split-fn-when
Split-all-gso
Copy-fn
Rename
Utilities
Representation
Insertion-sort
Pack
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
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
Split-fn
Split-fn-implementation
Implementation of
split-fn
.
Subtopics
Abstract-fn
Create a new function from the block items following the
split-fn
split point.
Split-fn-block-item-list
Transform a list of block items.
Decl-to-ident-param-declon-map
Convert a regular declaration into an omap of identifiers to parameter declarations.
Split-fn-fundef
Transform a function definition, splitting it if matches the target identifier, or else leaving it untouched.
Split-fn-extdecl
Transform an external declaration.
Split-fn-filepath-transunit-map
Transform a filepath.
Split-fn-extdecl-list
Transform a list of external declarations.
Split-fn-transunit-ensemble
Transform a translation unit ensemble.
Split-fn-transunit
Transform a translation unit.
Param-declon-to-ident-param-declon-map
Convert a parameter declaration into a singleton omap associating the declared identifier to the declaration.
Param-declon-list-to-ident-param-declon-map
Fold
param-declon-to-ident-param-declon-map
over a list.
Ident-param-declon-map-filter
Decl-to-ident-param-declon-map0
Decl-list-to-ident-param-declon-map
Fold
decl-to-ident-param-declon-map
over a list.
Add-pointer-param-declon
Map-address-ident-list
Map
c$::expr-unary
c$::unop-address
over a list of identifiers.
Map-add-pointer-param-declon
Make-deref-subst
Ident-param-declon-map
An omap mapping
identp
to
param-declonp
.
Split-fn-event-generation
Event generation performed by
split-fn
.
Split-fn-input-processing
Input processing performed by
split-fn
.