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
Gl
Esim
Vl2014
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Expression-sizing
Occform
Oprewrite
Expand-functions
Delayredux
Unparameterization
Caseelim
Split
Selresolve
Weirdint-elim
Vl-delta
Replicate-insts
Rangeresolve
Propagate
Clean-selects
Clean-params
Blankargs
Inline-mods
Expr-simp
Trunc
Always-top
Edgesynth
Stmtrewrite
Vl-modulelist-stmtrewrite
Vl-blockstmt-rewrite
Vl-repeatstmt-rewrite
Vl-flatten-blocks
Vl-stmt-rewrite-top
Vl-casestmt-rewrite
Vl-stmt-rewrite
Vl-stmtlist-rewrite
Vl-caselist-rewrite
Vl-waitstmt-rewrite
Vl-ifstmt-combine-rewrite
Vl-forstmt-rewrite
Vl-initiallist-stmtrewrite
Vl-alwayslist-stmtrewrite
Vl-initial-stmtrewrite
Vl-foreverstmt-rewrite
Vl-always-stmtrewrite
Vl-module-stmtrewrite
Vl-design-stmtrewrite
Vl-remove-null-statements
Vl-$vcover-stmt-p
Vl-$display-stmt-p
Vl-caselist-all-null-p
Cblock
Vl-always-convert-regports
Vl-always-convert-regs
Stmttemps
Edgesplit
Vl-always-check-reg
Vl-convert-regs
Latchsynth
Vl-always-check-regs
Vl-match-always-at-some-edges
Unelse
Vl-always-convert-reg
Vl-design-always-backend
Vl-stmt-guts
Vl-always-convert-regport
Vl-always-scary-regs
Eliminitial
Ifmerge
Vl-edge-control-p
Elimalways
Gatesplit
Gate-elim
Expression-optimization
Elim-supplies
Wildelim
Drop-blankports
Clean-warnings
Addinstnames
Custom-transform-hooks
Annotate
Latchcode
Elim-unused-vars
Problem-modules
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-stmt-rewrite
Vl-caselist-rewrite
Signature
(vl-caselist-rewrite x unroll-limit warnings) → (mv warnings new-x)
Arguments
x
—
Guard
(
vl-caselist-p
x)
.
unroll-limit
—
Guard
(
natp
unroll-limit)
.
warnings
—
Guard
(
vl-warninglist-p
warnings)
.
Returns
warnings
—
Type
(
vl-warninglist-p
warnings)
.
new-x
—
Type
(
vl-caselist-p
new-x)
.