(vl-syscall-typedecide x) → (mv warnings class)
Function:
(defun vl-syscall-typedecide (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-expr-case x :vl-call x.systemp :otherwise nil))) (let ((__function__ 'vl-syscall-typedecide)) (declare (ignorable __function__)) (b* ((warnings nil) (name (vl-simple-id-name (vl-call->name x))) ((when (equal name "$signed")) (mv (ok) :vl-signed-int-class)) ((when (equal name "$unsigned")) (mv (ok) :vl-unsigned-int-class)) (retinfo (vl-syscall->returninfo x)) ((unless retinfo) (mv (ok) :vl-error-class)) ((vl-coredatatype-info retinfo))) (mv (ok) (vl-coretype-arithclass retinfo retinfo.default-signedp)))))
Theorem:
(defthm vl-warninglist-p-of-vl-syscall-typedecide.warnings (b* (((mv ?warnings common-lisp::?class) (vl-syscall-typedecide x))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-arithclass-p-of-vl-syscall-typedecide.class (b* (((mv ?warnings common-lisp::?class) (vl-syscall-typedecide x))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-syscall-typedecide-of-vl-expr-fix-x (equal (vl-syscall-typedecide (vl-expr-fix x)) (vl-syscall-typedecide x)))
Theorem:
(defthm vl-syscall-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-syscall-typedecide x) (vl-syscall-typedecide x-equiv))) :rule-classes :congruence)