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
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Scopestack
Hid-tools
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Vl-function-specialization-map-strip
Vl-portdecl-or-blockitem-list-strip
Vl-maybe-delayoreventcontrol-strip
Vl-portdecl-or-blockitem-strip
Vl-fundecl-strip
Vl-function-specialization-strip
Vl-taskdecl-strip
Vl-repeateventcontrol-strip
Vl-delayoreventcontrol-strip
Vl-sequence-strip
Vl-property-strip
Vl-paramtype-strip
Vl-modinst-strip
Vl-maybe-gatedelay-strip
Vl-gateinst-strip
Vl-assign-strip
Vl-vardecl-strip
Vl-propspec-strip
Vl-propport-strip
Vl-portdecl-strip
Vl-paramdecl-strip
Vl-maybe-exprdist-strip
Vl-letdecl-strip
Vl-initial-strip
Vl-blockitem-strip
Vl-arguments-strip
Vl-always-strip
Vl-alias-strip
Vl-vardecllist-strip
Vl-typedeflist-strip
Vl-repetition-strip
Vl-propportlist-strip
Vl-portdecllist-strip
Vl-plainarglist-strip
Vl-paramdecllist-strip
Vl-namedarglist-strip
Vl-modinstlist-strip
Vl-maybe-rhs-strip
Vl-gateinstlist-strip
Vl-gatedelay-strip
Vl-final-strip
Vl-exprdistlist-strip
Vl-eventcontrol-strip
Vl-distitem-strip
Vl-delaycontrol-strip
Vl-blockitemlist-strip
Vl-typedef-strip
Vl-rhs-strip
Vl-plainarg-strip
Vl-namedarg-strip
Vl-importlist-strip
Vl-import-strip
Vl-exprdist-strip
Vl-distlist-strip
Vl-assignlist-strip
Vl-expr-strip
Genblob
Expr-tools
Extract-vl-types
Hierarchy
Range-tools
Finding-by-name
Stmt-tools
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Stripping-functions
Vl-expr-strip
Strip an expression, removing attributes and code locations.
See
stripping-functions
.