		Search-engine friendly clone of the ACL2 documentation.

Qmarksize-check

Vl-expr-qmarksize-test-trivial

Recognize test expressions that are too trivial to warn about.

Signature
(vl-expr-qmarksize-test-trivial x ss) → *
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-expr-qmarksize-test-trivial

(defun vl-expr-qmarksize-test-trivial (x ss)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-expr-qmarksize-test-trivial))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x)))
   (vl-expr-case
    x :vl-literal
    (vl-value-case x.val
                   :vl-constint (or (eql x.val.value 1)
                                    (eql x.val.value 0))
                   :otherwise nil)
    :vl-index
    (b*
     (((unless (and (atom x.indices)
                    (vl-partselect-case x.part :none)))
       nil)
      ((mv err trace ?context ?tail)
       (vl-follow-scopeexpr x.scope ss))
      ((when err) nil)
      (target (vl-hidstep->item (car trace)))
      ((unless (eq (tag target) :vl-paramdecl))
       nil)
      ((vl-paramdecl target))
      (plain-p
       (vl-paramtype-case
        target.type
        :vl-implicitvalueparam (and (not target.type.range)
                                    (not target.type.sign))
        :vl-explicitvalueparam
        (vl-datatype-case
         target.type.type
         :vl-coretype
         (and
           (vl-coretypename-equiv target.type.type.name :vl-integer)
           (atom target.type.type.pdims)
           (atom target.type.type.udims))
         :otherwise nil)
        :vl-typeparam nil)))
     plain-p)
    :otherwise nil))))