• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
          • Vl-rebuild-caselist
          • Vl-stmt-atomicstmts
          • Vl-compoundstmt->stmts
          • Vl-compoundstmt->exprs
          • Vl-compoundstmt->vardecls
          • Change-vl-compoundstmt
          • Vl-compoundstmt->paramdecls
          • Vl-compoundstmt->ctrl
          • Vl-atomicstmtlist-p
          • Vl-stmt->atts
          • Vl-atomicstmt-p
          • Vl-timingstmt-p
          • Vl-repeatstmt-p
          • Vl-foreverstmt-p
          • Vl-assignstmt-p
          • Vl-whilestmt-p
          • Vl-waitstmt-p
          • Vl-nullstmt-p
          • Vl-ifstmt-p
          • Vl-forstmt-p
          • Vl-dostmt-p
          • Vl-casestmt-p
          • Vl-callstmt-p
          • Vl-exprlistlist
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Stmt-tools

Vl-compoundstmt->stmts

Get all immediate sub-statements from any compound statement.

Signature

(vl-compoundstmt->stmts x) → stmts

Arguments

x — Guard (vl-stmt-p x).

Returns

stmts — Type (vl-stmtlist-p stmts).

This is useful for functions that want to recur over statements without paying much attention to the kinds of statements being traversed. For instance, if you just want to collect up all of the expressions everywhere throughout a statement, you can recur through the vl-compoundstmt->stmts without having to have separate cases for all the different kinds of expressions.

Definitions and Theorems

Function: vl-compoundstmt->stmts

(defun vl-compoundstmt->stmts (x)
 (declare (xargs :guard (vl-stmt-p x)))
 (declare (xargs :guard (not (vl-atomicstmt-p x))))
 (let ((__function__ 'vl-compoundstmt->stmts))
  (declare (ignorable __function__))
  (vl-stmt-case
      x :vl-casestmt
      (cons x.default (alist-vals x.caselist))
      :vl-ifstmt
      (list x.truebranch x.falsebranch)
      :vl-foreverstmt (list x.body)
      :vl-waitstmt (list x.body)
      :vl-whilestmt (list x.body)
      :vl-dostmt (list x.body)
      :vl-forstmt
      (append-without-guard x.initassigns x.stepforms (list x.body))
      :vl-foreachstmt (list x.body)
      :vl-blockstmt
      x.stmts :vl-repeatstmt (list x.body)
      :vl-timingstmt (list x.body)
      :vl-assertstmt
      (b* (((vl-assertion x.assertion)))
        (list x.assertion.success
              x.assertion.failure))
      :vl-cassertstmt
      (b* (((vl-cassertion x.cassertion)))
        (list x.cassertion.success
              x.cassertion.failure))
      :otherwise nil)))

Theorem: vl-stmtlist-p-of-vl-compoundstmt->stmts

(defthm vl-stmtlist-p-of-vl-compoundstmt->stmts
  (b* ((stmts (vl-compoundstmt->stmts x)))
    (vl-stmtlist-p stmts))
  :rule-classes :rewrite)

Theorem: vl-stmtlist-count-of-vl-compoundstmt->stmts-weak

(defthm vl-stmtlist-count-of-vl-compoundstmt->stmts-weak
  (<= (vl-stmtlist-count (vl-compoundstmt->stmts x))
      (vl-stmt-count x))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-stmtlist-count-of-vl-compoundstmt->stmts-strong

(defthm vl-stmtlist-count-of-vl-compoundstmt->stmts-strong
  (implies (not (vl-atomicstmt-p x))
           (< (vl-stmtlist-count (vl-compoundstmt->stmts x))
              (vl-stmt-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-compoundstmt->stmts-of-vl-stmt-fix-x

(defthm vl-compoundstmt->stmts-of-vl-stmt-fix-x
  (equal (vl-compoundstmt->stmts (vl-stmt-fix x))
         (vl-compoundstmt->stmts x)))

Theorem: vl-compoundstmt->stmts-vl-stmt-equiv-congruence-on-x

(defthm vl-compoundstmt->stmts-vl-stmt-equiv-congruence-on-x
  (implies (vl-stmt-equiv x x-equiv)
           (equal (vl-compoundstmt->stmts x)
                  (vl-compoundstmt->stmts x-equiv)))
  :rule-classes :congruence)