Determine an atomic, splittable statement's effect on a single lvalue.
(vl-edgesplit-atomicstmt-for-lvalue x lvalue) → stmt
Function:
(defun vl-edgesplit-atomicstmt-for-lvalue (x lvalue) (declare (xargs :guard (and (and (vl-stmt-p x) (vl-atomicstmt-p x) (vl-edgesplit-atomicstmt-p x)) (stringp lvalue)))) (let ((__function__ 'vl-edgesplit-atomicstmt-for-lvalue)) (declare (ignorable __function__)) (case (vl-stmt-kind x) (:vl-assignstmt (if (equal (vl-idexpr->name (vl-assignstmt->lvalue x)) lvalue) x (make-vl-nullstmt))) (otherwise (make-vl-nullstmt)))))
Theorem:
(defthm vl-stmt-p-of-vl-edgesplit-atomicstmt-for-lvalue (implies (and (force (if (vl-stmt-p x) (if (vl-atomicstmt-p x) (vl-edgesplit-atomicstmt-p x) 'nil) 'nil)) (force (stringp lvalue))) (b* ((stmt (vl-edgesplit-atomicstmt-for-lvalue x lvalue))) (vl-stmt-p stmt))) :rule-classes :rewrite)