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
Expression-sizing-minutia
Expression-sizing-intro
Vl-keyvalue-pattern-collect-array-replacements
Vl-assignpattern-positional-replacement
Vl-plainarg-exprsize
Vl-assignpattern-keyvalue-replacement
Vl-keyvalue-pattern-collect-struct-replacements
Vl-modulelist-exprsize
Vl-expr-assignpattern-extend/truncate
Vl-structmemberlist->types
Vl-expr-size
Vl-expr-selfsize
Vl-op-selfsize
Vl-atom-selfsize
Vl-exprlist-selfsize
Vl-expr-typedecide
Vl-expr-expandsizes
Vl-exprlist-expandsizes
Vl-exprlist-size
Vl-expr-selfdetermine-type
Vl-assignpattern-multi-replacement
Vl-parse-keyval-pattern-struct
Vl-plainarglist-exprsize
Vl-parse-keyval-pattern-array
Vl-warn-about-implicit-extension
Vl-assigncontext-size
Vl-arguments-exprsize
Vl-assignpattern-replacement
Vl-packeddimensionlist-exprsize
Vl-namedparamvaluelist-exprsize
Vl-maybe-delayoreventcontrol-exprsize
Vl-repeateventcontrol-exprsize
Vl-paramvaluelist-exprsize
Vl-maybe-packeddimension-exprsize
Vl-delayoreventcontrol-exprsize
Vl-namedparamvalue-exprsize
Vl-namedarglist-exprsize
Vl-enumitemlist-exprsize
Vl-packeddimension-exprsize
Vl-maybe-paramvalue-exprsize
Vl-evatomlist-exprsize
Vl-atom-selfdetermine-type
Vl-rangelist-exprsize
Vl-maybe-gatedelay-exprsize
Vl-maybe-datatype-exprsize
Vl-gatedelay-exprsize
Vl-paramargs-exprsize
Vl-namedarg-exprsize
Vl-eventcontrol-exprsize
Vl-enumbasetype-exprsize
Vl-delaycontrol-exprsize
Vl-paramvalue-exprsize
Vl-maybe-range-exprsize
Vl-enumitem-exprsize
Vl-range-exprsize
Vl-paramdecl-exprsize
Vl-paramdecllist-exprsize
Vl-maybe-expr-size
Vl-evatom-exprsize
Vl-vardecllist-exprsize
Vl-portdecllist-exprsize
Vl-modinstlist-exprsize
Vl-initiallist-exprsize
Vl-gateinstlist-exprsize
Vl-fundecllist-exprsize
Vl-assign-exprsize
Vl-interfaceport-exprsize
Vl-assignlist-exprsize
Vl-alwayslist-exprsize
Vl-portlist-exprsize
Vl-modinst-exprsize
Vl-gateinst-exprsize
Vl-fundecl-exprsize
Vl-vardecl-exprsize
Vl-regularport-exprsize
Vl-portdecl-exprsize
Vl-initial-exprsize
Vl-always-exprsize
Vl-port-exprsize
Vl-lvalue-type
Vl-classify-extension-warning-hook
Welltyped
Vl-castexpr->datatype
Vl-expr-size-assigncontext
Vl-type-expr-pairs-sum-datatype-sizes
Vl-basictype->datatype
Vl-expr-replace-assignpatterns
Vl-design-exprsize
Vl-op-simple-vector-p
Vl-expr-val-alist-max-count
Vl-expr-has-patterns
Vl-exprlist-max-count
Vl-unsigned-when-size-zero-lst
Vl-type-expr-pairs
Append-n
Vl-expr-val-alist
Vl-datatypelist
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
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-expr-selfsize
Vl-exprlist-selfsize
Signature
(vl-exprlist-selfsize x ss ctx warnings) → (mv warnings size-list)
Arguments
x
— Expressions whose sizes we are to compute.
Guard
(
vl-exprlist-p
x)
.
ss
— Scope where these expressions occur.
Guard
(
vl-scopestack-p
ss)
.
ctx
— Context for warnings.
Guard
(
vl-context-p
ctx)
.
warnings
— Ordinary
warnings
accumulator.
Guard
(
vl-warninglist-p
warnings)
.
Returns
warnings
—
Type
(
vl-warninglist-p
warnings)
.
size-list
—
Type
(
and
(
vl-maybe-nat-listp
size-list) (
equal
(
len
size-list) (
len
x)))
.