Should we size the arguments to this system call?
(vl-sysfun-should-size-args-p name) → bool
This is used among functions like vl-expr-expandsizes and our notion of welltyped expressions to decide whether calls of system functions should have their arguments sized normally.
Motivation: consider the system function
However, for functions like
Function:
(defun vl-sysfun-should-size-args-p (name) (declare (xargs :guard (stringp name))) (let ((__function__ 'vl-sysfun-should-size-args-p)) (declare (ignorable __function__)) (let ((name (string-fix name))) (not (equal name "$bits")))))
Theorem:
(defthm vl-sysfun-should-size-args-p-of-str-fix-name (equal (vl-sysfun-should-size-args-p (str-fix name)) (vl-sysfun-should-size-args-p name)))
Theorem:
(defthm vl-sysfun-should-size-args-p-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-sysfun-should-size-args-p name) (vl-sysfun-should-size-args-p name-equiv))) :rule-classes :congruence)