		Search-engine friendly clone of the ACL2 documentation.

Inline-mods

Vl-ok-to-inline-p

Check if a module is simple enough for us to inline.

Signature
(vl-ok-to-inline-p x) → okp
Arguments: x — Guard (vl-module-p x).

Definitions and Theorems

Function: vl-ok-to-inline-p

(defun vl-ok-to-inline-p (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-ok-to-inline-p))
    (declare (ignorable __function__))
    (b* (((vl-module x) x)
         (- (cw "Checking if we can inline ~s0..."
                x.name)))
      (and (or (not (vl-portdecls-with-dir :vl-inout x.portdecls))
               (cw "no: inout ports~%"))
           (or (not x.alwayses)
               (cw "no: always blocks~%"))
           (or (not x.paramdecls)
               (cw "no: parameter declarations~%"))
           (or (not x.fundecls)
               (cw "no: function declarations~%"))
           (or (not x.taskdecls)
               (cw "no: task declarations~%"))
           (not (cw "yes~%"))))))