Try to convert a list of statements that make up a function's body into a vl-assignlist-p.
(vl-funbody-to-assignments-aux x warnings function) → (mv successp warnings assigns)
If this function is reasonable and in our supported subset, then
If
Function:
(defun vl-funbody-to-assignments-aux (x warnings function) (declare (xargs :guard (and (vl-stmtlist-p x) (vl-warninglist-p warnings) (vl-fundecl-p function)))) (let ((__function__ 'vl-funbody-to-assignments-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv t (ok) nil)) ((when (vl-nullstmt-p (car x))) (vl-funbody-to-assignments-aux (cdr x) warnings function)) ((unless (vl-assignstmt-p (car x))) (mv nil (fatal :type :vl-bad-function-stmt :msg "In ~a0, after rewriting, the function's body ~ includes ~a1, but only simple assignment statements ~ are permitted." :args (list function (car x))) nil)) ((mv okp warnings) (vl-fun-stmt-okp (car x) warnings function)) ((unless okp) (mv nil warnings nil)) ((vl-assignstmt x1) (car x)) (assign1 (make-vl-assign :lvalue x1.lvalue :expr x1.expr :atts (acons "VL_FUN_ASSIGN" (make-vl-atom :guts (make-vl-string :value (vl-fundecl->name function))) x1.atts) :loc x1.loc)) ((mv okp warnings cdr-assigns) (vl-funbody-to-assignments-aux (cdr x) warnings function))) (mv okp warnings (cons assign1 cdr-assigns)))))
Theorem:
(defthm booleanp-of-vl-funbody-to-assignments-aux.successp (b* (((mv ?successp ?warnings ?assigns) (vl-funbody-to-assignments-aux x warnings function))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-funbody-to-assignments-aux.warnings (b* (((mv ?successp ?warnings ?assigns) (vl-funbody-to-assignments-aux x warnings function))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-funbody-to-assignments-aux.assigns (b* (((mv ?successp ?warnings ?assigns) (vl-funbody-to-assignments-aux x warnings function))) (vl-assignlist-p assigns)) :rule-classes :rewrite)