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
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Svstmt-case
Svstmt-while
Svstmt-p
Svstmt-if
Svstmt-equiv
Svstmt-xcond
Svstmt-scope
Svstmt-assign
Svstmt-compile
Svstmt-constraints
Svstmt-jump
Svstmt-jump->type
Make-svstmt-jump
Change-svstmt-jump
Svstmtlist
Svstmt-kind
Svstmt.lisp
Svstmt-fix
Svstmt-count
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svstmt
Svstmt-jump
This is a product type, introduced by
deftagsum
in support of
svstmt
.
Fields
type —
svjump-p
Subtopics
Svstmt-jump->type
Get the
type
field from a
svstmt-jump
.
Make-svstmt-jump
Basic constructor macro for
svstmt-jump
structures.
Change-svstmt-jump
Modifying constructor for
svstmt-jump
structures.