(vl-edgesplit-atomicstmt-lvalues x) → lvalue-names
Function:
(defun vl-edgesplit-atomicstmt-lvalues (x) (declare (xargs :guard (and (vl-stmt-p x) (vl-atomicstmt-p x) (vl-edgesplit-atomicstmt-p x)))) (let ((__function__ 'vl-edgesplit-atomicstmt-lvalues)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-assignstmt (list (vl-idexpr->name (vl-assignstmt->lvalue x)))) (otherwise nil))))
Theorem:
(defthm string-listp-of-vl-edgesplit-atomicstmt-lvalues (b* ((lvalue-names (vl-edgesplit-atomicstmt-lvalues x))) (string-listp lvalue-names)) :rule-classes :rewrite)